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