src/HOL/Old_Number_Theory/Gauss.thy
author wenzelm
Sat, 10 Oct 2015 16:26:23 +0200
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 63566 e5abbdee461a
permissions -rw-r--r--
isabelle update_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
     1
(*  Title:      HOL/Old_Number_Theory/Gauss.thy
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
     2
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     3
*)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     4
61382
efac889fccbc isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     5
section \<open>Gauss' Lemma\<close>
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     6
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26289
diff changeset
     7
theory Gauss
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26289
diff changeset
     8
imports Euler
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26289
diff changeset
     9
begin
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    10
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    11
locale GAUSS =
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    12
  fixes p :: "int"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    13
  fixes a :: "int"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    14
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
    15
  assumes p_prime: "zprime p"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    16
  assumes p_g_2: "2 < p"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    17
  assumes p_a_relprime: "~[a = 0](mod p)"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    18
  assumes a_nonzero:    "0 < a"
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    19
begin
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    20
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
    21
definition "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
    22
definition "B = (%x. x * a) ` A"
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
    23
definition "C = StandardRes p ` B"
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
    24
definition "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
    25
definition "E = C \<inter> {x. ((p - 1) div 2) < x}"
e9b4835a54ee modernized specifications;
wenzelm
parents: 32479
diff changeset
    26
definition "F = (%x. (p - x)) ` E"
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    27
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    28
61382
efac889fccbc isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    29
subsection \<open>Basic properties of p\<close>
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    30
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    31
lemma p_odd: "p \<in> zOdd"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    32
  by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    33
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    34
lemma p_g_0: "0 < p"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    35
  using p_g_2 by auto
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    36
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    37
lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
26289
9d2c375e242b avoid unclear fact references;
wenzelm
parents: 22274
diff changeset
    38
  using ListMem.insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    39
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    40
lemma p_minus_one_l: "(p - 1) div 2 < p"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    41
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    42
  have "(p - 1) div 2 \<le> (p - 1) div 1"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    43
    by (rule zdiv_mono2) (auto simp add: p_g_0)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    44
  also have "\<dots> = p - 1" by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    45
  finally show ?thesis by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    46
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    47
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    48
lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
30034
60f64f112174 removed redundant thms
nipkow
parents: 27556
diff changeset
    49
  using div_mult_self1_is_id [of 2 "p - 1"] by auto
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    50
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    51
21288
wenzelm
parents: 21233
diff changeset
    52
lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    53
  apply (frule odd_minus_one_even)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    54
  apply (simp add: zEven_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    55
  apply (subgoal_tac "2 \<noteq> 0")
30034
60f64f112174 removed redundant thms
nipkow
parents: 27556
diff changeset
    56
  apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    57
  apply (auto simp add: even_div_2_prop2)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    58
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    59
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    60
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    61
lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    62
  apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    63
  apply (frule zodd_imp_zdiv_eq, auto)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    64
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    65
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    66
61382
efac889fccbc isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    67
subsection \<open>Basic Properties of the Gauss Sets\<close>
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    68
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    69
lemma finite_A: "finite (A)"
46756
faf62905cd53 adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
bulwahn
parents: 44766
diff changeset
    70
by (auto simp add: A_def)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    71
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    72
lemma finite_B: "finite (B)"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 38159
diff changeset
    73
by (auto simp add: B_def finite_A)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    74
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    75
lemma finite_C: "finite (C)"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 38159
diff changeset
    76
by (auto simp add: C_def finite_B)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    77
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    78
lemma finite_D: "finite (D)"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    79
by (auto simp add: D_def finite_C)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    80
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    81
lemma finite_E: "finite (E)"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    82
by (auto simp add: E_def finite_C)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    83
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    84
lemma finite_F: "finite (F)"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 38159
diff changeset
    85
by (auto simp add: F_def finite_E)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    86
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    87
lemma C_eq: "C = D \<union> E"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 38159
diff changeset
    88
by (auto simp add: C_def D_def E_def)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    89
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    90
lemma A_card_eq: "card A = nat ((p - 1) div 2)"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    91
  apply (auto simp add: A_def)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    92
  apply (insert int_nat)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    93
  apply (erule subst)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    94
  apply (auto simp add: card_bdd_int_set_l_le)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    95
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    96
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
    97
lemma inj_on_xa_A: "inj_on (%x. x * a) A"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
    98
  using a_nonzero by (simp add: A_def inj_on_def)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    99
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   100
lemma A_res: "ResSet p A"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   101
  apply (auto simp add: A_def ResSet_def)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   102
  apply (rule_tac m = p in zcong_less_eq)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   103
  apply (insert p_g_2, auto)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   104
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   105
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   106
lemma B_res: "ResSet p B"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   107
  apply (insert p_g_2 p_a_relprime p_minus_one_l)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   108
  apply (auto simp add: B_def)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   109
  apply (rule ResSet_image)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   110
  apply (auto simp add: A_res)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   111
  apply (auto simp add: A_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   112
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   113
  fix x fix y
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   114
  assume a: "[x * a = y * a] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   115
  assume b: "0 < x"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   116
  assume c: "x \<le> (p - 1) div 2"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   117
  assume d: "0 < y"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   118
  assume e: "y \<le> (p - 1) div 2"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   119
  from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   120
  have "[x = y](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   121
    by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   122
  with zcong_less_eq [of x y p] p_minus_one_l
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   123
      order_le_less_trans [of x "(p - 1) div 2" p]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   124
      order_le_less_trans [of y "(p - 1) div 2" p] show "x = y"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   125
    by (simp add: b c d e p_minus_one_l p_g_0)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   126
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   127
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   128
lemma SR_B_inj: "inj_on (StandardRes p) B"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   129
  apply (auto simp add: B_def StandardRes_def inj_on_def A_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   130
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   131
  fix x fix y
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   132
  assume a: "x * a mod p = y * a mod p"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   133
  assume b: "0 < x"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   134
  assume c: "x \<le> (p - 1) div 2"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   135
  assume d: "0 < y"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   136
  assume e: "y \<le> (p - 1) div 2"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   137
  assume f: "x \<noteq> y"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   138
  from a have "[x * a = y * a](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   139
    by (simp add: zcong_zmod_eq p_g_0)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   140
  with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   141
  have "[x = y](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   142
    by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   143
  with zcong_less_eq [of x y p] p_minus_one_l
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   144
    order_le_less_trans [of x "(p - 1) div 2" p]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   145
    order_le_less_trans [of y "(p - 1) div 2" p] have "x = y"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   146
    by (simp add: b c d e p_minus_one_l p_g_0)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   147
  then have False
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   148
    by (simp add: f)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   149
  then show "a = 0"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   150
    by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   151
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   152
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   153
lemma inj_on_pminusx_E: "inj_on (%x. p - x) E"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   154
  apply (auto simp add: E_def C_def B_def A_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   155
  apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   156
  apply auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   157
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   158
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   159
lemma A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   160
  apply (auto simp add: A_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   161
  apply (frule_tac m = p in zcong_not_zero)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   162
  apply (insert p_minus_one_l)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   163
  apply auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   164
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   165
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   166
lemma A_greater_zero: "x \<in> A ==> 0 < x"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   167
  by (auto simp add: A_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   168
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   169
lemma B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   170
  apply (auto simp add: B_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   171
  apply (frule A_ncong_p)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   172
  apply (insert p_a_relprime p_prime a_nonzero)
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 57418
diff changeset
   173
  apply (frule_tac a = xa and b = a in zcong_zprime_prod_zero_contra)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   174
  apply (auto simp add: A_greater_zero)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   175
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   176
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   177
lemma B_greater_zero: "x \<in> B ==> 0 < x"
56544
b60d5d119489 made mult_pos_pos a simp rule
nipkow
parents: 49962
diff changeset
   178
  using a_nonzero by (auto simp add: B_def A_greater_zero)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   179
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   180
lemma C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   181
  apply (auto simp add: C_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   182
  apply (frule B_ncong_p)
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 57418
diff changeset
   183
  apply (subgoal_tac "[xa = StandardRes p xa](mod p)")
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   184
  defer apply (simp add: StandardRes_prop1)
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 57418
diff changeset
   185
  apply (frule_tac a = xa and b = "StandardRes p xa" and c = 0 in zcong_trans)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   186
  apply auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   187
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   188
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   189
lemma C_greater_zero: "y \<in> C ==> 0 < y"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   190
  apply (auto simp add: C_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   191
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   192
  fix x
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   193
  assume a: "x \<in> B"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   194
  from p_g_0 have "0 \<le> StandardRes p x"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   195
    by (simp add: StandardRes_lbound)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   196
  moreover have "~[x = 0] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   197
    by (simp add: a B_ncong_p)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   198
  then have "StandardRes p x \<noteq> 0"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   199
    by (simp add: StandardRes_prop3)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   200
  ultimately show "0 < StandardRes p x"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   201
    by (simp add: order_le_less)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   202
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   203
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   204
lemma D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   205
  by (auto simp add: D_def C_ncong_p)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   206
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   207
lemma E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   208
  by (auto simp add: E_def C_ncong_p)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   209
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   210
lemma F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   211
  apply (auto simp add: F_def)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   212
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   213
  fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   214
  from E_ncong_p have "~[x = 0] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   215
    by (simp add: a)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   216
  moreover from a have "0 < x"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   217
    by (simp add: a E_def C_greater_zero)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   218
  moreover from a have "x < p"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   219
    by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   220
  ultimately have "~[p - x = 0] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   221
    by (simp add: zcong_not_zero)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   222
  from this show False by (simp add: b)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   223
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   224
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   225
lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   226
  apply (auto simp add: F_def E_def)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   227
  apply (insert p_g_0)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   228
  apply (frule_tac x = xa in StandardRes_ubound)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   229
  apply (frule_tac x = x in StandardRes_ubound)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   230
  apply (subgoal_tac "xa = StandardRes p xa")
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   231
  apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   232
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   233
  from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   234
    "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   235
    by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   236
  with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   237
      ==> p - StandardRes p x \<le> (p - 1) div 2"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   238
    by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   239
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   240
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   241
lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   242
  by (auto simp add: D_def C_greater_zero)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   243
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   244
lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   245
  by (auto simp add: F_def E_def D_def C_def B_def A_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   246
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   247
lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   248
  by (auto simp add: D_def C_def B_def A_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   249
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   250
lemma D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   251
  by (auto simp add: D_eq)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   252
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   253
lemma F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   254
  apply (auto simp add: F_eq A_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   255
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   256
  fix y
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   257
  assume "(p - 1) div 2 < StandardRes p (y * a)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   258
  then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   259
    by arith
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   260
  also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   261
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   262
  also have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   263
    by arith
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   264
  finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   265
    using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   266
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   267
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26289
diff changeset
   268
lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   269
  using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   270
27556
292098f2efdf unified curried gcd, lcm, zgcd, zlcm
haftmann
parents: 26289
diff changeset
   271
lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
30837
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30034
diff changeset
   272
by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   273
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   274
61382
efac889fccbc isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   275
subsection \<open>Relationships Between Gauss Sets\<close>
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   276
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   277
lemma B_card_eq_A: "card B = card A"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   278
  using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   279
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   280
lemma B_card_eq: "card B = nat ((p - 1) div 2)"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   281
  by (simp add: B_card_eq_A A_card_eq)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   282
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   283
lemma F_card_eq_E: "card F = card E"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   284
  using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   285
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   286
lemma C_card_eq_B: "card C = card B"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   287
  apply (insert finite_B)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   288
  apply (subgoal_tac "inj_on (StandardRes p) B")
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   289
  apply (simp add: B_def C_def card_image)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   290
  apply (rule StandardRes_inj_on_ResSet)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   291
  apply (simp add: B_res)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   292
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   293
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   294
lemma D_E_disj: "D \<inter> E = {}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   295
  by (auto simp add: D_def E_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   296
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   297
lemma C_card_eq_D_plus_E: "card C = card D + card E"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   298
  by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   299
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   300
lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   301
  apply (insert D_E_disj finite_D finite_E C_eq)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   302
  apply (frule setprod.union_disjoint [of D E id])
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   303
  apply auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   304
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   305
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   306
lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   307
  apply (auto simp add: C_def)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   308
  apply (insert finite_B SR_B_inj)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   309
  apply (frule setprod.reindex [of "StandardRes p" B id])
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   310
  apply auto
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   311
  apply (rule setprod_same_function_zcong)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   312
  apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   313
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   314
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   315
lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   316
  apply (rule Un_least)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   317
  apply (auto simp add: A_def F_subset D_subset)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   318
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   319
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   320
lemma F_D_disj: "(F \<inter> D) = {}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   321
  apply (simp add: F_eq D_eq)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   322
  apply (auto simp add: F_eq D_eq)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   323
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   324
  fix y fix ya
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   325
  assume "p - StandardRes p (y * a) = StandardRes p (ya * a)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   326
  then have "p = StandardRes p (y * a) + StandardRes p (ya * a)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   327
    by arith
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   328
  moreover have "p dvd p"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   329
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   330
  ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   331
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   332
  then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   333
    by (auto simp add: zcong_def)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   334
  have "[y * a = StandardRes p (y * a)] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   335
    by (simp only: zcong_sym StandardRes_prop1)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   336
  moreover have "[ya * a = StandardRes p (ya * a)] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   337
    by (simp only: zcong_sym StandardRes_prop1)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   338
  ultimately have "[y * a + ya * a =
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   339
    StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   340
    by (rule zcong_zadd)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   341
  with a have "[y * a + ya * a = 0] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   342
    apply (elim zcong_trans)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   343
    by (simp only: zcong_refl)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   344
  also have "y * a + ya * a = a * (y + ya)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   345
    by (simp add: distrib_left mult.commute)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   346
  finally have "[a * (y + ya) = 0] (mod p)" .
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   347
  with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   348
    p_a_relprime
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   349
  have a: "[y + ya = 0] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   350
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   351
  assume b: "y \<in> A" and c: "ya: A"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   352
  with A_def have "0 < y + ya"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   353
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   354
  moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   355
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   356
  moreover from b c p_eq2 A_def have "y + ya < p"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   357
    by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   358
  ultimately show False
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   359
    apply simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   360
    apply (frule_tac m = p in zcong_not_zero)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   361
    apply (auto simp add: a)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   362
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   363
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   364
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   365
lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   366
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   367
  have "card (F \<union> D) = card E + card D"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   368
    by (auto simp add: finite_F finite_D F_D_disj
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   369
      card_Un_disjoint F_card_eq_E)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   370
  then have "card (F \<union> D) = card C"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   371
    by (simp add: C_card_eq_D_plus_E)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   372
  from this show "card (F \<union> D) = nat ((p - 1) div 2)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   373
    by (simp add: C_card_eq_B B_card_eq)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   374
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   375
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   376
lemma F_Un_D_eq_A: "F \<union> D = A"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   377
  using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   378
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   379
lemma prod_D_F_eq_prod_A:
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   380
    "(setprod id D) * (setprod id F) = setprod id A"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   381
  apply (insert F_D_disj finite_D finite_F)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   382
  apply (frule setprod.union_disjoint [of F D id])
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   383
  apply (auto simp add: F_Un_D_eq_A)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   384
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   385
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   386
lemma prod_F_zcong:
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   387
  "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   388
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   389
  have "setprod id F = setprod id (op - p ` E)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   390
    by (auto simp add: F_def)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   391
  then have "setprod id F = setprod (op - p) E"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   392
    apply simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   393
    apply (insert finite_E inj_on_pminusx_E)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   394
    apply (frule setprod.reindex [of "minus p" E id])
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   395
    apply auto
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   396
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   397
  then have one:
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   398
    "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   399
    apply simp
30837
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30034
diff changeset
   400
    apply (insert p_g_0 finite_E StandardRes_prod)
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30034
diff changeset
   401
    by (auto)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   402
  moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   403
    apply clarify
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   404
    apply (insert zcong_id [of p])
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   405
    apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   406
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   407
  moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   408
    apply clarify
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   409
    apply (simp add: StandardRes_prop1 zcong_sym)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   410
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   411
  moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   412
    apply clarify
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   413
    apply (insert a b)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   414
    apply (rule_tac b = "p - x" in zcong_trans, auto)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   415
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   416
  ultimately have c:
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   417
    "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   418
    apply simp
30837
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30034
diff changeset
   419
    using finite_E p_g_0
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30034
diff changeset
   420
      setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
3d4832d9f7e4 added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents: 30034
diff changeset
   421
    by auto
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   422
  then have two: "[setprod id F = setprod (uminus) E](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   423
    apply (insert one c)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   424
    apply (rule zcong_trans [of "setprod id F"
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   425
                               "setprod (StandardRes p o op - p) E" p
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   426
                               "setprod uminus E"], auto)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   427
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   428
  also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
22274
ce1459004c8d Adapted to changes in Finite_Set theory.
berghofe
parents: 21404
diff changeset
   429
    using finite_E by (induct set: finite) auto
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   430
  then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   431
    by (simp add: mult.commute)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   432
  with two show ?thesis
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   433
    by simp
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   434
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   435
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   436
61382
efac889fccbc isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   437
subsection \<open>Gauss' Lemma\<close>
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   438
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57512
diff changeset
   439
lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   440
  by (auto simp add: finite_E neg_one_special)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   441
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   442
theorem pre_gauss_lemma:
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   443
  "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   444
proof -
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   445
  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: 57492
diff changeset
   446
    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   447
  then have "[setprod id A = ((-1)^(card E) * setprod id E) *
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   448
      setprod id D] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   449
    apply (rule zcong_trans)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   450
    apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.cong)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   451
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   452
  then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   453
    apply (rule zcong_trans)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   454
    apply (insert C_prod_eq_D_times_E, erule subst)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   455
    apply (subst mult.assoc, auto)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   456
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   457
  then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   458
    apply (rule zcong_trans)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   459
    apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod.cong)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   460
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   461
  then have "[setprod id A = ((-1)^(card E) *
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   462
    (setprod id ((%x. x * a) ` A)))] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   463
    by (simp add: B_def)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   464
  then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   465
    (mod p)"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   466
    by (simp add:finite_A inj_on_xa_A setprod.reindex cong del:setprod.cong)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   467
  moreover have "setprod (%x. x * a) A =
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   468
    setprod (%x. a) A * setprod id A"
22274
ce1459004c8d Adapted to changes in Finite_Set theory.
berghofe
parents: 21404
diff changeset
   469
    using finite_A by (induct set: finite) auto
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   470
  ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   471
    setprod id A))] (mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   472
    by simp
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   473
  then have "[setprod id A = ((-1)^(card E) * a^(card A) *
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   474
      setprod id A)](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   475
    apply (rule zcong_trans)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   476
    apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   477
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   478
  then have a: "[setprod id A * (-1)^(card E) =
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   479
      ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   480
    by (rule zcong_scalar)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   481
  then have "[setprod id A * (-1)^(card E) = setprod id A *
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   482
      (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   483
    apply (rule zcong_trans)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   484
    apply (simp add: a mult.commute mult.left_commute)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   485
    done
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   486
  then have "[setprod id A * (-1)^(card E) = setprod id A *
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   487
      a^(card A)](mod p)"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   488
    apply (rule zcong_trans)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 56544
diff changeset
   489
    apply (simp add: aux cong del:setprod.cong)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   490
    done
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57512
diff changeset
   491
  with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"]
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57512
diff changeset
   492
      p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   493
    by (simp add: order_less_imp_le)
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   494
  from this show ?thesis
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   495
    by (simp add: A_card_eq zcong_sym)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   496
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   497
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   498
theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   499
proof -
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   500
  from Euler_Criterion p_prime p_g_2 have
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16775
diff changeset
   501
      "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   502
    by auto
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   503
  moreover note pre_gauss_lemma
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   504
  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   505
    by (rule zcong_trans)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   506
  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   507
    by (auto simp add: Legendre_def)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   508
  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   509
    by (rule neg_one_power)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   510
  ultimately show ?thesis
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   511
    by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 14981
diff changeset
   512
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   513
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16733
diff changeset
   514
end
21233
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   515
5a5c8ea5f66a tuned specifications;
wenzelm
parents: 20898
diff changeset
   516
end