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