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