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