src/HOL/Old_Number_Theory/Residues.thy
author wenzelm
Thu Jan 13 23:50:16 2011 +0100 (2011-01-13)
changeset 41541 1fa4725c4656
parent 38159 e9b4835a54ee
child 53077 a1b3784f8129
permissions -rw-r--r--
eliminated global prems;
tuned proofs;
     1 (*  Title:      HOL/Old_Number_Theory/Residues.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3 *)
     4 
     5 header {* Residue Sets *}
     6 
     7 theory Residues
     8 imports Int2
     9 begin
    10 
    11 text {*
    12   \medskip Define the residue of a set, the standard residue,
    13   quadratic residues, and prove some basic properties. *}
    14 
    15 definition ResSet :: "int => int set => bool"
    16   where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
    17 
    18 definition StandardRes :: "int => int => int"
    19   where "StandardRes m x = x mod m"
    20 
    21 definition QuadRes :: "int => int => bool"
    22   where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
    23 
    24 definition Legendre :: "int => int => int" where
    25   "Legendre a p = (if ([a = 0] (mod p)) then 0
    26                      else if (QuadRes p a) then 1
    27                      else -1)"
    28 
    29 definition SR :: "int => int set"
    30   where "SR p = {x. (0 \<le> x) & (x < p)}"
    31 
    32 definition SRStar :: "int => int set"
    33   where "SRStar p = {x. (0 < x) & (x < p)}"
    34 
    35 
    36 subsection {* Some useful properties of StandardRes *}
    37 
    38 lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
    39   by (auto simp add: StandardRes_def zcong_zmod)
    40 
    41 lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
    42       = ([x1 = x2] (mod m))"
    43   by (auto simp add: StandardRes_def zcong_zmod_eq)
    44 
    45 lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))"
    46   by (auto simp add: StandardRes_def zcong_def dvd_eq_mod_eq_0)
    47 
    48 lemma StandardRes_prop4: "2 < m 
    49      ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
    50   by (auto simp add: StandardRes_def zcong_zmod_eq 
    51                      mod_mult_eq [of x y m])
    52 
    53 lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
    54   by (auto simp add: StandardRes_def)
    55 
    56 lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p"
    57   by (auto simp add: StandardRes_def)
    58 
    59 lemma StandardRes_eq_zcong: 
    60    "(StandardRes m x = 0) = ([x = 0](mod m))"
    61   by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
    62 
    63 
    64 subsection {* Relations between StandardRes, SRStar, and SR *}
    65 
    66 lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p"
    67   by (auto simp add: SRStar_def SR_def)
    68 
    69 lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x"
    70   by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)
    71 
    72 lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
    73      = (~[x = 0] (mod p))"
    74   apply (auto simp add: StandardRes_prop3 StandardRes_def SRStar_def)
    75   apply (subgoal_tac "0 < p")
    76   apply (drule_tac a = x in pos_mod_sign, arith, simp)
    77   done
    78 
    79 lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))"
    80   by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
    81 
    82 lemma StandardRes_SRStar_prop2: "[| 2 < p; zprime p; x \<in> SRStar p |] 
    83      ==> StandardRes p (MultInv p x) \<in> SRStar p"
    84   apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp)
    85   apply (rule MultInv_prop3)
    86   apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
    87   done
    88 
    89 lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x"
    90   by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
    91 
    92 lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \<in> SRStar p |] 
    93      ==> StandardRes p x \<in> SRStar p"
    94   by (frule StandardRes_SRStar_prop3, auto)
    95 
    96 lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] 
    97      ==> (StandardRes p (x * y)):SRStar p"
    98   apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
    99   apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
   100   apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
   101   done
   102 
   103 lemma SRStar_mult_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)); 
   104      x \<in> SRStar p |] 
   105      ==> StandardRes p (a * MultInv p x) \<in> SRStar p"
   106   apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
   107   apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
   108   apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
   109   done
   110 
   111 lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1"
   112   by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
   113 
   114 lemma SRStar_finite: "2 < p ==> finite( SRStar p)"
   115   by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
   116 
   117 
   118 subsection {* Properties relating ResSets with StandardRes *}
   119 
   120 lemma aux: "x mod m = y mod m ==> [x = y] (mod m)"
   121   apply (subgoal_tac "x = y ==> [x = y](mod m)")
   122   apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)")
   123   apply (auto simp add: zcong_zmod [of x y m])
   124   done
   125 
   126 lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)"
   127   apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
   128   apply (drule_tac m = m in aux, auto)
   129   done
   130 
   131 lemma StandardRes_Sum: "[| finite X; 0 < m |] 
   132      ==> [setsum f X = setsum (StandardRes m o f) X](mod m)" 
   133   apply (rule_tac F = X in finite_induct)
   134   apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
   135   done
   136 
   137 lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}"
   138   by (auto simp add: StandardRes_ubound StandardRes_lbound)
   139 
   140 lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X"
   141   apply (rule_tac f = "StandardRes m" in finite_imageD) 
   142   apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset)
   143   apply (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
   144   done
   145 
   146 lemma mod_mod_is_mod: "[x = x mod m](mod m)"
   147   by (auto simp add: zcong_zmod)
   148 
   149 lemma StandardRes_prod: "[| finite X; 0 < m |] 
   150      ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)"
   151   apply (rule_tac F = X in finite_induct)
   152   apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
   153   done
   154 
   155 lemma ResSet_image:
   156   "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==>
   157     ResSet m (f ` A)"
   158   by (auto simp add: ResSet_def)
   159 
   160 
   161 subsection {* Property for SRStar *}
   162 
   163 lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
   164   by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
   165 
   166 end