src/HOL/NumberTheory/Residues.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 14981 e73f8140af78 child 15392 290bc97038c7 permissions -rw-r--r--
import -> imports
```     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 = Int2:;
```
```     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 by (drule_tac a = x in pos_mod_sign, arith, simp)
```
```    95
```
```    96 lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))";
```
```    97   by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
```
```    98
```
```    99 lemma StandardRes_SRStar_prop2: "[| 2 < p; p \<in> zprime; x \<in> SRStar p |]
```
```   100      ==> StandardRes p (MultInv p x) \<in> SRStar p";
```
```   101   apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
```
```   102   apply (rule MultInv_prop3)
```
```   103   apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
```
```   104 done
```
```   105
```
```   106 lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x";
```
```   107   by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
```
```   108
```
```   109 lemma StandardRes_SRStar_prop4: "[| p \<in> zprime; 2 < p; x \<in> SRStar p |]
```
```   110      ==> StandardRes p x \<in> SRStar p";
```
```   111   by (frule StandardRes_SRStar_prop3, auto)
```
```   112
```
```   113 lemma SRStar_mult_prop1: "[| p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p|]
```
```   114      ==> (StandardRes p (x * y)):SRStar p";
```
```   115   apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
```
```   116   apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
```
```   117   apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
```
```   118 done
```
```   119
```
```   120 lemma SRStar_mult_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p));
```
```   121      x \<in> SRStar p |]
```
```   122      ==> StandardRes p (a * MultInv p x) \<in> SRStar p";
```
```   123   apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
```
```   124   apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
```
```   125   apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
```
```   126 done
```
```   127
```
```   128 lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
```
```   129   by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
```
```   130
```
```   131 lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
```
```   132   by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
```
```   133
```
```   134 (******************************************************************)
```
```   135 (*                                                                *)
```
```   136 (* Some useful stuff about ResSet and StandardRes                 *)
```
```   137 (*                                                                *)
```
```   138 (******************************************************************)
```
```   139
```
```   140 subsection {* Properties relating ResSets with StandardRes *}
```
```   141
```
```   142 lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
```
```   143   apply (subgoal_tac "x = y ==> [x = y](mod m)");
```
```   144   apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
```
```   145   apply (auto simp add: zcong_zmod [of x y m])
```
```   146 done
```
```   147
```
```   148 lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
```
```   149   apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
```
```   150   apply (drule_tac m = m in aux, auto)
```
```   151 done
```
```   152
```
```   153 lemma StandardRes_Sum: "[| finite X; 0 < m |]
```
```   154      ==> [setsum f X = setsum (StandardRes m o f) X](mod m)";
```
```   155   apply (rule_tac F = X in finite_induct)
```
```   156   apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
```
```   157 done
```
```   158
```
```   159 lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}";
```
```   160   by (auto simp add: StandardRes_ubound StandardRes_lbound)
```
```   161
```
```   162 lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
```
```   163   apply (rule_tac f = "StandardRes m" in finite_imageD)
```
```   164   apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset);
```
```   165 by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
```
```   166
```
```   167 lemma mod_mod_is_mod: "[x = x mod m](mod m)";
```
```   168   by (auto simp add: zcong_zmod)
```
```   169
```
```   170 lemma StandardRes_prod: "[| finite X; 0 < m |]
```
```   171      ==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)";
```
```   172   apply (rule_tac F = X in finite_induct)
```
```   173 by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
```
```   174
```
```   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)";
```
```   176   by (auto simp add: ResSet_def)
```
```   177
```
```   178 (****************************************************************)
```
```   179 (*                                                              *)
```
```   180 (* Property for SRStar                                          *)
```
```   181 (*                                                              *)
```
```   182 (****************************************************************)
```
```   183
```
```   184 lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
```
```   185   by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
```
```   186
```
`   187 end;`