src/HOL/NumberTheory/Residues.thy
changeset 13871 26e5f5e624f6
child 14981 e73f8140af78
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NumberTheory/Residues.thy	Thu Mar 20 15:58:25 2003 +0100
     1.3 @@ -0,0 +1,187 @@
     1.4 +(*  Title:      HOL/Quadratic_Reciprocity/Residues.thy
     1.5 +    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.6 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.7 +*)
     1.8 +
     1.9 +header {* Residue Sets *}
    1.10 +
    1.11 +theory Residues = Int2:;
    1.12 +
    1.13 +text{*Note.  This theory is being revised.  See the web page
    1.14 +\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
    1.15 +
    1.16 +(*****************************************************************)
    1.17 +(*                                                               *)
    1.18 +(* Define the residue of a set, the standard residue, quadratic  *)
    1.19 +(* residues, and prove some basic properties.                    *)
    1.20 +(*                                                               *)
    1.21 +(*****************************************************************)
    1.22 +
    1.23 +constdefs
    1.24 +  ResSet      :: "int => int set => bool"
    1.25 +  "ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) --> 
    1.26 +    y1 = y2)"
    1.27 +
    1.28 +  StandardRes :: "int => int => int"
    1.29 +  "StandardRes m x == x mod m"
    1.30 +
    1.31 +  QuadRes     :: "int => int => bool"
    1.32 +  "QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))"
    1.33 +
    1.34 +  Legendre    :: "int => int => int"      
    1.35 +  "Legendre a p == (if ([a = 0] (mod p)) then 0
    1.36 +                     else if (QuadRes p a) then 1
    1.37 +                     else -1)"
    1.38 +
    1.39 +  SR          :: "int => int set"
    1.40 +  "SR p == {x. (0 \<le> x) & (x < p)}"
    1.41 +
    1.42 +  SRStar      :: "int => int set"
    1.43 +  "SRStar p == {x. (0 < x) & (x < p)}";
    1.44 +
    1.45 +(******************************************************************)
    1.46 +(*                                                                *)
    1.47 +(* Some useful properties of StandardRes                          *)
    1.48 +(*                                                                *)
    1.49 +(******************************************************************)
    1.50 +
    1.51 +subsection {* Properties of StandardRes *}
    1.52 +
    1.53 +lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)";
    1.54 +  by (auto simp add: StandardRes_def zcong_zmod)
    1.55 +
    1.56 +lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
    1.57 +      = ([x1 = x2] (mod m))";
    1.58 +  by (auto simp add: StandardRes_def zcong_zmod_eq)
    1.59 +
    1.60 +lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))";
    1.61 +  by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)
    1.62 +
    1.63 +lemma StandardRes_prop4: "2 < m 
    1.64 +     ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)";
    1.65 +  by (auto simp add: StandardRes_def zcong_zmod_eq 
    1.66 +                     zmod_zmult_distrib [of x y m])
    1.67 +
    1.68 +lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x";
    1.69 +  by (auto simp add: StandardRes_def pos_mod_sign)
    1.70 +
    1.71 +lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p";
    1.72 +  by (auto simp add: StandardRes_def pos_mod_bound)
    1.73 +
    1.74 +lemma StandardRes_eq_zcong: 
    1.75 +   "(StandardRes m x = 0) = ([x = 0](mod m))";
    1.76 +  by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
    1.77 +
    1.78 +(******************************************************************)
    1.79 +(*                                                                *)
    1.80 +(* Some useful stuff relating StandardRes and SRStar and SR       *)
    1.81 +(*                                                                *)
    1.82 +(******************************************************************)
    1.83 +
    1.84 +subsection {* Relations between StandardRes, SRStar, and SR *}
    1.85 +
    1.86 +lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p";
    1.87 +  by (auto simp add: SRStar_def SR_def)
    1.88 +
    1.89 +lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x";
    1.90 +  by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)
    1.91 +
    1.92 +lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) 
    1.93 +     = (~[x = 0] (mod p))";
    1.94 +  apply (auto simp add: StandardRes_prop3 StandardRes_def
    1.95 +                        SRStar_def pos_mod_bound)
    1.96 +  apply (subgoal_tac "0 < p")
    1.97 +by (drule_tac a = x in pos_mod_sign, arith, simp)
    1.98 +
    1.99 +lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))";
   1.100 +  by (auto simp add: SRStar_def zcong_def zdvd_not_zless)
   1.101 +
   1.102 +lemma StandardRes_SRStar_prop2: "[| 2 < p; p \<in> zprime; x \<in> SRStar p |] 
   1.103 +     ==> StandardRes p (MultInv p x) \<in> SRStar p";
   1.104 +  apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
   1.105 +  apply (rule MultInv_prop3)
   1.106 +  apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
   1.107 +done
   1.108 +
   1.109 +lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x";
   1.110 +  by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)
   1.111 +
   1.112 +lemma StandardRes_SRStar_prop4: "[| p \<in> zprime; 2 < p; x \<in> SRStar p |] 
   1.113 +     ==> StandardRes p x \<in> SRStar p";
   1.114 +  by (frule StandardRes_SRStar_prop3, auto)
   1.115 +
   1.116 +lemma SRStar_mult_prop1: "[| p \<in> zprime; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] 
   1.117 +     ==> (StandardRes p (x * y)):SRStar p";
   1.118 +  apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
   1.119 +  apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
   1.120 +  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
   1.121 +done
   1.122 +
   1.123 +lemma SRStar_mult_prop2: "[| p \<in> zprime; 2 < p; ~([a = 0](mod p)); 
   1.124 +     x \<in> SRStar p |] 
   1.125 +     ==> StandardRes p (a * MultInv p x) \<in> SRStar p";
   1.126 +  apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
   1.127 +  apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
   1.128 +  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
   1.129 +done
   1.130 +
   1.131 +lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
   1.132 +  by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)
   1.133 +
   1.134 +lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
   1.135 +  by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
   1.136 +
   1.137 +(******************************************************************)
   1.138 +(*                                                                *)
   1.139 +(* Some useful stuff about ResSet and StandardRes                 *)
   1.140 +(*                                                                *)
   1.141 +(******************************************************************)
   1.142 +
   1.143 +subsection {* Properties relating ResSets with StandardRes *}
   1.144 +
   1.145 +lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
   1.146 +  apply (subgoal_tac "x = y ==> [x = y](mod m)");
   1.147 +  apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
   1.148 +  apply (auto simp add: zcong_zmod [of x y m])
   1.149 +done
   1.150 +
   1.151 +lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
   1.152 +  apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
   1.153 +  apply (drule_tac m = m in aux, auto)
   1.154 +done
   1.155 +
   1.156 +lemma StandardRes_Sum: "[| finite X; 0 < m |] 
   1.157 +     ==> [setsum f X = setsum (StandardRes m o f) X](mod m)"; 
   1.158 +  apply (rule_tac F = X in finite_induct)
   1.159 +  apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
   1.160 +done
   1.161 +
   1.162 +lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}";
   1.163 +  by (auto simp add: StandardRes_ubound StandardRes_lbound)
   1.164 +
   1.165 +lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
   1.166 +  apply (rule_tac f = "StandardRes m" in finite_imageD) 
   1.167 +  apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset);
   1.168 +by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)
   1.169 +
   1.170 +lemma mod_mod_is_mod: "[x = x mod m](mod m)";
   1.171 +  by (auto simp add: zcong_zmod)
   1.172 +
   1.173 +lemma StandardRes_prod: "[| finite X; 0 < m |] 
   1.174 +     ==> [gsetprod f X = gsetprod (StandardRes m o f) X] (mod m)";
   1.175 +  apply (rule_tac F = X in finite_induct)
   1.176 +by (auto intro!: zcong_zmult simp add: StandardRes_prop1)
   1.177 +
   1.178 +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)";
   1.179 +  by (auto simp add: ResSet_def)
   1.180 +
   1.181 +(****************************************************************)
   1.182 +(*                                                              *)
   1.183 +(* Property for SRStar                                          *)
   1.184 +(*                                                              *)
   1.185 +(****************************************************************)
   1.186 +
   1.187 +lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
   1.188 +  by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
   1.189 +
   1.190 +end;
   1.191 \ No newline at end of file