src/HOL/NumberTheory/Residues.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 13871 26e5f5e624f6
child 15392 290bc97038c7
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Quadratic_Reciprocity/Residues.thy
14981
e73f8140af78 Merged in license change from Isabelle2004
kleing
parents: 13871
diff changeset
     2
    ID:         $Id$
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     3
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     4
*)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     5
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     6
header {* Residue Sets *}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     7
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     8
theory Residues = Int2:;
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     9
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    10
text{*Note.  This theory is being revised.  See the web page
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    11
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    12
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    13
(*****************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    14
(*                                                               *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    15
(* Define the residue of a set, the standard residue, quadratic  *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    16
(* residues, and prove some basic properties.                    *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    17
(*                                                               *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    18
(*****************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    19
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    20
constdefs
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    21
  ResSet      :: "int => int set => bool"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    22
  "ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) --> 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    23
    y1 = y2)"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    24
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    25
  StandardRes :: "int => int => int"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    26
  "StandardRes m x == x mod m"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    27
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    28
  QuadRes     :: "int => int => bool"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    29
  "QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    30
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    31
  Legendre    :: "int => int => int"      
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    32
  "Legendre a p == (if ([a = 0] (mod p)) then 0
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    33
                     else if (QuadRes p a) then 1
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    34
                     else -1)"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    35
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    36
  SR          :: "int => int set"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    37
  "SR p == {x. (0 \<le> x) & (x < p)}"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    38
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    39
  SRStar      :: "int => int set"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    40
  "SRStar p == {x. (0 < x) & (x < p)}";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    41
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    42
(******************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    43
(*                                                                *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    44
(* Some useful properties of StandardRes                          *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    45
(*                                                                *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    46
(******************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    47
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    48
subsection {* Properties of StandardRes *}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    49
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    50
lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    51
  by (auto simp add: StandardRes_def zcong_zmod)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    52
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    53
lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    54
      = ([x1 = x2] (mod m))";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    55
  by (auto simp add: StandardRes_def zcong_zmod_eq)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    56
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    57
lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    58
  by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    59
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    60
lemma StandardRes_prop4: "2 < m 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    61
     ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    62
  by (auto simp add: StandardRes_def zcong_zmod_eq 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    63
                     zmod_zmult_distrib [of x y m])
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    64
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    65
lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    66
  by (auto simp add: StandardRes_def pos_mod_sign)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    67
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    68
lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    69
  by (auto simp add: StandardRes_def pos_mod_bound)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    70
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    71
lemma StandardRes_eq_zcong: 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    72
   "(StandardRes m x = 0) = ([x = 0](mod m))";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    73
  by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    74
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    75
(******************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    76
(*                                                                *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    77
(* Some useful stuff relating StandardRes and SRStar and SR       *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    78
(*                                                                *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    79
(******************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    80
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    81
subsection {* Relations between StandardRes, SRStar, and SR *}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    82
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    83
lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    84
  by (auto simp add: SRStar_def SR_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    85
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    86
lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    87
  by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    88
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    89
lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    90
     = (~[x = 0] (mod p))";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    91
  apply (auto simp add: StandardRes_prop3 StandardRes_def
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    92
                        SRStar_def pos_mod_bound)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    93
  apply (subgoal_tac "0 < p")
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    94
by (drule_tac a = x in pos_mod_sign, arith, simp)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    95
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    96
lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    97
  by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    98
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    99
lemma StandardRes_SRStar_prop2: "[| 2 < p; p \<in> zprime; x \<in> SRStar p |] 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   100
     ==> StandardRes p (MultInv p x) \<in> SRStar p";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   101
  apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   102
  apply (rule MultInv_prop3)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   103
  apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   104
done
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   105
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   106
lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   107
  by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   108
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   109
lemma StandardRes_SRStar_prop4: "[| p \<in> zprime; 2 < p; x \<in> SRStar p |] 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   110
     ==> StandardRes p x \<in> SRStar p";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   111
  by (frule StandardRes_SRStar_prop3, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   112
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   113
lemma SRStar_mult_prop1: "[| p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   114
     ==> (StandardRes p (x * y)):SRStar p";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   115
  apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   116
  apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   117
  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   118
done
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   119
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   120
lemma SRStar_mult_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)); 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   121
     x \<in> SRStar p |] 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   122
     ==> StandardRes p (a * MultInv p x) \<in> SRStar p";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   123
  apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   124
  apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   125
  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   126
done
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   127
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   128
lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   129
  by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   130
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   131
lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   132
  by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   133
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   134
(******************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   135
(*                                                                *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   136
(* Some useful stuff about ResSet and StandardRes                 *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   137
(*                                                                *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   138
(******************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   139
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   140
subsection {* Properties relating ResSets with StandardRes *}
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   141
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   142
lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   143
  apply (subgoal_tac "x = y ==> [x = y](mod m)");
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   144
  apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   145
  apply (auto simp add: zcong_zmod [of x y m])
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   146
done
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   147
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   148
lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   149
  apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   150
  apply (drule_tac m = m in aux, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   151
done
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   152
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   153
lemma StandardRes_Sum: "[| finite X; 0 < m |] 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   154
     ==> [setsum f X = setsum (StandardRes m o f) X](mod m)"; 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   155
  apply (rule_tac F = X in finite_induct)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   156
  apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   157
done
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   158
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   159
lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   160
  by (auto simp add: StandardRes_ubound StandardRes_lbound)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   161
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   162
lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   163
  apply (rule_tac f = "StandardRes m" in finite_imageD) 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   164
  apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset);
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   165
by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   166
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   167
lemma mod_mod_is_mod: "[x = x mod m](mod m)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   168
  by (auto simp add: zcong_zmod)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   169
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   170
lemma StandardRes_prod: "[| finite X; 0 < m |] 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   171
     ==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   172
  apply (rule_tac F = X in finite_induct)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   173
by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   174
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   175
lemma ResSet_image: "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> ResSet m (f ` A)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   176
  by (auto simp add: ResSet_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   177
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   178
(****************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   179
(*                                                              *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   180
(* Property for SRStar                                          *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   181
(*                                                              *)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   182
(****************************************************************)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   183
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   184
lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   185
  by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   186
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   187
end;