Gauss.thy ported from Old_Number_Theory (unfinished)
authorpaulson <lp15@cam.ac.uk>
Mon Feb 24 23:17:55 2014 +0000 (2014-02-24)
changeset 5573097ff9276e12d
parent 55729 3244957ca236
child 55731 66df76dd2640
child 55739 d8270c17b5be
Gauss.thy ported from Old_Number_Theory (unfinished)
src/HOL/Number_Theory/Gauss.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Mon Feb 24 23:17:55 2014 +0000
     1.3 @@ -0,0 +1,393 @@
     1.4 +(*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.5 +
     1.6 +Ported by lcp but unfinished
     1.7 +*)
     1.8 +
     1.9 +header {* Gauss' Lemma *}
    1.10 +
    1.11 +theory Gauss
    1.12 +imports Residues
    1.13 +begin
    1.14 +
    1.15 +lemma cong_prime_prod_zero_nat: 
    1.16 +  fixes a::nat
    1.17 +  shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
    1.18 +  by (auto simp add: cong_altdef_nat)
    1.19 +
    1.20 +lemma cong_prime_prod_zero_int: 
    1.21 +  fixes a::int
    1.22 +  shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
    1.23 +  by (auto simp add: cong_altdef_int)
    1.24 +
    1.25 +
    1.26 +locale GAUSS =
    1.27 +  fixes p :: "nat"
    1.28 +  fixes a :: "int"
    1.29 +
    1.30 +  assumes p_prime: "prime p"
    1.31 +  assumes p_ge_2: "2 < p"
    1.32 +  assumes p_a_relprime: "[a \<noteq> 0](mod p)"
    1.33 +  assumes a_nonzero:    "0 < a"
    1.34 +begin
    1.35 +
    1.36 +definition "A = {0::int <.. ((int p - 1) div 2)}"
    1.37 +definition "B = (\<lambda>x. x * a) ` A"
    1.38 +definition "C = (\<lambda>x. x mod p) ` B"
    1.39 +definition "D = C \<inter> {.. (int p - 1) div 2}"
    1.40 +definition "E = C \<inter> {(int p - 1) div 2 <..}"
    1.41 +definition "F = (\<lambda>x. (int p - x)) ` E"
    1.42 +
    1.43 +
    1.44 +subsection {* Basic properties of p *}
    1.45 +
    1.46 +lemma odd_p: "odd p"
    1.47 +by (metis p_prime p_ge_2 prime_odd_nat)
    1.48 +
    1.49 +lemma p_minus_one_l: "(int p - 1) div 2 < p"
    1.50 +proof -
    1.51 +  have "(p - 1) div 2 \<le> (p - 1) div 1"
    1.52 +    by (metis div_by_1 div_le_dividend)
    1.53 +  also have "\<dots> = p - 1" by simp
    1.54 +  finally show ?thesis using p_ge_2 by arith
    1.55 +qed
    1.56 +
    1.57 +lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
    1.58 +  using odd_p p_ge_2 div_mult_self1_is_id [of 2 "p - 1"]   
    1.59 +  by auto presburger
    1.60 +
    1.61 +lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
    1.62 +  using odd_p p_ge_2
    1.63 +  by (auto simp add: even_def) (metis p_eq2)
    1.64 +
    1.65 +
    1.66 +subsection {* Basic Properties of the Gauss Sets *}
    1.67 +
    1.68 +lemma finite_A: "finite (A)"
    1.69 +by (auto simp add: A_def)
    1.70 +
    1.71 +lemma finite_B: "finite (B)"
    1.72 +by (auto simp add: B_def finite_A)
    1.73 +
    1.74 +lemma finite_C: "finite (C)"
    1.75 +by (auto simp add: C_def finite_B)
    1.76 +
    1.77 +lemma finite_D: "finite (D)"
    1.78 +by (auto simp add: D_def finite_C)
    1.79 +
    1.80 +lemma finite_E: "finite (E)"
    1.81 +by (auto simp add: E_def finite_C)
    1.82 +
    1.83 +lemma finite_F: "finite (F)"
    1.84 +by (auto simp add: F_def finite_E)
    1.85 +
    1.86 +lemma C_eq: "C = D \<union> E"
    1.87 +by (auto simp add: C_def D_def E_def)
    1.88 +
    1.89 +lemma A_card_eq: "card A = nat ((int p - 1) div 2)"
    1.90 +  by (auto simp add: A_def)
    1.91 +
    1.92 +lemma inj_on_xa_A: "inj_on (\<lambda>x. x * a) A"
    1.93 +  using a_nonzero by (simp add: A_def inj_on_def)
    1.94 +
    1.95 +definition ResSet :: "int => int set => bool"
    1.96 +  where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
    1.97 +
    1.98 +lemma ResSet_image:
    1.99 +  "\<lbrakk> 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) \<rbrakk> \<Longrightarrow>
   1.100 +    ResSet m (f ` A)"
   1.101 +  by (auto simp add: ResSet_def)
   1.102 +
   1.103 +lemma A_res: "ResSet p A"
   1.104 +  using p_ge_2
   1.105 +  by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int)
   1.106 +
   1.107 +lemma B_res: "ResSet p B"
   1.108 +proof -
   1.109 +  {fix x fix y
   1.110 +    assume a: "[x * a = y * a] (mod p)"
   1.111 +    assume b: "0 < x"
   1.112 +    assume c: "x \<le> (int p - 1) div 2"
   1.113 +    assume d: "0 < y"
   1.114 +    assume e: "y \<le> (int p - 1) div 2"
   1.115 +    from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
   1.116 +    have "[x = y](mod p)"
   1.117 +      by (metis comm_monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
   1.118 +                cong_mult_self_int gcd_int.commute prime_imp_coprime_int)
   1.119 +    with cong_less_imp_eq_int [of x y p] p_minus_one_l
   1.120 +        order_le_less_trans [of x "(int p - 1) div 2" p]
   1.121 +        order_le_less_trans [of y "(int p - 1) div 2" p] 
   1.122 +    have "x = y"
   1.123 +      by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
   1.124 +    } note xy = this
   1.125 +  show ?thesis
   1.126 +    apply (insert p_ge_2 p_a_relprime p_minus_one_l)
   1.127 +    apply (auto simp add: B_def)
   1.128 +    apply (rule ResSet_image)
   1.129 +    apply (auto simp add: A_res)
   1.130 +    apply (auto simp add: A_def xy)
   1.131 +    done
   1.132 +  qed
   1.133 +
   1.134 +lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B"
   1.135 +proof -
   1.136 +{ fix x fix y
   1.137 +  assume a: "x * a mod p = y * a mod p"
   1.138 +  assume b: "0 < x"
   1.139 +  assume c: "x \<le> (int p - 1) div 2"
   1.140 +  assume d: "0 < y"
   1.141 +  assume e: "y \<le> (int p - 1) div 2"
   1.142 +  assume f: "x \<noteq> y"
   1.143 +  from a have "[x * a = y * a](mod p)" 
   1.144 +    by (metis cong_int_def)
   1.145 +  with p_a_relprime p_prime cong_mult_rcancel_int [of a p x y]
   1.146 +  have "[x = y](mod p)" 
   1.147 +    by (metis cong_mult_self_int dvd_div_mult_self gcd_commute_int prime_imp_coprime_int)
   1.148 +  with cong_less_imp_eq_int [of x y p] p_minus_one_l
   1.149 +    order_le_less_trans [of x "(int p - 1) div 2" p]
   1.150 +    order_le_less_trans [of y "(int p - 1) div 2" p] 
   1.151 +  have "x = y"
   1.152 +    by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int zero_zle_int)
   1.153 +  then have False
   1.154 +    by (simp add: f)}
   1.155 +  then show ?thesis
   1.156 +    by (auto simp add: B_def inj_on_def A_def) metis
   1.157 +qed
   1.158 +
   1.159 +lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
   1.160 +  apply (auto simp add: E_def C_def B_def A_def)
   1.161 +  apply (rule_tac g = "(op - (int p))" in inj_on_inverseI)
   1.162 +  apply auto
   1.163 +  done
   1.164 +
   1.165 +lemma nonzero_mod_p:
   1.166 +  fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
   1.167 +by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int 
   1.168 +     inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int)
   1.169 +
   1.170 +lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
   1.171 +  by (rule nonzero_mod_p) (auto simp add: A_def)
   1.172 +
   1.173 +lemma A_greater_zero: "x \<in> A \<Longrightarrow> 0 < x"
   1.174 +  by (auto simp add: A_def)
   1.175 +
   1.176 +lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
   1.177 +  by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
   1.178 +
   1.179 +lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
   1.180 +  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
   1.181 +
   1.182 +lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
   1.183 +proof (auto simp add: C_def)
   1.184 +  fix x :: int
   1.185 +  assume a1: "x \<in> B"
   1.186 +  have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith
   1.187 +  have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp
   1.188 +  thus "0 < x mod int p" using a1 f2 
   1.189 +    by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
   1.190 +qed
   1.191 +
   1.192 +lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}"
   1.193 +  apply (auto simp add: F_def E_def C_def)
   1.194 +  apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj)
   1.195 +  apply (auto intro: p_odd_int)
   1.196 +  done
   1.197 +
   1.198 +lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   1.199 +  by (auto simp add: D_def C_greater_zero)
   1.200 +
   1.201 +lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}"
   1.202 +  by (auto simp add: F_def E_def D_def C_def B_def A_def)
   1.203 +
   1.204 +lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}"
   1.205 +  by (auto simp add: D_def C_def B_def A_def)
   1.206 +
   1.207 +lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
   1.208 +  using p_prime A_ncong_p [OF assms]
   1.209 +  by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
   1.210 +
   1.211 +lemma A_prod_relprime: "gcd (setprod id A) p = 1"
   1.212 +  by (metis DEADID.map_id all_A_relprime setprod_coprime_int)
   1.213 +
   1.214 +
   1.215 +subsection {* Relationships Between Gauss Sets *}
   1.216 +
   1.217 +lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
   1.218 +  by (auto simp add: ResSet_def inj_on_def cong_int_def)
   1.219 +
   1.220 +lemma B_card_eq_A: "card B = card A"
   1.221 +  using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
   1.222 +
   1.223 +lemma B_card_eq: "card B = nat ((int p - 1) div 2)"
   1.224 +  by (simp add: B_card_eq_A A_card_eq)
   1.225 +
   1.226 +lemma F_card_eq_E: "card F = card E"
   1.227 +  using finite_E 
   1.228 +  by (simp add: F_def inj_on_pminusx_E card_image)
   1.229 +
   1.230 +lemma C_card_eq_B: "card C = card B"
   1.231 +proof -
   1.232 +  have "inj_on (\<lambda>x. x mod p) B"
   1.233 +    by (metis SR_B_inj) 
   1.234 +  then show ?thesis
   1.235 +    by (metis C_def card_image)
   1.236 +qed
   1.237 +
   1.238 +lemma D_E_disj: "D \<inter> E = {}"
   1.239 +  by (auto simp add: D_def E_def)
   1.240 +
   1.241 +lemma C_card_eq_D_plus_E: "card C = card D + card E"
   1.242 +  by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   1.243 +
   1.244 +lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
   1.245 +  by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod_Un_disjoint sup_commute)
   1.246 +
   1.247 +lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   1.248 +  apply (auto simp add: C_def)
   1.249 +  apply (insert finite_B SR_B_inj)
   1.250 +  apply (frule_tac f = "\<lambda>x. x mod int p" in setprod_reindex_id [symmetric], auto)
   1.251 +  apply (rule cong_setprod_int)
   1.252 +  apply (auto simp add: cong_int_def)
   1.253 +  done
   1.254 +
   1.255 +lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
   1.256 +  apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset])
   1.257 +  apply (auto simp add: A_def)
   1.258 +  done
   1.259 +
   1.260 +lemma F_D_disj: "(F \<inter> D) = {}"
   1.261 +proof (auto simp add: F_eq D_eq)
   1.262 +  fix y::int and z::int
   1.263 +  assume "p - (y*a) mod p = (z*a) mod p"
   1.264 +  then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
   1.265 +    by (metis add_commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
   1.266 +  moreover have "[y * a = (y*a) mod p] (mod p)"
   1.267 +    by (metis cong_int_def mod_mod_trivial)
   1.268 +  ultimately have "[a * (y + z) = 0] (mod p)"
   1.269 +    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult_commute ring_class.ring_distribs(1))
   1.270 +  with p_prime a_nonzero p_a_relprime
   1.271 +  have a: "[y + z = 0] (mod p)"
   1.272 +    by (metis cong_prime_prod_zero_int)
   1.273 +  assume b: "y \<in> A" and c: "z \<in> A"
   1.274 +  with A_def have "0 < y + z"
   1.275 +    by auto
   1.276 +  moreover from b c p_eq2 A_def have "y + z < p"
   1.277 +    by auto
   1.278 +  ultimately show False
   1.279 +    by (metis a nonzero_mod_p)
   1.280 +qed
   1.281 +
   1.282 +lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
   1.283 +proof -
   1.284 +  have "card (F \<union> D) = card E + card D"
   1.285 +    by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E)
   1.286 +  then have "card (F \<union> D) = card C"
   1.287 +    by (simp add: C_card_eq_D_plus_E)
   1.288 +  then show "card (F \<union> D) = nat ((p - 1) div 2)"
   1.289 +    by (simp add: C_card_eq_B B_card_eq)
   1.290 +qed
   1.291 +
   1.292 +lemma F_Un_D_eq_A: "F \<union> D = A"
   1.293 +  using finite_A F_Un_D_subset A_card_eq F_Un_D_card 
   1.294 +  by (auto simp add: card_seteq)
   1.295 +
   1.296 +lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
   1.297 +  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod_Un_disjoint)
   1.298 +
   1.299 +lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   1.300 +proof -
   1.301 +  have FE: "setprod id F = setprod (op - p) E"
   1.302 +    apply (auto simp add: F_def)
   1.303 +    apply (insert finite_E inj_on_pminusx_E)
   1.304 +    apply (frule setprod_reindex_id, auto)
   1.305 +    done
   1.306 +  then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
   1.307 +    by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
   1.308 +  then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)"
   1.309 +    using finite_E p_ge_2
   1.310 +          cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
   1.311 +    by auto
   1.312 +  then have two: "[setprod id F = setprod (uminus) E](mod p)"
   1.313 +    by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1)
   1.314 +  have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   1.315 +    using finite_E by (induct set: finite) auto
   1.316 +  with two show ?thesis
   1.317 +    by simp
   1.318 +qed
   1.319 +
   1.320 +
   1.321 +subsection {* Gauss' Lemma *}
   1.322 +
   1.323 +lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
   1.324 +by (metis (no_types) minus_minus mult_commute mult_left_commute power_minus power_one)
   1.325 +
   1.326 +theorem pre_gauss_lemma:
   1.327 +  "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   1.328 +proof -
   1.329 +  have "[setprod id A = setprod id F * setprod id D](mod p)"
   1.330 +    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
   1.331 +  then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
   1.332 +    apply (rule cong_trans_int)
   1.333 +    apply (metis cong_scalar_int prod_F_zcong)
   1.334 +    done
   1.335 +  then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   1.336 +    by (metis C_prod_eq_D_times_E mult_commute mult_left_commute)
   1.337 +  then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   1.338 +    by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
   1.339 +  then have "[setprod id A = ((-1)^(card E) *
   1.340 +    (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)"
   1.341 +    by (simp add: B_def)
   1.342 +  then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
   1.343 +    (mod p)"
   1.344 +    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
   1.345 +  moreover have "setprod (\<lambda>x. x * a) A =
   1.346 +    setprod (\<lambda>x. a) A * setprod id A"
   1.347 +    using finite_A by (induct set: finite) auto
   1.348 +  ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A *
   1.349 +    setprod id A))] (mod p)"
   1.350 +    by simp
   1.351 +  then have "[setprod id A = ((-1)^(card E) * a^(card A) *
   1.352 +      setprod id A)](mod p)"
   1.353 +    apply (rule cong_trans_int)
   1.354 +    apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult_assoc)
   1.355 +    done
   1.356 +  then have a: "[setprod id A * (-1)^(card E) =
   1.357 +      ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   1.358 +    by (rule cong_scalar_int)
   1.359 +  then have "[setprod id A * (-1)^(card E) = setprod id A *
   1.360 +      (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   1.361 +    apply (rule cong_trans_int)
   1.362 +    apply (simp add: a mult_commute mult_left_commute)
   1.363 +    done
   1.364 +  then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
   1.365 +    apply (rule cong_trans_int)
   1.366 +    apply (simp add: aux cong del:setprod_cong)
   1.367 +    done
   1.368 +  with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   1.369 +    by (metis cong_mult_lcancel_int)
   1.370 +  then show ?thesis
   1.371 +    by (simp add: A_card_eq cong_sym_int)
   1.372 +qed
   1.373 +
   1.374 +(*NOT WORKING. Old_Number_Theory/Euler.thy needs to be translated, but it's
   1.375 +quite a mess and should better be completely redone.
   1.376 +
   1.377 +theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   1.378 +proof -
   1.379 +  from Euler_Criterion p_prime p_ge_2 have
   1.380 +      "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   1.381 +    by auto
   1.382 +  moreover note pre_gauss_lemma
   1.383 +  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
   1.384 +    by (rule cong_trans_int)
   1.385 +  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
   1.386 +    by (auto simp add: Legendre_def)
   1.387 +  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
   1.388 +    by (rule neg_one_power)
   1.389 +  ultimately show ?thesis
   1.390 +    by (auto simp add: p_ge_2 one_not_neg_one_mod_m zcong_sym)
   1.391 +qed
   1.392 +*)
   1.393 +
   1.394 +end
   1.395 +
   1.396 +end
     2.1 --- a/src/HOL/ROOT	Mon Feb 24 22:41:08 2014 +0100
     2.2 +++ b/src/HOL/ROOT	Mon Feb 24 23:17:55 2014 +0000
     2.3 @@ -173,7 +173,7 @@
     2.4  session "HOL-Number_Theory" in Number_Theory = HOL +
     2.5    description {*
     2.6      Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     2.7 -    Theorem, Wilson's Theorem, Quadratic Reciprocity.
     2.8 +    Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
     2.9    *}
    2.10    options [document_graph]
    2.11    theories [document = false]
    2.12 @@ -183,6 +183,7 @@
    2.13      "~~/src/HOL/Algebra/FiniteProduct"
    2.14    theories
    2.15      Pocklington
    2.16 +    Gauss
    2.17      Number_Theory
    2.18    files
    2.19      "document/root.tex"