src/HOL/Old_Number_Theory/Residues.thy
 author wenzelm Sun Aug 18 19:59:19 2013 +0200 (2013-08-18) changeset 53077 a1b3784f8129 parent 41541 1fa4725c4656 child 58889 5b7a9633cfa8 permissions -rw-r--r--
more symbols;
 wenzelm@38159 ` 1` ```(* Title: HOL/Old_Number_Theory/Residues.thy ``` paulson@13871 ` 2` ``` Authors: Jeremy Avigad, David Gray, and Adam Kramer ``` paulson@13871 ` 3` ```*) ``` paulson@13871 ` 4` paulson@13871 ` 5` ```header {* Residue Sets *} ``` paulson@13871 ` 6` wenzelm@38159 ` 7` ```theory Residues ``` wenzelm@38159 ` 8` ```imports Int2 ``` wenzelm@38159 ` 9` ```begin ``` paulson@13871 ` 10` wenzelm@19670 ` 11` ```text {* ``` wenzelm@19670 ` 12` ``` \medskip Define the residue of a set, the standard residue, ``` wenzelm@19670 ` 13` ``` quadratic residues, and prove some basic properties. *} ``` paulson@13871 ` 14` wenzelm@38159 ` 15` ```definition ResSet :: "int => int set => bool" ``` wenzelm@38159 ` 16` ``` where "ResSet m X = (\y1 y2. (y1 \ X & y2 \ X & [y1 = y2] (mod m) --> y1 = y2))" ``` paulson@13871 ` 17` wenzelm@38159 ` 18` ```definition StandardRes :: "int => int => int" ``` wenzelm@38159 ` 19` ``` where "StandardRes m x = x mod m" ``` paulson@13871 ` 20` wenzelm@38159 ` 21` ```definition QuadRes :: "int => int => bool" ``` wenzelm@53077 ` 22` ``` where "QuadRes m x = (\y. ([y\<^sup>2 = x] (mod m)))" ``` paulson@13871 ` 23` wenzelm@38159 ` 24` ```definition Legendre :: "int => int => int" where ``` 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` wenzelm@38159 ` 29` ```definition SR :: "int => int set" ``` wenzelm@38159 ` 30` ``` where "SR p = {x. (0 \ x) & (x < p)}" ``` paulson@13871 ` 31` wenzelm@38159 ` 32` ```definition SRStar :: "int => int set" ``` wenzelm@38159 ` 33` ``` where "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))" ``` nipkow@30042 ` 46` ``` by (auto simp add: StandardRes_def zcong_def dvd_eq_mod_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 ``` nipkow@29948 ` 51` ``` mod_mult_eq [of x y m]) ``` paulson@13871 ` 52` wenzelm@18369 ` 53` ```lemma StandardRes_lbound: "0 < p ==> 0 \ StandardRes p x" ``` wenzelm@41541 ` 54` ``` by (auto simp add: StandardRes_def) ``` paulson@13871 ` 55` wenzelm@18369 ` 56` ```lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p" ``` wenzelm@41541 ` 57` ``` by (auto simp add: StandardRes_def) ``` 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))" ``` wenzelm@41541 ` 74` ``` apply (auto simp add: StandardRes_prop3 StandardRes_def SRStar_def) ``` paulson@13871 ` 75` ``` apply (subgoal_tac "0 < p") ``` wenzelm@18369 ` 76` ``` apply (drule_tac a = x in pos_mod_sign, arith, simp) ``` wenzelm@18369 ` 77` ``` done ``` paulson@13871 ` 78` wenzelm@18369 ` 79` ```lemma StandardRes_SRStar_prop1a: "x \ SRStar p ==> ~([x = 0] (mod p))" ``` paulson@13871 ` 80` ``` by (auto simp add: SRStar_def zcong_def zdvd_not_zless) ``` paulson@13871 ` 81` nipkow@16663 ` 82` ```lemma StandardRes_SRStar_prop2: "[| 2 < p; zprime p; x \ SRStar p |] ``` wenzelm@18369 ` 83` ``` ==> StandardRes p (MultInv p x) \ SRStar p" ``` wenzelm@18369 ` 84` ``` apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp) ``` paulson@13871 ` 85` ``` apply (rule MultInv_prop3) ``` paulson@13871 ` 86` ``` apply (auto simp add: SRStar_def zcong_def zdvd_not_zless) ``` wenzelm@18369 ` 87` ``` done ``` paulson@13871 ` 88` wenzelm@18369 ` 89` ```lemma StandardRes_SRStar_prop3: "x \ SRStar p ==> StandardRes p x = x" ``` paulson@13871 ` 90` ``` by (auto simp add: SRStar_SR_prop StandardRes_SR_prop) ``` paulson@13871 ` 91` nipkow@16663 ` 92` ```lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \ SRStar p |] ``` wenzelm@18369 ` 93` ``` ==> StandardRes p x \ SRStar p" ``` paulson@13871 ` 94` ``` by (frule StandardRes_SRStar_prop3, auto) ``` paulson@13871 ` 95` nipkow@16663 ` 96` ```lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \ SRStar p; y \ SRStar p|] ``` wenzelm@18369 ` 97` ``` ==> (StandardRes p (x * y)):SRStar p" ``` paulson@13871 ` 98` ``` apply (frule_tac x = x in StandardRes_SRStar_prop4, auto) ``` paulson@13871 ` 99` ``` apply (frule_tac x = y in StandardRes_SRStar_prop4, auto) ``` paulson@13871 ` 100` ``` apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) ``` wenzelm@18369 ` 101` ``` done ``` paulson@13871 ` 102` nipkow@16663 ` 103` ```lemma SRStar_mult_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)); ``` paulson@13871 ` 104` ``` x \ SRStar p |] ``` wenzelm@18369 ` 105` ``` ==> StandardRes p (a * MultInv p x) \ SRStar p" ``` paulson@13871 ` 106` ``` apply (frule_tac x = x in StandardRes_SRStar_prop2, auto) ``` paulson@13871 ` 107` ``` apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1) ``` paulson@13871 ` 108` ``` apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) ``` wenzelm@18369 ` 109` ``` done ``` paulson@13871 ` 110` wenzelm@18369 ` 111` ```lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1" ``` paulson@13871 ` 112` ``` by (auto simp add: SRStar_def int_card_bdd_int_set_l_l) ``` paulson@13871 ` 113` wenzelm@18369 ` 114` ```lemma SRStar_finite: "2 < p ==> finite( SRStar p)" ``` paulson@13871 ` 115` ``` by (auto simp add: SRStar_def bdd_int_set_l_l_finite) ``` paulson@13871 ` 116` paulson@13871 ` 117` paulson@13871 ` 118` ```subsection {* Properties relating ResSets with StandardRes *} ``` paulson@13871 ` 119` wenzelm@18369 ` 120` ```lemma aux: "x mod m = y mod m ==> [x = y] (mod m)" ``` wenzelm@18369 ` 121` ``` apply (subgoal_tac "x = y ==> [x = y](mod m)") ``` wenzelm@18369 ` 122` ``` apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)") ``` paulson@13871 ` 123` ``` apply (auto simp add: zcong_zmod [of x y m]) ``` wenzelm@18369 ` 124` ``` done ``` paulson@13871 ` 125` wenzelm@18369 ` 126` ```lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)" ``` paulson@13871 ` 127` ``` apply (auto simp add: ResSet_def StandardRes_def inj_on_def) ``` paulson@13871 ` 128` ``` apply (drule_tac m = m in aux, auto) ``` wenzelm@18369 ` 129` ``` done ``` paulson@13871 ` 130` paulson@13871 ` 131` ```lemma StandardRes_Sum: "[| finite X; 0 < m |] ``` wenzelm@18369 ` 132` ``` ==> [setsum f X = setsum (StandardRes m o f) X](mod m)" ``` paulson@13871 ` 133` ``` apply (rule_tac F = X in finite_induct) ``` paulson@13871 ` 134` ``` apply (auto intro!: zcong_zadd simp add: StandardRes_prop1) ``` wenzelm@18369 ` 135` ``` done ``` paulson@13871 ` 136` wenzelm@18369 ` 137` ```lemma SR_pos: "0 < m ==> (StandardRes m ` X) \ {x. 0 \ x & x < m}" ``` paulson@13871 ` 138` ``` by (auto simp add: StandardRes_ubound StandardRes_lbound) ``` paulson@13871 ` 139` wenzelm@18369 ` 140` ```lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X" ``` paulson@13871 ` 141` ``` apply (rule_tac f = "StandardRes m" in finite_imageD) ``` wenzelm@18369 ` 142` ``` apply (rule_tac B = "{x. (0 :: int) \ x & x < m}" in finite_subset) ``` wenzelm@18369 ` 143` ``` apply (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos) ``` wenzelm@18369 ` 144` ``` done ``` paulson@13871 ` 145` wenzelm@18369 ` 146` ```lemma mod_mod_is_mod: "[x = x mod m](mod m)" ``` paulson@13871 ` 147` ``` by (auto simp add: zcong_zmod) ``` paulson@13871 ` 148` paulson@13871 ` 149` ```lemma StandardRes_prod: "[| finite X; 0 < m |] ``` wenzelm@18369 ` 150` ``` ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)" ``` paulson@13871 ` 151` ``` apply (rule_tac F = X in finite_induct) ``` wenzelm@18369 ` 152` ``` apply (auto intro!: zcong_zmult simp add: StandardRes_prop1) ``` wenzelm@18369 ` 153` ``` done ``` paulson@13871 ` 154` wenzelm@19670 ` 155` ```lemma ResSet_image: ``` wenzelm@19670 ` 156` ``` "[| 0 < m; ResSet m A; \x \ A. \y \ A. ([f x = f y](mod m) --> x = y) |] ==> ``` wenzelm@19670 ` 157` ``` ResSet m (f ` A)" ``` paulson@13871 ` 158` ``` by (auto simp add: ResSet_def) ``` paulson@13871 ` 159` wenzelm@19670 ` 160` wenzelm@19670 ` 161` ```subsection {* Property for SRStar *} ``` paulson@13871 ` 162` wenzelm@18369 ` 163` ```lemma ResSet_SRStar_prop: "ResSet p (SRStar p)" ``` paulson@13871 ` 164` ``` by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq) ``` paulson@13871 ` 165` wenzelm@18369 ` 166` ```end ```