Added NewNumberTheory by Jeremy Avigad
authornipkow
Fri Jun 19 18:33:10 2009 +0200 (2009-06-19)
changeset 3171929f5b20e8ee8
parent 31718 7715d4d3586f
child 31720 d1ac3f3b2f54
child 31721 b03270a8c23f
Added NewNumberTheory by Jeremy Avigad
src/HOL/IsaMakefile
src/HOL/NewNumberTheory/Binomial.thy
src/HOL/NewNumberTheory/Cong.thy
src/HOL/NewNumberTheory/Fib.thy
src/HOL/NewNumberTheory/MiscAlgebra.thy
src/HOL/NewNumberTheory/ROOT.ML
src/HOL/NewNumberTheory/Residues.thy
src/HOL/NewNumberTheory/UniqueFactorization.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 19 18:01:09 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 19 18:33:10 2009 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4    HOL-Modelcheck \
     1.5    HOL-NanoJava \
     1.6    HOL-Nominal-Examples \
     1.7 +  HOL-NewNumberTheory \
     1.8    HOL-NumberTheory \
     1.9    HOL-Prolog \
    1.10    HOL-SET-Protocol \
    1.11 @@ -489,6 +490,18 @@
    1.12  	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
    1.13  
    1.14  
    1.15 +## HOL-NewNumberTheory
    1.16 +
    1.17 +HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
    1.18 +
    1.19 +$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL GCD.thy Library/Multiset.thy	\
    1.20 +  NewNumberTheory/Fib.thy NewNumberTheory/Binomial.thy			\
    1.21 +  NewNumberTheory/Residues.thy NewNumberTheory/UniqueFactorization.thy  \
    1.22 +  NewNumberTheory/Cong.thy NewNumberTheory/MiscAlgebra.thy \
    1.23 +  NewNumberTheory/ROOT.ML
    1.24 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
    1.25 +
    1.26 +
    1.27  ## HOL-NumberTheory
    1.28  
    1.29  HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/NewNumberTheory/Binomial.thy	Fri Jun 19 18:33:10 2009 +0200
     2.3 @@ -0,0 +1,540 @@
     2.4 +(*  Title:      Binomial.thy
     2.5 +    Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
     2.6 +
     2.7 +
     2.8 +Defines factorial and the "choose" function, and establishes basic properties.
     2.9 +
    2.10 +The original theory "Binomial" was by Lawrence C. Paulson, based on
    2.11 +the work of Andy Gordon and Florian Kammueller. The approach here,
    2.12 +which derives the definition of binomial coefficients in terms of the
    2.13 +factorial function, is due to Jeremy Avigad. The binomial theorem was
    2.14 +formalized by Tobias Nipkow.
    2.15 +
    2.16 +*)
    2.17 +
    2.18 +
    2.19 +header {* Binomial *}
    2.20 +
    2.21 +theory Binomial
    2.22 +imports Cong
    2.23 +begin
    2.24 +
    2.25 +
    2.26 +subsection {* Main definitions *}
    2.27 +
    2.28 +class binomial =
    2.29 +
    2.30 +fixes 
    2.31 +  fact :: "'a \<Rightarrow> 'a" and
    2.32 +  binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
    2.33 +
    2.34 +(* definitions for the natural numbers *)
    2.35 +
    2.36 +instantiation nat :: binomial
    2.37 +
    2.38 +begin 
    2.39 +
    2.40 +fun
    2.41 +  fact_nat :: "nat \<Rightarrow> nat"
    2.42 +where
    2.43 +  "fact_nat x = 
    2.44 +   (if x = 0 then 1 else
    2.45 +                  x * fact(x - 1))"
    2.46 +
    2.47 +fun
    2.48 +  binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    2.49 +where
    2.50 +  "binomial_nat n k =
    2.51 +   (if k = 0 then 1 else
    2.52 +    if n = 0 then 0 else
    2.53 +      (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
    2.54 +
    2.55 +instance proof qed
    2.56 +
    2.57 +end
    2.58 +
    2.59 +(* definitions for the integers *)
    2.60 +
    2.61 +instantiation int :: binomial
    2.62 +
    2.63 +begin 
    2.64 +
    2.65 +definition
    2.66 +  fact_int :: "int \<Rightarrow> int"
    2.67 +where  
    2.68 +  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
    2.69 +
    2.70 +definition
    2.71 +  binomial_int :: "int => int \<Rightarrow> int"
    2.72 +where
    2.73 +  "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
    2.74 +      else 0)"
    2.75 +instance proof qed
    2.76 +
    2.77 +end
    2.78 +
    2.79 +
    2.80 +subsection {* Set up Transfer *}
    2.81 +
    2.82 +
    2.83 +lemma transfer_nat_int_binomial:
    2.84 +  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
    2.85 +  "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) = 
    2.86 +      nat (binomial n k)"
    2.87 +  unfolding fact_int_def binomial_int_def 
    2.88 +  by auto
    2.89 +
    2.90 +
    2.91 +lemma transfer_nat_int_binomial_closures:
    2.92 +  "x >= (0::int) \<Longrightarrow> fact x >= 0"
    2.93 +  "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
    2.94 +  by (auto simp add: fact_int_def binomial_int_def)
    2.95 +
    2.96 +declare TransferMorphism_nat_int[transfer add return: 
    2.97 +    transfer_nat_int_binomial transfer_nat_int_binomial_closures]
    2.98 +
    2.99 +lemma transfer_int_nat_binomial:
   2.100 +  "fact (int x) = int (fact x)"
   2.101 +  "binomial (int n) (int k) = int (binomial n k)"
   2.102 +  unfolding fact_int_def binomial_int_def by auto
   2.103 +
   2.104 +lemma transfer_int_nat_binomial_closures:
   2.105 +  "is_nat x \<Longrightarrow> fact x >= 0"
   2.106 +  "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
   2.107 +  by (auto simp add: fact_int_def binomial_int_def)
   2.108 +
   2.109 +declare TransferMorphism_int_nat[transfer add return: 
   2.110 +    transfer_int_nat_binomial transfer_int_nat_binomial_closures]
   2.111 +
   2.112 +
   2.113 +subsection {* Factorial *}
   2.114 +
   2.115 +lemma nat_fact_zero [simp]: "fact (0::nat) = 1"
   2.116 +  by simp
   2.117 +
   2.118 +lemma int_fact_zero [simp]: "fact (0::int) = 1"
   2.119 +  by (simp add: fact_int_def)
   2.120 +
   2.121 +lemma nat_fact_one [simp]: "fact (1::nat) = 1"
   2.122 +  by simp
   2.123 +
   2.124 +lemma nat_fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
   2.125 +  by (simp add: One_nat_def)
   2.126 +
   2.127 +lemma int_fact_one [simp]: "fact (1::int) = 1"
   2.128 +  by (simp add: fact_int_def)
   2.129 +
   2.130 +lemma nat_fact_plus_one: "fact ((n::nat) + 1) = (n + 1) * fact n"
   2.131 +  by simp
   2.132 +
   2.133 +lemma nat_fact_Suc: "fact (Suc n) = (Suc n) * fact n"
   2.134 +  by (simp add: One_nat_def)
   2.135 +
   2.136 +lemma int_fact_plus_one: 
   2.137 +  assumes "n >= 0"
   2.138 +  shows "fact ((n::int) + 1) = (n + 1) * fact n"
   2.139 +
   2.140 +  using prems by (rule nat_fact_plus_one [transferred])
   2.141 +
   2.142 +lemma nat_fact_reduce: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   2.143 +  by simp
   2.144 +
   2.145 +lemma int_fact_reduce: 
   2.146 +  assumes "(n::int) > 0"
   2.147 +  shows "fact n = n * fact (n - 1)"
   2.148 +
   2.149 +  using prems apply (subst tsub_eq [symmetric], auto)
   2.150 +  apply (rule nat_fact_reduce [transferred])
   2.151 +  using prems apply auto
   2.152 +done
   2.153 +
   2.154 +declare fact_nat.simps [simp del]
   2.155 +
   2.156 +lemma nat_fact_nonzero [simp]: "fact (n::nat) \<noteq> 0"
   2.157 +  apply (induct n rule: nat_induct')
   2.158 +  apply (auto simp add: nat_fact_plus_one)
   2.159 +done
   2.160 +
   2.161 +lemma int_fact_nonzero [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
   2.162 +  by (simp add: fact_int_def)
   2.163 +
   2.164 +lemma nat_fact_gt_zero [simp]: "fact (n :: nat) > 0"
   2.165 +  by (insert nat_fact_nonzero [of n], arith)
   2.166 +
   2.167 +lemma int_fact_gt_zero [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
   2.168 +  by (auto simp add: fact_int_def)
   2.169 +
   2.170 +lemma nat_fact_ge_one [simp]: "fact (n :: nat) >= 1"
   2.171 +  by (insert nat_fact_nonzero [of n], arith)
   2.172 +
   2.173 +lemma nat_fact_ge_Suc_0 [simp]: "fact (n :: nat) >= Suc 0"
   2.174 +  by (insert nat_fact_nonzero [of n], arith)
   2.175 +
   2.176 +lemma int_fact_ge_one [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
   2.177 +  apply (auto simp add: fact_int_def)
   2.178 +  apply (subgoal_tac "1 = int 1")
   2.179 +  apply (erule ssubst)
   2.180 +  apply (subst zle_int)
   2.181 +  apply auto
   2.182 +done
   2.183 +
   2.184 +lemma nat_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
   2.185 +  apply (induct n rule: nat_induct')
   2.186 +  apply (auto simp add: nat_fact_plus_one)
   2.187 +  apply (subgoal_tac "m = n + 1")
   2.188 +  apply auto
   2.189 +done
   2.190 +
   2.191 +lemma int_dvd_fact [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
   2.192 +  apply (case_tac "1 <= n")
   2.193 +  apply (induct n rule: int_ge_induct)
   2.194 +  apply (auto simp add: int_fact_plus_one)
   2.195 +  apply (subgoal_tac "m = i + 1")
   2.196 +  apply auto
   2.197 +done
   2.198 +
   2.199 +lemma nat_interval_plus_one: "(i::nat) <= j + 1 \<Longrightarrow> 
   2.200 +  {i..j+1} = {i..j} Un {j+1}"
   2.201 +  by auto
   2.202 +
   2.203 +lemma int_interval_plus_one: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
   2.204 +  by auto
   2.205 +
   2.206 +lemma nat_fact_altdef: "fact (n::nat) = (PROD i:{1..n}. i)"
   2.207 +  apply (induct n rule: nat_induct')
   2.208 +  apply force
   2.209 +  apply (subst nat_fact_plus_one)
   2.210 +  apply (subst nat_interval_plus_one)
   2.211 +  apply auto
   2.212 +done
   2.213 +
   2.214 +lemma int_fact_altdef: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
   2.215 +  apply (induct n rule: int_ge_induct)
   2.216 +  apply force
   2.217 +  apply (subst int_fact_plus_one, assumption)
   2.218 +  apply (subst int_interval_plus_one)
   2.219 +  apply auto
   2.220 +done
   2.221 +
   2.222 +subsection {* Infinitely many primes *}
   2.223 +
   2.224 +lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
   2.225 +proof-
   2.226 +  have f1: "fact n + 1 \<noteq> 1" using nat_fact_ge_one [of n] by arith 
   2.227 +  from nat_prime_factor [OF f1]
   2.228 +      obtain p where "prime p" and "p dvd fact n + 1" by auto
   2.229 +  hence "p \<le> fact n + 1" 
   2.230 +    by (intro dvd_imp_le, auto)
   2.231 +  {assume "p \<le> n"
   2.232 +    from `prime p` have "p \<ge> 1" 
   2.233 +      by (cases p, simp_all)
   2.234 +    with `p <= n` have "p dvd fact n" 
   2.235 +      by (intro nat_dvd_fact)
   2.236 +    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   2.237 +      by (rule nat_dvd_diff)
   2.238 +    hence "p dvd 1" by simp
   2.239 +    hence "p <= 1" by auto
   2.240 +    moreover from `prime p` have "p > 1" by auto
   2.241 +    ultimately have False by auto}
   2.242 +  hence "n < p" by arith
   2.243 +  with `prime p` and `p <= fact n + 1` show ?thesis by auto
   2.244 +qed
   2.245 +
   2.246 +lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
   2.247 +using next_prime_bound by auto
   2.248 +
   2.249 +lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
   2.250 +proof
   2.251 +  assume "finite {(p::nat). prime p}"
   2.252 +  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
   2.253 +    by auto
   2.254 +  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
   2.255 +    by auto
   2.256 +  with bigger_prime [of b] show False by auto
   2.257 +qed
   2.258 +
   2.259 +
   2.260 +subsection {* Binomial coefficients *}
   2.261 +
   2.262 +lemma nat_choose_zero [simp]: "(n::nat) choose 0 = 1"
   2.263 +  by simp
   2.264 +
   2.265 +lemma int_choose_zero [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
   2.266 +  by (simp add: binomial_int_def)
   2.267 +
   2.268 +lemma nat_zero_choose [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
   2.269 +  by (induct n rule: nat_induct', auto)
   2.270 +
   2.271 +lemma int_zero_choose [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
   2.272 +  unfolding binomial_int_def apply (case_tac "n < 0")
   2.273 +  apply force
   2.274 +  apply (simp del: binomial_nat.simps)
   2.275 +done
   2.276 +
   2.277 +lemma nat_choose_reduce: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
   2.278 +    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
   2.279 +  by simp
   2.280 +
   2.281 +lemma int_choose_reduce: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
   2.282 +    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
   2.283 +  unfolding binomial_int_def apply (subst nat_choose_reduce)
   2.284 +    apply (auto simp del: binomial_nat.simps 
   2.285 +      simp add: nat_diff_distrib)
   2.286 +done
   2.287 +
   2.288 +lemma nat_choose_plus_one: "((n::nat) + 1) choose (k + 1) = 
   2.289 +    (n choose (k + 1)) + (n choose k)"
   2.290 +  by (simp add: nat_choose_reduce)
   2.291 +
   2.292 +lemma nat_choose_Suc: "(Suc n) choose (Suc k) = 
   2.293 +    (n choose (Suc k)) + (n choose k)"
   2.294 +  by (simp add: nat_choose_reduce One_nat_def)
   2.295 +
   2.296 +lemma int_choose_plus_one: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) = 
   2.297 +    (n choose (k + 1)) + (n choose k)"
   2.298 +  by (simp add: binomial_int_def nat_choose_plus_one nat_add_distrib 
   2.299 +    del: binomial_nat.simps)
   2.300 +
   2.301 +declare binomial_nat.simps [simp del]
   2.302 +
   2.303 +lemma nat_choose_self [simp]: "((n::nat) choose n) = 1"
   2.304 +  by (induct n rule: nat_induct', auto simp add: nat_choose_plus_one)
   2.305 +
   2.306 +lemma int_choose_self [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
   2.307 +  by (auto simp add: binomial_int_def)
   2.308 +
   2.309 +lemma nat_choose_one [simp]: "(n::nat) choose 1 = n"
   2.310 +  by (induct n rule: nat_induct', auto simp add: nat_choose_reduce)
   2.311 +
   2.312 +lemma int_choose_one [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
   2.313 +  by (auto simp add: binomial_int_def)
   2.314 +
   2.315 +lemma nat_plus_one_choose_self [simp]: "(n::nat) + 1 choose n = n + 1"
   2.316 +  apply (induct n rule: nat_induct', force)
   2.317 +  apply (case_tac "n = 0")
   2.318 +  apply auto
   2.319 +  apply (subst nat_choose_reduce)
   2.320 +  apply (auto simp add: One_nat_def)  
   2.321 +  (* natdiff_cancel_numerals introduces Suc *)
   2.322 +done
   2.323 +
   2.324 +lemma nat_Suc_choose_self [simp]: "(Suc n) choose n = Suc n"
   2.325 +  using nat_plus_one_choose_self by (simp add: One_nat_def)
   2.326 +
   2.327 +lemma int_plus_one_choose_self [rule_format, simp]: 
   2.328 +    "(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"
   2.329 +   by (auto simp add: binomial_int_def nat_add_distrib)
   2.330 +
   2.331 +(* bounded quantification doesn't work with the unicode characters? *)
   2.332 +lemma nat_choose_pos [rule_format]: "ALL k <= (n::nat). 
   2.333 +    ((n::nat) choose k) > 0"
   2.334 +  apply (induct n rule: nat_induct') 
   2.335 +  apply force
   2.336 +  apply clarify
   2.337 +  apply (case_tac "k = 0")
   2.338 +  apply force
   2.339 +  apply (subst nat_choose_reduce)
   2.340 +  apply auto
   2.341 +done
   2.342 +
   2.343 +lemma int_choose_pos: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
   2.344 +    ((n::int) choose k) > 0"
   2.345 +  by (auto simp add: binomial_int_def nat_choose_pos)
   2.346 +
   2.347 +lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow> 
   2.348 +    (ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
   2.349 +    P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
   2.350 +  apply (induct n rule: nat_induct')
   2.351 +  apply auto
   2.352 +  apply (case_tac "k = 0")
   2.353 +  apply auto
   2.354 +  apply (case_tac "k = n + 1")
   2.355 +  apply auto
   2.356 +  apply (drule_tac x = n in spec) back back 
   2.357 +  apply (drule_tac x = "k - 1" in spec) back back back
   2.358 +  apply auto
   2.359 +done
   2.360 +
   2.361 +lemma nat_choose_altdef_aux: "(k::nat) \<le> n \<Longrightarrow> 
   2.362 +    fact k * fact (n - k) * (n choose k) = fact n"
   2.363 +  apply (rule binomial_induct [of _ k n])
   2.364 +  apply auto
   2.365 +proof -
   2.366 +  fix k :: nat and n
   2.367 +  assume less: "k < n"
   2.368 +  assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
   2.369 +  hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
   2.370 +    by (subst nat_fact_plus_one, auto)
   2.371 +  assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = 
   2.372 +      fact n"
   2.373 +  with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * 
   2.374 +      (n choose (k + 1)) = (n - k) * fact n"
   2.375 +    by (subst (2) nat_fact_plus_one, auto)
   2.376 +  with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) = 
   2.377 +      (n - k) * fact n" by simp
   2.378 +  have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
   2.379 +      fact (k + 1) * fact (n - k) * (n choose (k + 1)) + 
   2.380 +      fact (k + 1) * fact (n - k) * (n choose k)" 
   2.381 +    by (subst nat_choose_reduce, auto simp add: ring_simps)
   2.382 +  also note one
   2.383 +  also note two
   2.384 +  also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
   2.385 +    apply (subst nat_fact_plus_one)
   2.386 +    apply (subst left_distrib [symmetric])
   2.387 +    apply simp
   2.388 +    done
   2.389 +  finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = 
   2.390 +    fact (n + 1)" .
   2.391 +qed
   2.392 +
   2.393 +lemma nat_choose_altdef: "(k::nat) \<le> n \<Longrightarrow> 
   2.394 +    n choose k = fact n div (fact k * fact (n - k))"
   2.395 +  apply (frule nat_choose_altdef_aux)
   2.396 +  apply (erule subst)
   2.397 +  apply (simp add: mult_ac)
   2.398 +done
   2.399 +
   2.400 +
   2.401 +lemma int_choose_altdef: 
   2.402 +  assumes "(0::int) <= k" and "k <= n"
   2.403 +  shows "n choose k = fact n div (fact k * fact (n - k))"
   2.404 +  
   2.405 +  apply (subst tsub_eq [symmetric], rule prems)
   2.406 +  apply (rule nat_choose_altdef [transferred])
   2.407 +  using prems apply auto
   2.408 +done
   2.409 +
   2.410 +lemma nat_choose_dvd: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
   2.411 +  unfolding dvd_def apply (frule nat_choose_altdef_aux)
   2.412 +  (* why don't blast and auto get this??? *)
   2.413 +  apply (rule exI)
   2.414 +  apply (erule sym)
   2.415 +done
   2.416 +
   2.417 +lemma int_choose_dvd: 
   2.418 +  assumes "(0::int) <= k" and "k <= n"
   2.419 +  shows "fact k * fact (n - k) dvd fact n"
   2.420 + 
   2.421 +  apply (subst tsub_eq [symmetric], rule prems)
   2.422 +  apply (rule nat_choose_dvd [transferred])
   2.423 +  using prems apply auto
   2.424 +done
   2.425 +
   2.426 +(* generalizes Tobias Nipkow's proof to any commutative semiring *)
   2.427 +theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = 
   2.428 +  (SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
   2.429 +proof (induct n rule: nat_induct')
   2.430 +  show "?P 0" by simp
   2.431 +next
   2.432 +  fix n
   2.433 +  assume ih: "?P n"
   2.434 +  have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
   2.435 +    by auto
   2.436 +  have decomp2: "{0..n} = {0} Un {1..n}"
   2.437 +    by auto
   2.438 +  have decomp3: "{1..n+1} = {n+1} Un {1..n}"
   2.439 +    by auto
   2.440 +  have "(a+b)^(n+1) = 
   2.441 +      (a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
   2.442 +    using ih by (simp add: power_plus_one)
   2.443 +  also have "... =  a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
   2.444 +                   b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
   2.445 +    by (rule distrib)
   2.446 +  also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
   2.447 +                  (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
   2.448 +    by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
   2.449 +  also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
   2.450 +                  (SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
   2.451 +    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le 
   2.452 +             power_Suc ring_simps One_nat_def del:setsum_cl_ivl_Suc)
   2.453 +  also have "... = a^(n+1) + b^(n+1) +
   2.454 +                  (SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
   2.455 +                  (SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
   2.456 +    by (simp add: decomp2 decomp3)
   2.457 +  also have
   2.458 +      "... = a^(n+1) + b^(n+1) + 
   2.459 +         (SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
   2.460 +    by (auto simp add: ring_simps setsum_addf [symmetric]
   2.461 +      nat_choose_reduce)
   2.462 +  also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
   2.463 +    using decomp by (simp add: ring_simps)
   2.464 +  finally show "?P (n + 1)" by simp
   2.465 +qed
   2.466 +
   2.467 +lemma set_explicit: "{S. S = T \<and> P S} = (if P T then {T} else {})"
   2.468 +  by auto
   2.469 +
   2.470 +lemma nat_card_subsets [rule_format]:
   2.471 +  fixes S :: "'a set"
   2.472 +  assumes "finite S"
   2.473 +  shows "ALL k. card {T. T \<le> S \<and> card T = k} = card S choose k" 
   2.474 +      (is "?P S")
   2.475 +using `finite S`
   2.476 +proof (induct set: finite)
   2.477 +  show "?P {}" by (auto simp add: set_explicit)
   2.478 +  next fix x :: "'a" and F
   2.479 +  assume iassms: "finite F" "x ~: F"
   2.480 +  assume ih: "?P F"
   2.481 +  show "?P (insert x F)" (is "ALL k. ?Q k")
   2.482 +  proof
   2.483 +    fix k
   2.484 +    show "card {T. T \<subseteq> (insert x F) \<and> card T = k} = 
   2.485 +        card (insert x F) choose k" (is "?Q k")
   2.486 +    proof (induct k rule: nat_induct')
   2.487 +      from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
   2.488 +        apply auto
   2.489 +        apply (subst (asm) card_0_eq)
   2.490 +        apply (auto elim: finite_subset)
   2.491 +        done
   2.492 +      thus "?Q 0" 
   2.493 +        by auto
   2.494 +      next fix k
   2.495 +      show "?Q (k + 1)"
   2.496 +      proof -
   2.497 +        from iassms have fin: "finite (insert x F)" by auto
   2.498 +        hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
   2.499 +          {T. T \<le> F & card T = k + 1} Un 
   2.500 +          {T. T \<le> insert x F & x : T & card T = k + 1}"
   2.501 +          by (auto intro!: subsetI)
   2.502 +        with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
   2.503 +          card ({T. T \<subseteq> F \<and> card T = k + 1}) + 
   2.504 +          card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
   2.505 +          apply (subst card_Un_disjoint [symmetric])
   2.506 +          apply auto
   2.507 +          (* note: nice! Didn't have to say anything here *)
   2.508 +          done
   2.509 +        also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) = 
   2.510 +          card F choose (k+1)" by auto
   2.511 +        also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
   2.512 +          card ({T. T <= F & card T = k})"
   2.513 +        proof -
   2.514 +          let ?f = "%T. T Un {x}"
   2.515 +          from iassms have "inj_on ?f {T. T <= F & card T = k}"
   2.516 +            unfolding inj_on_def by (auto intro!: subsetI)
   2.517 +          hence "card ({T. T <= F & card T = k}) = 
   2.518 +            card(?f ` {T. T <= F & card T = k})"
   2.519 +            by (rule card_image [symmetric])
   2.520 +          also from iassms fin have "?f ` {T. T <= F & card T = k} = 
   2.521 +            {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}"
   2.522 +            unfolding image_def 
   2.523 +            (* I can't figure out why this next line takes so long *)
   2.524 +            apply auto
   2.525 +            apply (frule (1) finite_subset, force)
   2.526 +            apply (rule_tac x = "xa - {x}" in exI)
   2.527 +            apply (subst card_Diff_singleton)
   2.528 +            apply (auto elim: finite_subset)
   2.529 +            done
   2.530 +          finally show ?thesis by (rule sym)
   2.531 +        qed
   2.532 +        also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
   2.533 +          by auto
   2.534 +        finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
   2.535 +          card F choose (k + 1) + (card F choose k)".
   2.536 +        with iassms nat_choose_plus_one show ?thesis
   2.537 +          by auto
   2.538 +      qed
   2.539 +    qed
   2.540 +  qed
   2.541 +qed
   2.542 +
   2.543 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/NewNumberTheory/Cong.thy	Fri Jun 19 18:33:10 2009 +0200
     3.3 @@ -0,0 +1,1093 @@
     3.4 +(*  Title:      HOL/Library/Cong.thy
     3.5 +    ID:         
     3.6 +    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     3.7 +                Thomas M. Rasmussen, Jeremy Avigad
     3.8 +
     3.9 +
    3.10 +Defines congruence (notation: [x = y] (mod z)) for natural numbers and
    3.11 +integers.
    3.12 +
    3.13 +This file combines and revises a number of prior developments.
    3.14 +
    3.15 +The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    3.16 +and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    3.17 +gcd, lcm, and prime for the natural numbers.
    3.18 +
    3.19 +The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    3.20 +extended gcd, lcm, primes to the integers. Amine Chaieb provided
    3.21 +another extension of the notions to the integers, and added a number
    3.22 +of results to "Primes" and "GCD". 
    3.23 +
    3.24 +The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
    3.25 +developed the congruence relations on the integers. The notion was
    3.26 +extended to the natural numbers by Chiaeb. Jeremy Avigad combined
    3.27 +these, revised and tidied them, made the development uniform for the
    3.28 +natural numbers and the integers, and added a number of new theorems.
    3.29 +
    3.30 +*)
    3.31 +
    3.32 +
    3.33 +header {* Congruence *}
    3.34 +
    3.35 +theory Cong
    3.36 +imports GCD
    3.37 +begin
    3.38 +
    3.39 +subsection {* Turn off One_nat_def *}
    3.40 +
    3.41 +lemma nat_induct' [case_names zero plus1, induct type: nat]: 
    3.42 +    "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
    3.43 +by (erule nat_induct) (simp add:One_nat_def)
    3.44 +
    3.45 +lemma nat_cases [case_names zero plus1, cases type: nat]: 
    3.46 +    "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
    3.47 +by(metis nat_induct')
    3.48 +
    3.49 +lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
    3.50 +by (simp add: One_nat_def)
    3.51 +
    3.52 +lemma nat_power_eq_one_eq [simp]: 
    3.53 +  "((x::nat)^m = 1) = (m = 0 | x = 1)"
    3.54 +by (induct m, auto)
    3.55 +
    3.56 +lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
    3.57 +  card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
    3.58 +by (auto simp add: insert_absorb)
    3.59 +
    3.60 +(* why wasn't card_insert_if a simp rule? *)
    3.61 +declare card_insert_disjoint [simp del]
    3.62 +
    3.63 +lemma nat_1' [simp]: "nat 1 = 1"
    3.64 +by simp
    3.65 +
    3.66 +(* For those annoying moments where Suc reappears *)
    3.67 +lemma Suc_remove: "Suc n = n + 1"
    3.68 +by simp
    3.69 +
    3.70 +declare nat_1 [simp del]
    3.71 +declare add_2_eq_Suc [simp del] 
    3.72 +declare add_2_eq_Suc' [simp del]
    3.73 +
    3.74 +
    3.75 +declare mod_pos_pos_trivial [simp]
    3.76 +
    3.77 +
    3.78 +subsection {* Main definitions *}
    3.79 +
    3.80 +class cong =
    3.81 +
    3.82 +fixes 
    3.83 +  cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
    3.84 +
    3.85 +begin
    3.86 +
    3.87 +abbreviation
    3.88 +  notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
    3.89 +where
    3.90 +  "notcong x y m == (~cong x y m)" 
    3.91 +
    3.92 +end
    3.93 +
    3.94 +(* definitions for the natural numbers *)
    3.95 +
    3.96 +instantiation nat :: cong
    3.97 +
    3.98 +begin 
    3.99 +
   3.100 +definition 
   3.101 +  cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
   3.102 +where 
   3.103 +  "cong_nat x y m = ((x mod m) = (y mod m))"
   3.104 +
   3.105 +instance proof qed
   3.106 +
   3.107 +end
   3.108 +
   3.109 +
   3.110 +(* definitions for the integers *)
   3.111 +
   3.112 +instantiation int :: cong
   3.113 +
   3.114 +begin 
   3.115 +
   3.116 +definition 
   3.117 +  cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
   3.118 +where 
   3.119 +  "cong_int x y m = ((x mod m) = (y mod m))"
   3.120 +
   3.121 +instance proof qed
   3.122 +
   3.123 +end
   3.124 +
   3.125 +
   3.126 +subsection {* Set up Transfer *}
   3.127 +
   3.128 +
   3.129 +lemma transfer_nat_int_cong:
   3.130 +  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 
   3.131 +    ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
   3.132 +  unfolding cong_int_def cong_nat_def 
   3.133 +  apply (auto simp add: nat_mod_distrib [symmetric])
   3.134 +  apply (subst (asm) eq_nat_nat_iff)
   3.135 +  apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
   3.136 +  apply assumption
   3.137 +done
   3.138 +
   3.139 +declare TransferMorphism_nat_int[transfer add return: 
   3.140 +    transfer_nat_int_cong]
   3.141 +
   3.142 +lemma transfer_int_nat_cong:
   3.143 +  "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
   3.144 +  apply (auto simp add: cong_int_def cong_nat_def)
   3.145 +  apply (auto simp add: zmod_int [symmetric])
   3.146 +done
   3.147 +
   3.148 +declare TransferMorphism_int_nat[transfer add return: 
   3.149 +    transfer_int_nat_cong]
   3.150 +
   3.151 +
   3.152 +subsection {* Congruence *}
   3.153 +
   3.154 +(* was zcong_0, etc. *)
   3.155 +lemma nat_cong_0 [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
   3.156 +  by (unfold cong_nat_def, auto)
   3.157 +
   3.158 +lemma int_cong_0 [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
   3.159 +  by (unfold cong_int_def, auto)
   3.160 +
   3.161 +lemma nat_cong_1 [simp, presburger]: "[(a::nat) = b] (mod 1)"
   3.162 +  by (unfold cong_nat_def, auto)
   3.163 +
   3.164 +lemma nat_cong_Suc_0 [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
   3.165 +  by (unfold cong_nat_def, auto simp add: One_nat_def)
   3.166 +
   3.167 +lemma int_cong_1 [simp, presburger]: "[(a::int) = b] (mod 1)"
   3.168 +  by (unfold cong_int_def, auto)
   3.169 +
   3.170 +lemma nat_cong_refl [simp]: "[(k::nat) = k] (mod m)"
   3.171 +  by (unfold cong_nat_def, auto)
   3.172 +
   3.173 +lemma int_cong_refl [simp]: "[(k::int) = k] (mod m)"
   3.174 +  by (unfold cong_int_def, auto)
   3.175 +
   3.176 +lemma nat_cong_sym: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   3.177 +  by (unfold cong_nat_def, auto)
   3.178 +
   3.179 +lemma int_cong_sym: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
   3.180 +  by (unfold cong_int_def, auto)
   3.181 +
   3.182 +lemma nat_cong_sym_eq: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
   3.183 +  by (unfold cong_nat_def, auto)
   3.184 +
   3.185 +lemma int_cong_sym_eq: "[(a::int) = b] (mod m) = [b = a] (mod m)"
   3.186 +  by (unfold cong_int_def, auto)
   3.187 +
   3.188 +lemma nat_cong_trans [trans]:
   3.189 +    "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   3.190 +  by (unfold cong_nat_def, auto)
   3.191 +
   3.192 +lemma int_cong_trans [trans]:
   3.193 +    "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
   3.194 +  by (unfold cong_int_def, auto)
   3.195 +
   3.196 +lemma nat_cong_add:
   3.197 +    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   3.198 +  apply (unfold cong_nat_def)
   3.199 +  apply (subst (1 2) mod_add_eq)
   3.200 +  apply simp
   3.201 +done
   3.202 +
   3.203 +lemma int_cong_add:
   3.204 +    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
   3.205 +  apply (unfold cong_int_def)
   3.206 +  apply (subst (1 2) mod_add_left_eq)
   3.207 +  apply (subst (1 2) mod_add_right_eq)
   3.208 +  apply simp
   3.209 +done
   3.210 +
   3.211 +lemma int_cong_diff:
   3.212 +    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
   3.213 +  apply (unfold cong_int_def)
   3.214 +  apply (subst (1 2) mod_diff_eq)
   3.215 +  apply simp
   3.216 +done
   3.217 +
   3.218 +lemma int_cong_diff_aux:
   3.219 +  "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> 
   3.220 +      [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
   3.221 +  apply (subst (1 2) tsub_eq)
   3.222 +  apply (auto intro: int_cong_diff)
   3.223 +done;
   3.224 +
   3.225 +lemma nat_cong_diff:
   3.226 +  assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
   3.227 +    "[c = d] (mod m)"
   3.228 +  shows "[a - c = b - d] (mod m)"
   3.229 +
   3.230 +  using prems by (rule int_cong_diff_aux [transferred]);
   3.231 +
   3.232 +lemma nat_cong_mult:
   3.233 +    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   3.234 +  apply (unfold cong_nat_def)
   3.235 +  apply (subst (1 2) mod_mult_eq)
   3.236 +  apply simp
   3.237 +done
   3.238 +
   3.239 +lemma int_cong_mult:
   3.240 +    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
   3.241 +  apply (unfold cong_int_def)
   3.242 +  apply (subst (1 2) zmod_zmult1_eq)
   3.243 +  apply (subst (1 2) mult_commute)
   3.244 +  apply (subst (1 2) zmod_zmult1_eq)
   3.245 +  apply simp
   3.246 +done
   3.247 +
   3.248 +lemma nat_cong_exp: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   3.249 +  apply (induct k)
   3.250 +  apply (auto simp add: nat_cong_refl nat_cong_mult)
   3.251 +done
   3.252 +
   3.253 +lemma int_cong_exp: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
   3.254 +  apply (induct k)
   3.255 +  apply (auto simp add: int_cong_refl int_cong_mult)
   3.256 +done
   3.257 +
   3.258 +lemma nat_cong_setsum [rule_format]: 
   3.259 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
   3.260 +      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
   3.261 +  apply (case_tac "finite A")
   3.262 +  apply (induct set: finite)
   3.263 +  apply (auto intro: nat_cong_add)
   3.264 +done
   3.265 +
   3.266 +lemma int_cong_setsum [rule_format]:
   3.267 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
   3.268 +      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
   3.269 +  apply (case_tac "finite A")
   3.270 +  apply (induct set: finite)
   3.271 +  apply (auto intro: int_cong_add)
   3.272 +done
   3.273 +
   3.274 +lemma nat_cong_setprod [rule_format]: 
   3.275 +    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
   3.276 +      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
   3.277 +  apply (case_tac "finite A")
   3.278 +  apply (induct set: finite)
   3.279 +  apply (auto intro: nat_cong_mult)
   3.280 +done
   3.281 +
   3.282 +lemma int_cong_setprod [rule_format]: 
   3.283 +    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
   3.284 +      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
   3.285 +  apply (case_tac "finite A")
   3.286 +  apply (induct set: finite)
   3.287 +  apply (auto intro: int_cong_mult)
   3.288 +done
   3.289 +
   3.290 +lemma nat_cong_scalar: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   3.291 +  by (rule nat_cong_mult, simp_all)
   3.292 +
   3.293 +lemma int_cong_scalar: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
   3.294 +  by (rule int_cong_mult, simp_all)
   3.295 +
   3.296 +lemma nat_cong_scalar2: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   3.297 +  by (rule nat_cong_mult, simp_all)
   3.298 +
   3.299 +lemma int_cong_scalar2: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
   3.300 +  by (rule int_cong_mult, simp_all)
   3.301 +
   3.302 +lemma nat_cong_mult_self: "[(a::nat) * m = 0] (mod m)"
   3.303 +  by (unfold cong_nat_def, auto)
   3.304 +
   3.305 +lemma int_cong_mult_self: "[(a::int) * m = 0] (mod m)"
   3.306 +  by (unfold cong_int_def, auto)
   3.307 +
   3.308 +lemma int_cong_eq_diff_cong_0: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
   3.309 +  apply (rule iffI)
   3.310 +  apply (erule int_cong_diff [of a b m b b, simplified])
   3.311 +  apply (erule int_cong_add [of "a - b" 0 m b b, simplified])
   3.312 +done
   3.313 +
   3.314 +lemma int_cong_eq_diff_cong_0_aux: "a >= b \<Longrightarrow>
   3.315 +    [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
   3.316 +  by (subst tsub_eq, assumption, rule int_cong_eq_diff_cong_0)
   3.317 +
   3.318 +lemma nat_cong_eq_diff_cong_0:
   3.319 +  assumes "(a::nat) >= b"
   3.320 +  shows "[a = b] (mod m) = [a - b = 0] (mod m)"
   3.321 +
   3.322 +  using prems by (rule int_cong_eq_diff_cong_0_aux [transferred])
   3.323 +
   3.324 +lemma nat_cong_diff_cong_0': 
   3.325 +  "[(x::nat) = y] (mod n) \<longleftrightarrow> 
   3.326 +    (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
   3.327 +  apply (case_tac "y <= x")
   3.328 +  apply (frule nat_cong_eq_diff_cong_0 [where m = n])
   3.329 +  apply auto [1]
   3.330 +  apply (subgoal_tac "x <= y")
   3.331 +  apply (frule nat_cong_eq_diff_cong_0 [where m = n])
   3.332 +  apply (subst nat_cong_sym_eq)
   3.333 +  apply auto
   3.334 +done
   3.335 +
   3.336 +lemma nat_cong_altdef: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
   3.337 +  apply (subst nat_cong_eq_diff_cong_0, assumption)
   3.338 +  apply (unfold cong_nat_def)
   3.339 +  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   3.340 +done
   3.341 +
   3.342 +lemma int_cong_altdef: "[(a::int) = b] (mod m) = (m dvd (a - b))"
   3.343 +  apply (subst int_cong_eq_diff_cong_0)
   3.344 +  apply (unfold cong_int_def)
   3.345 +  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
   3.346 +done
   3.347 +
   3.348 +lemma int_cong_abs: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
   3.349 +  by (simp add: int_cong_altdef)
   3.350 +
   3.351 +lemma int_cong_square:
   3.352 +   "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
   3.353 +    \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
   3.354 +  apply (simp only: int_cong_altdef)
   3.355 +  apply (subst int_prime_dvd_mult_eq [symmetric], assumption)
   3.356 +  (* any way around this? *)
   3.357 +  apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
   3.358 +  apply (auto simp add: ring_simps)
   3.359 +done
   3.360 +
   3.361 +lemma int_cong_mult_rcancel:
   3.362 +  "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
   3.363 +  apply (subst (1 2) int_cong_altdef)
   3.364 +  apply (subst left_diff_distrib [symmetric])
   3.365 +  apply (rule int_coprime_dvd_mult_iff)
   3.366 +  apply (subst int_gcd_commute, assumption)
   3.367 +done
   3.368 +
   3.369 +lemma nat_cong_mult_rcancel:
   3.370 +  assumes  "coprime k (m::nat)"
   3.371 +  shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
   3.372 +
   3.373 +  apply (rule int_cong_mult_rcancel [transferred])
   3.374 +  using prems apply auto
   3.375 +done
   3.376 +
   3.377 +lemma nat_cong_mult_lcancel:
   3.378 +  "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
   3.379 +  by (simp add: mult_commute nat_cong_mult_rcancel)
   3.380 +
   3.381 +lemma int_cong_mult_lcancel:
   3.382 +  "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
   3.383 +  by (simp add: mult_commute int_cong_mult_rcancel)
   3.384 +
   3.385 +(* was zcong_zgcd_zmult_zmod *)
   3.386 +lemma int_coprime_cong_mult:
   3.387 +  "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
   3.388 +    \<Longrightarrow> [a = b] (mod m * n)"
   3.389 +  apply (simp only: int_cong_altdef)
   3.390 +  apply (erule (2) int_divides_mult)
   3.391 +done
   3.392 +
   3.393 +lemma nat_coprime_cong_mult:
   3.394 +  assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
   3.395 +  shows "[a = b] (mod m * n)"
   3.396 +
   3.397 +  apply (rule int_coprime_cong_mult [transferred])
   3.398 +  using prems apply auto
   3.399 +done
   3.400 +
   3.401 +lemma nat_cong_less_imp_eq: "0 \<le> (a::nat) \<Longrightarrow>
   3.402 +    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   3.403 +  by (auto simp add: cong_nat_def mod_pos_pos_trivial)
   3.404 +
   3.405 +lemma int_cong_less_imp_eq: "0 \<le> (a::int) \<Longrightarrow>
   3.406 +    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
   3.407 +  by (auto simp add: cong_int_def mod_pos_pos_trivial)
   3.408 +
   3.409 +lemma nat_cong_less_unique:
   3.410 +    "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   3.411 +  apply auto
   3.412 +  apply (rule_tac x = "a mod m" in exI)
   3.413 +  apply (unfold cong_nat_def, auto)
   3.414 +done
   3.415 +
   3.416 +lemma int_cong_less_unique:
   3.417 +    "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
   3.418 +  apply auto
   3.419 +  apply (rule_tac x = "a mod m" in exI)
   3.420 +  apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
   3.421 +done
   3.422 +
   3.423 +lemma int_cong_iff_lin: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
   3.424 +  apply (auto simp add: int_cong_altdef dvd_def ring_simps)
   3.425 +  apply (rule_tac [!] x = "-k" in exI, auto)
   3.426 +done
   3.427 +
   3.428 +lemma nat_cong_iff_lin: "([(a::nat) = b] (mod m)) = 
   3.429 +    (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   3.430 +  apply (rule iffI)
   3.431 +  apply (case_tac "b <= a")
   3.432 +  apply (subst (asm) nat_cong_altdef, assumption)
   3.433 +  apply (unfold dvd_def, auto)
   3.434 +  apply (rule_tac x = k in exI)
   3.435 +  apply (rule_tac x = 0 in exI)
   3.436 +  apply (auto simp add: ring_simps)
   3.437 +  apply (subst (asm) nat_cong_sym_eq)
   3.438 +  apply (subst (asm) nat_cong_altdef)
   3.439 +  apply force
   3.440 +  apply (unfold dvd_def, auto)
   3.441 +  apply (rule_tac x = 0 in exI)
   3.442 +  apply (rule_tac x = k in exI)
   3.443 +  apply (auto simp add: ring_simps)
   3.444 +  apply (unfold cong_nat_def)
   3.445 +  apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
   3.446 +  apply (erule ssubst)back
   3.447 +  apply (erule subst)
   3.448 +  apply auto
   3.449 +done
   3.450 +
   3.451 +lemma int_cong_gcd_eq: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
   3.452 +  apply (subst (asm) int_cong_iff_lin, auto)
   3.453 +  apply (subst add_commute) 
   3.454 +  apply (subst (2) int_gcd_commute)
   3.455 +  apply (subst mult_commute)
   3.456 +  apply (subst int_gcd_add_mult)
   3.457 +  apply (rule int_gcd_commute)
   3.458 +done
   3.459 +
   3.460 +lemma nat_cong_gcd_eq: 
   3.461 +  assumes "[(a::nat) = b] (mod m)"
   3.462 +  shows "gcd a m = gcd b m"
   3.463 +
   3.464 +  apply (rule int_cong_gcd_eq [transferred])
   3.465 +  using prems apply auto
   3.466 +done
   3.467 +
   3.468 +lemma nat_cong_imp_coprime: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
   3.469 +    coprime b m"
   3.470 +  by (auto simp add: nat_cong_gcd_eq)
   3.471 +
   3.472 +lemma int_cong_imp_coprime: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
   3.473 +    coprime b m"
   3.474 +  by (auto simp add: int_cong_gcd_eq)
   3.475 +
   3.476 +lemma nat_cong_cong_mod: "[(a::nat) = b] (mod m) = 
   3.477 +    [a mod m = b mod m] (mod m)"
   3.478 +  by (auto simp add: cong_nat_def)
   3.479 +
   3.480 +lemma int_cong_cong_mod: "[(a::int) = b] (mod m) = 
   3.481 +    [a mod m = b mod m] (mod m)"
   3.482 +  by (auto simp add: cong_int_def)
   3.483 +
   3.484 +lemma int_cong_minus [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
   3.485 +  by (subst (1 2) int_cong_altdef, auto)
   3.486 +
   3.487 +lemma nat_cong_zero [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
   3.488 +  by (auto simp add: cong_nat_def)
   3.489 +
   3.490 +lemma int_cong_zero [iff]: "[(a::int) = b] (mod 0) = (a = b)"
   3.491 +  by (auto simp add: cong_int_def)
   3.492 +
   3.493 +(*
   3.494 +lemma int_mod_dvd_mod:
   3.495 +    "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
   3.496 +  apply (unfold dvd_def, auto)
   3.497 +  apply (rule mod_mod_cancel)
   3.498 +  apply auto
   3.499 +done
   3.500 +
   3.501 +lemma mod_dvd_mod:
   3.502 +  assumes "0 < (m::nat)" and "m dvd b"
   3.503 +  shows "(a mod b mod m) = (a mod m)"
   3.504 +
   3.505 +  apply (rule int_mod_dvd_mod [transferred])
   3.506 +  using prems apply auto
   3.507 +done
   3.508 +*)
   3.509 +
   3.510 +lemma nat_cong_add_lcancel: 
   3.511 +    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
   3.512 +  by (simp add: nat_cong_iff_lin)
   3.513 +
   3.514 +lemma int_cong_add_lcancel: 
   3.515 +    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
   3.516 +  by (simp add: int_cong_iff_lin)
   3.517 +
   3.518 +lemma nat_cong_add_rcancel: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   3.519 +  by (simp add: nat_cong_iff_lin)
   3.520 +
   3.521 +lemma int_cong_add_rcancel: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   3.522 +  by (simp add: int_cong_iff_lin)
   3.523 +
   3.524 +lemma nat_cong_add_lcancel_0: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   3.525 +  by (simp add: nat_cong_iff_lin)
   3.526 +
   3.527 +lemma int_cong_add_lcancel_0: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   3.528 +  by (simp add: int_cong_iff_lin)
   3.529 +
   3.530 +lemma nat_cong_add_rcancel_0: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   3.531 +  by (simp add: nat_cong_iff_lin)
   3.532 +
   3.533 +lemma int_cong_add_rcancel_0: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
   3.534 +  by (simp add: int_cong_iff_lin)
   3.535 +
   3.536 +lemma nat_cong_dvd_modulus: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   3.537 +    [x = y] (mod n)"
   3.538 +  apply (auto simp add: nat_cong_iff_lin dvd_def)
   3.539 +  apply (rule_tac x="k1 * k" in exI)
   3.540 +  apply (rule_tac x="k2 * k" in exI)
   3.541 +  apply (simp add: ring_simps)
   3.542 +done
   3.543 +
   3.544 +lemma int_cong_dvd_modulus: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
   3.545 +    [x = y] (mod n)"
   3.546 +  by (auto simp add: int_cong_altdef dvd_def)
   3.547 +
   3.548 +lemma nat_cong_dvd_eq: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   3.549 +  by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
   3.550 +
   3.551 +lemma int_cong_dvd_eq: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
   3.552 +  by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
   3.553 +
   3.554 +lemma nat_cong_mod: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
   3.555 +  by (simp add: cong_nat_def)
   3.556 +
   3.557 +lemma int_cong_mod: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
   3.558 +  by (simp add: cong_int_def)
   3.559 +
   3.560 +lemma nat_mod_mult_cong: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 
   3.561 +    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   3.562 +  by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
   3.563 +
   3.564 +lemma int_neg_cong: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
   3.565 +  apply (simp add: int_cong_altdef)
   3.566 +  apply (subst dvd_minus_iff [symmetric])
   3.567 +  apply (simp add: ring_simps)
   3.568 +done
   3.569 +
   3.570 +lemma int_cong_modulus_neg: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   3.571 +  by (auto simp add: int_cong_altdef)
   3.572 +
   3.573 +lemma int_mod_mult_cong: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
   3.574 +    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
   3.575 +  apply (case_tac "b > 0")
   3.576 +  apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
   3.577 +  apply (subst (1 2) int_cong_modulus_neg)
   3.578 +  apply (unfold cong_int_def)
   3.579 +  apply (subgoal_tac "a * b = (-a * -b)")
   3.580 +  apply (erule ssubst)
   3.581 +  apply (subst zmod_zmult2_eq)
   3.582 +  apply (auto simp add: mod_add_left_eq) 
   3.583 +done
   3.584 +
   3.585 +lemma nat_cong_to_1: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
   3.586 +  apply (case_tac "a = 0")
   3.587 +  apply force
   3.588 +  apply (subst (asm) nat_cong_altdef)
   3.589 +  apply auto
   3.590 +done
   3.591 +
   3.592 +lemma nat_0_cong_1: "[(0::nat) = 1] (mod n) = (n = 1)"
   3.593 +  by (unfold cong_nat_def, auto)
   3.594 +
   3.595 +lemma int_0_cong_1: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
   3.596 +  by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
   3.597 +
   3.598 +lemma nat_cong_to_1': "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
   3.599 +    a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
   3.600 +  apply (case_tac "n = 1")
   3.601 +  apply auto [1]
   3.602 +  apply (drule_tac x = "a - 1" in spec)
   3.603 +  apply force
   3.604 +  apply (case_tac "a = 0")
   3.605 +  apply (auto simp add: nat_0_cong_1) [1]
   3.606 +  apply (rule iffI)
   3.607 +  apply (drule nat_cong_to_1)
   3.608 +  apply (unfold dvd_def)
   3.609 +  apply auto [1]
   3.610 +  apply (rule_tac x = k in exI)
   3.611 +  apply (auto simp add: ring_simps) [1]
   3.612 +  apply (subst nat_cong_altdef)
   3.613 +  apply (auto simp add: dvd_def)
   3.614 +done
   3.615 +
   3.616 +lemma nat_cong_le: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   3.617 +  apply (subst nat_cong_altdef)
   3.618 +  apply assumption
   3.619 +  apply (unfold dvd_def, auto simp add: ring_simps)
   3.620 +  apply (rule_tac x = k in exI)
   3.621 +  apply auto
   3.622 +done
   3.623 +
   3.624 +lemma nat_cong_solve: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   3.625 +  apply (case_tac "n = 0")
   3.626 +  apply force
   3.627 +  apply (frule nat_bezout [of a n], auto)
   3.628 +  apply (rule exI, erule ssubst)
   3.629 +  apply (rule nat_cong_trans)
   3.630 +  apply (rule nat_cong_add)
   3.631 +  apply (subst mult_commute)
   3.632 +  apply (rule nat_cong_mult_self)
   3.633 +  prefer 2
   3.634 +  apply simp
   3.635 +  apply (rule nat_cong_refl)
   3.636 +  apply (rule nat_cong_refl)
   3.637 +done
   3.638 +
   3.639 +lemma int_cong_solve: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   3.640 +  apply (case_tac "n = 0")
   3.641 +  apply (case_tac "a \<ge> 0")
   3.642 +  apply auto
   3.643 +  apply (rule_tac x = "-1" in exI)
   3.644 +  apply auto
   3.645 +  apply (insert int_bezout [of a n], auto)
   3.646 +  apply (rule exI)
   3.647 +  apply (erule subst)
   3.648 +  apply (rule int_cong_trans)
   3.649 +  prefer 2
   3.650 +  apply (rule int_cong_add)
   3.651 +  apply (rule int_cong_refl)
   3.652 +  apply (rule int_cong_sym)
   3.653 +  apply (rule int_cong_mult_self)
   3.654 +  apply simp
   3.655 +  apply (subst mult_commute)
   3.656 +  apply (rule int_cong_refl)
   3.657 +done
   3.658 +  
   3.659 +lemma nat_cong_solve_dvd: 
   3.660 +  assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
   3.661 +  shows "EX x. [a * x = d] (mod n)"
   3.662 +proof -
   3.663 +  from nat_cong_solve [OF a] obtain x where 
   3.664 +      "[a * x = gcd a n](mod n)"
   3.665 +    by auto
   3.666 +  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
   3.667 +    by (elim nat_cong_scalar2)
   3.668 +  also from b have "(d div gcd a n) * gcd a n = d"
   3.669 +    by (rule dvd_div_mult_self)
   3.670 +  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   3.671 +    by auto
   3.672 +  finally show ?thesis
   3.673 +    by auto
   3.674 +qed
   3.675 +
   3.676 +lemma int_cong_solve_dvd: 
   3.677 +  assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
   3.678 +  shows "EX x. [a * x = d] (mod n)"
   3.679 +proof -
   3.680 +  from int_cong_solve [OF a] obtain x where 
   3.681 +      "[a * x = gcd a n](mod n)"
   3.682 +    by auto
   3.683 +  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
   3.684 +    by (elim int_cong_scalar2)
   3.685 +  also from b have "(d div gcd a n) * gcd a n = d"
   3.686 +    by (rule dvd_div_mult_self)
   3.687 +  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
   3.688 +    by auto
   3.689 +  finally show ?thesis
   3.690 +    by auto
   3.691 +qed
   3.692 +
   3.693 +lemma nat_cong_solve_coprime: "coprime (a::nat) n \<Longrightarrow> 
   3.694 +    EX x. [a * x = 1] (mod n)"
   3.695 +  apply (case_tac "a = 0")
   3.696 +  apply force
   3.697 +  apply (frule nat_cong_solve [of a n])
   3.698 +  apply auto
   3.699 +done
   3.700 +
   3.701 +lemma int_cong_solve_coprime: "coprime (a::int) n \<Longrightarrow> 
   3.702 +    EX x. [a * x = 1] (mod n)"
   3.703 +  apply (case_tac "a = 0")
   3.704 +  apply auto
   3.705 +  apply (case_tac "n \<ge> 0")
   3.706 +  apply auto
   3.707 +  apply (subst cong_int_def, auto)
   3.708 +  apply (frule int_cong_solve [of a n])
   3.709 +  apply auto
   3.710 +done
   3.711 +
   3.712 +lemma nat_coprime_iff_invertible: "m > (1::nat) \<Longrightarrow> coprime a m = 
   3.713 +    (EX x. [a * x = 1] (mod m))"
   3.714 +  apply (auto intro: nat_cong_solve_coprime)
   3.715 +  apply (unfold cong_nat_def, auto intro: nat_invertible_coprime)
   3.716 +done
   3.717 +
   3.718 +lemma int_coprime_iff_invertible: "m > (1::int) \<Longrightarrow> coprime a m = 
   3.719 +    (EX x. [a * x = 1] (mod m))"
   3.720 +  apply (auto intro: int_cong_solve_coprime)
   3.721 +  apply (unfold cong_int_def)
   3.722 +  apply (auto intro: int_invertible_coprime)
   3.723 +done
   3.724 +
   3.725 +lemma int_coprime_iff_invertible': "m > (1::int) \<Longrightarrow> coprime a m = 
   3.726 +    (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
   3.727 +  apply (subst int_coprime_iff_invertible)
   3.728 +  apply auto
   3.729 +  apply (auto simp add: cong_int_def)
   3.730 +  apply (rule_tac x = "x mod m" in exI)
   3.731 +  apply (auto simp add: mod_mult_right_eq [symmetric])
   3.732 +done
   3.733 +
   3.734 +
   3.735 +lemma nat_cong_cong_lcm: "[(x::nat) = y] (mod a) \<Longrightarrow>
   3.736 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   3.737 +  apply (case_tac "y \<le> x")
   3.738 +  apply (auto simp add: nat_cong_altdef nat_lcm_least) [1]
   3.739 +  apply (rule nat_cong_sym)
   3.740 +  apply (subst (asm) (1 2) nat_cong_sym_eq)
   3.741 +  apply (auto simp add: nat_cong_altdef nat_lcm_least)
   3.742 +done
   3.743 +
   3.744 +lemma int_cong_cong_lcm: "[(x::int) = y] (mod a) \<Longrightarrow>
   3.745 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   3.746 +  by (auto simp add: int_cong_altdef int_lcm_least) [1]
   3.747 +
   3.748 +lemma nat_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
   3.749 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
   3.750 +  apply (frule (1) nat_cong_cong_lcm)back
   3.751 +  apply (simp add: lcm_nat_def)
   3.752 +done
   3.753 +
   3.754 +lemma int_cong_cong_coprime: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
   3.755 +    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
   3.756 +  apply (frule (1) int_cong_cong_lcm)back
   3.757 +  apply (simp add: int_lcm_altdef int_cong_abs abs_mult [symmetric])
   3.758 +done
   3.759 +
   3.760 +lemma nat_cong_cong_setprod_coprime [rule_format]: "finite A \<Longrightarrow>
   3.761 +    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   3.762 +    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
   3.763 +      [x = y] (mod (PROD i:A. m i))"
   3.764 +  apply (induct set: finite)
   3.765 +  apply auto
   3.766 +  apply (rule nat_cong_cong_coprime)
   3.767 +  apply (subst nat_gcd_commute)
   3.768 +  apply (rule nat_setprod_coprime)
   3.769 +  apply auto
   3.770 +done
   3.771 +
   3.772 +lemma int_cong_cong_setprod_coprime [rule_format]: "finite A \<Longrightarrow>
   3.773 +    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
   3.774 +    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
   3.775 +      [x = y] (mod (PROD i:A. m i))"
   3.776 +  apply (induct set: finite)
   3.777 +  apply auto
   3.778 +  apply (rule int_cong_cong_coprime)
   3.779 +  apply (subst int_gcd_commute)
   3.780 +  apply (rule int_setprod_coprime)
   3.781 +  apply auto
   3.782 +done
   3.783 +
   3.784 +lemma nat_binary_chinese_remainder_aux: 
   3.785 +  assumes a: "coprime (m1::nat) m2"
   3.786 +  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   3.787 +    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   3.788 +proof -
   3.789 +  from nat_cong_solve_coprime [OF a]
   3.790 +      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   3.791 +    by auto
   3.792 +  from a have b: "coprime m2 m1" 
   3.793 +    by (subst nat_gcd_commute)
   3.794 +  from nat_cong_solve_coprime [OF b]
   3.795 +      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   3.796 +    by auto
   3.797 +  have "[m1 * x1 = 0] (mod m1)"
   3.798 +    by (subst mult_commute, rule nat_cong_mult_self)
   3.799 +  moreover have "[m2 * x2 = 0] (mod m2)"
   3.800 +    by (subst mult_commute, rule nat_cong_mult_self)
   3.801 +  moreover note one two
   3.802 +  ultimately show ?thesis by blast
   3.803 +qed
   3.804 +
   3.805 +lemma int_binary_chinese_remainder_aux: 
   3.806 +  assumes a: "coprime (m1::int) m2"
   3.807 +  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
   3.808 +    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
   3.809 +proof -
   3.810 +  from int_cong_solve_coprime [OF a]
   3.811 +      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
   3.812 +    by auto
   3.813 +  from a have b: "coprime m2 m1" 
   3.814 +    by (subst int_gcd_commute)
   3.815 +  from int_cong_solve_coprime [OF b]
   3.816 +      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
   3.817 +    by auto
   3.818 +  have "[m1 * x1 = 0] (mod m1)"
   3.819 +    by (subst mult_commute, rule int_cong_mult_self)
   3.820 +  moreover have "[m2 * x2 = 0] (mod m2)"
   3.821 +    by (subst mult_commute, rule int_cong_mult_self)
   3.822 +  moreover note one two
   3.823 +  ultimately show ?thesis by blast
   3.824 +qed
   3.825 +
   3.826 +lemma nat_binary_chinese_remainder:
   3.827 +  assumes a: "coprime (m1::nat) m2"
   3.828 +  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   3.829 +proof -
   3.830 +  from nat_binary_chinese_remainder_aux [OF a] obtain b1 b2
   3.831 +    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   3.832 +          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   3.833 +    by blast
   3.834 +  let ?x = "u1 * b1 + u2 * b2"
   3.835 +  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   3.836 +    apply (rule nat_cong_add)
   3.837 +    apply (rule nat_cong_scalar2)
   3.838 +    apply (rule `[b1 = 1] (mod m1)`)
   3.839 +    apply (rule nat_cong_scalar2)
   3.840 +    apply (rule `[b2 = 0] (mod m1)`)
   3.841 +    done
   3.842 +  hence "[?x = u1] (mod m1)" by simp
   3.843 +  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   3.844 +    apply (rule nat_cong_add)
   3.845 +    apply (rule nat_cong_scalar2)
   3.846 +    apply (rule `[b1 = 0] (mod m2)`)
   3.847 +    apply (rule nat_cong_scalar2)
   3.848 +    apply (rule `[b2 = 1] (mod m2)`)
   3.849 +    done
   3.850 +  hence "[?x = u2] (mod m2)" by simp
   3.851 +  with `[?x = u1] (mod m1)` show ?thesis by blast
   3.852 +qed
   3.853 +
   3.854 +lemma int_binary_chinese_remainder:
   3.855 +  assumes a: "coprime (m1::int) m2"
   3.856 +  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   3.857 +proof -
   3.858 +  from int_binary_chinese_remainder_aux [OF a] obtain b1 b2
   3.859 +    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
   3.860 +          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
   3.861 +    by blast
   3.862 +  let ?x = "u1 * b1 + u2 * b2"
   3.863 +  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
   3.864 +    apply (rule int_cong_add)
   3.865 +    apply (rule int_cong_scalar2)
   3.866 +    apply (rule `[b1 = 1] (mod m1)`)
   3.867 +    apply (rule int_cong_scalar2)
   3.868 +    apply (rule `[b2 = 0] (mod m1)`)
   3.869 +    done
   3.870 +  hence "[?x = u1] (mod m1)" by simp
   3.871 +  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
   3.872 +    apply (rule int_cong_add)
   3.873 +    apply (rule int_cong_scalar2)
   3.874 +    apply (rule `[b1 = 0] (mod m2)`)
   3.875 +    apply (rule int_cong_scalar2)
   3.876 +    apply (rule `[b2 = 1] (mod m2)`)
   3.877 +    done
   3.878 +  hence "[?x = u2] (mod m2)" by simp
   3.879 +  with `[?x = u1] (mod m1)` show ?thesis by blast
   3.880 +qed
   3.881 +
   3.882 +lemma nat_cong_modulus_mult: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
   3.883 +    [x = y] (mod m)"
   3.884 +  apply (case_tac "y \<le> x")
   3.885 +  apply (simp add: nat_cong_altdef)
   3.886 +  apply (erule dvd_mult_left)
   3.887 +  apply (rule nat_cong_sym)
   3.888 +  apply (subst (asm) nat_cong_sym_eq)
   3.889 +  apply (simp add: nat_cong_altdef) 
   3.890 +  apply (erule dvd_mult_left)
   3.891 +done
   3.892 +
   3.893 +lemma int_cong_modulus_mult: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
   3.894 +    [x = y] (mod m)"
   3.895 +  apply (simp add: int_cong_altdef) 
   3.896 +  apply (erule dvd_mult_left)
   3.897 +done
   3.898 +
   3.899 +lemma nat_cong_less_modulus_unique: 
   3.900 +    "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   3.901 +  by (simp add: cong_nat_def)
   3.902 +
   3.903 +lemma nat_binary_chinese_remainder_unique:
   3.904 +  assumes a: "coprime (m1::nat) m2" and
   3.905 +         nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
   3.906 +  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
   3.907 +proof -
   3.908 +  from nat_binary_chinese_remainder [OF a] obtain y where 
   3.909 +      "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
   3.910 +    by blast
   3.911 +  let ?x = "y mod (m1 * m2)"
   3.912 +  from nz have less: "?x < m1 * m2"
   3.913 +    by auto   
   3.914 +  have one: "[?x = u1] (mod m1)"
   3.915 +    apply (rule nat_cong_trans)
   3.916 +    prefer 2
   3.917 +    apply (rule `[y = u1] (mod m1)`)
   3.918 +    apply (rule nat_cong_modulus_mult)
   3.919 +    apply (rule nat_cong_mod)
   3.920 +    using nz apply auto
   3.921 +    done
   3.922 +  have two: "[?x = u2] (mod m2)"
   3.923 +    apply (rule nat_cong_trans)
   3.924 +    prefer 2
   3.925 +    apply (rule `[y = u2] (mod m2)`)
   3.926 +    apply (subst mult_commute)
   3.927 +    apply (rule nat_cong_modulus_mult)
   3.928 +    apply (rule nat_cong_mod)
   3.929 +    using nz apply auto
   3.930 +    done
   3.931 +  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
   3.932 +      z = ?x"
   3.933 +  proof (clarify)
   3.934 +    fix z
   3.935 +    assume "z < m1 * m2"
   3.936 +    assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
   3.937 +    have "[?x = z] (mod m1)"
   3.938 +      apply (rule nat_cong_trans)
   3.939 +      apply (rule `[?x = u1] (mod m1)`)
   3.940 +      apply (rule nat_cong_sym)
   3.941 +      apply (rule `[z = u1] (mod m1)`)
   3.942 +      done
   3.943 +    moreover have "[?x = z] (mod m2)"
   3.944 +      apply (rule nat_cong_trans)
   3.945 +      apply (rule `[?x = u2] (mod m2)`)
   3.946 +      apply (rule nat_cong_sym)
   3.947 +      apply (rule `[z = u2] (mod m2)`)
   3.948 +      done
   3.949 +    ultimately have "[?x = z] (mod m1 * m2)"
   3.950 +      by (auto intro: nat_coprime_cong_mult a)
   3.951 +    with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
   3.952 +      apply (intro nat_cong_less_modulus_unique)
   3.953 +      apply (auto, erule nat_cong_sym)
   3.954 +      done
   3.955 +  qed  
   3.956 +  with less one two show ?thesis
   3.957 +    by auto
   3.958 + qed
   3.959 +
   3.960 +lemma nat_chinese_remainder_aux:
   3.961 +  fixes A :: "'a set" and
   3.962 +        m :: "'a \<Rightarrow> nat"
   3.963 +  assumes fin: "finite A" and
   3.964 +          cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   3.965 +  shows "EX b. (ALL i : A. 
   3.966 +      [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
   3.967 +proof (rule finite_set_choice, rule fin, rule ballI)
   3.968 +  fix i
   3.969 +  assume "i : A"
   3.970 +  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
   3.971 +    by (intro nat_setprod_coprime, auto)
   3.972 +  hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   3.973 +    by (elim nat_cong_solve_coprime)
   3.974 +  then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
   3.975 +    by auto
   3.976 +  moreover have "[(PROD j : A - {i}. m j) * x = 0] 
   3.977 +    (mod (PROD j : A - {i}. m j))"
   3.978 +    by (subst mult_commute, rule nat_cong_mult_self)
   3.979 +  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
   3.980 +      (mod setprod m (A - {i}))"
   3.981 +    by blast
   3.982 +qed
   3.983 +
   3.984 +lemma nat_chinese_remainder:
   3.985 +  fixes A :: "'a set" and
   3.986 +        m :: "'a \<Rightarrow> nat" and
   3.987 +        u :: "'a \<Rightarrow> nat"
   3.988 +  assumes 
   3.989 +        fin: "finite A" and
   3.990 +        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   3.991 +  shows "EX x. (ALL i:A. [x = u i] (mod m i))"
   3.992 +proof -
   3.993 +  from nat_chinese_remainder_aux [OF fin cop] obtain b where
   3.994 +    bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
   3.995 +      [b i = 0] (mod (PROD j : A - {i}. m j))"
   3.996 +    by blast
   3.997 +  let ?x = "SUM i:A. (u i) * (b i)"
   3.998 +  show "?thesis"
   3.999 +  proof (rule exI, clarify)
  3.1000 +    fix i
  3.1001 +    assume a: "i : A"
  3.1002 +    show "[?x = u i] (mod m i)" 
  3.1003 +    proof -
  3.1004 +      from fin a have "?x = (SUM j:{i}. u j * b j) + 
  3.1005 +          (SUM j:A-{i}. u j * b j)"
  3.1006 +        by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
  3.1007 +      hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
  3.1008 +        by auto
  3.1009 +      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
  3.1010 +                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
  3.1011 +        apply (rule nat_cong_add)
  3.1012 +        apply (rule nat_cong_scalar2)
  3.1013 +        using bprop a apply blast
  3.1014 +        apply (rule nat_cong_setsum)
  3.1015 +        apply (rule nat_cong_scalar2)
  3.1016 +        using bprop apply auto
  3.1017 +        apply (rule nat_cong_dvd_modulus)
  3.1018 +        apply (drule (1) bspec)
  3.1019 +        apply (erule conjE)
  3.1020 +        apply assumption
  3.1021 +        apply (rule dvd_setprod)
  3.1022 +        using fin a apply auto
  3.1023 +        done
  3.1024 +      finally show ?thesis
  3.1025 +        by simp
  3.1026 +    qed
  3.1027 +  qed
  3.1028 +qed
  3.1029 +
  3.1030 +lemma nat_coprime_cong_prod [rule_format]: "finite A \<Longrightarrow> 
  3.1031 +    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
  3.1032 +      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
  3.1033 +         [x = y] (mod (PROD i:A. m i))" 
  3.1034 +  apply (induct set: finite)
  3.1035 +  apply auto
  3.1036 +  apply (erule (1) nat_coprime_cong_mult)
  3.1037 +  apply (subst nat_gcd_commute)
  3.1038 +  apply (rule nat_setprod_coprime)
  3.1039 +  apply auto
  3.1040 +done
  3.1041 +
  3.1042 +lemma nat_chinese_remainder_unique:
  3.1043 +  fixes A :: "'a set" and
  3.1044 +        m :: "'a \<Rightarrow> nat" and
  3.1045 +        u :: "'a \<Rightarrow> nat"
  3.1046 +  assumes 
  3.1047 +        fin: "finite A" and
  3.1048 +         nz: "ALL i:A. m i \<noteq> 0" and
  3.1049 +        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
  3.1050 +  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
  3.1051 +proof -
  3.1052 +  from nat_chinese_remainder [OF fin cop] obtain y where
  3.1053 +      one: "(ALL i:A. [y = u i] (mod m i))" 
  3.1054 +    by blast
  3.1055 +  let ?x = "y mod (PROD i:A. m i)"
  3.1056 +  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
  3.1057 +    by auto
  3.1058 +  hence less: "?x < (PROD i:A. m i)"
  3.1059 +    by auto
  3.1060 +  have cong: "ALL i:A. [?x = u i] (mod m i)"
  3.1061 +    apply auto
  3.1062 +    apply (rule nat_cong_trans)
  3.1063 +    prefer 2
  3.1064 +    using one apply auto
  3.1065 +    apply (rule nat_cong_dvd_modulus)
  3.1066 +    apply (rule nat_cong_mod)
  3.1067 +    using prodnz apply auto
  3.1068 +    apply (rule dvd_setprod)
  3.1069 +    apply (rule fin)
  3.1070 +    apply assumption
  3.1071 +    done
  3.1072 +  have unique: "ALL z. z < (PROD i:A. m i) \<and> 
  3.1073 +      (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
  3.1074 +  proof (clarify)
  3.1075 +    fix z
  3.1076 +    assume zless: "z < (PROD i:A. m i)"
  3.1077 +    assume zcong: "(ALL i:A. [z = u i] (mod m i))"
  3.1078 +    have "ALL i:A. [?x = z] (mod m i)"
  3.1079 +      apply clarify     
  3.1080 +      apply (rule nat_cong_trans)
  3.1081 +      using cong apply (erule bspec)
  3.1082 +      apply (rule nat_cong_sym)
  3.1083 +      using zcong apply auto
  3.1084 +      done
  3.1085 +    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
  3.1086 +      by (intro nat_coprime_cong_prod, auto)
  3.1087 +    with zless less show "z = ?x"
  3.1088 +      apply (intro nat_cong_less_modulus_unique)
  3.1089 +      apply (auto, erule nat_cong_sym)
  3.1090 +      done
  3.1091 +  qed 
  3.1092 +  from less cong unique show ?thesis
  3.1093 +    by blast  
  3.1094 +qed
  3.1095 +
  3.1096 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/NewNumberTheory/Fib.thy	Fri Jun 19 18:33:10 2009 +0200
     4.3 @@ -0,0 +1,319 @@
     4.4 +(*  Title:      Fib.thy
     4.5 +    Authors:    Lawrence C. Paulson, Jeremy Avigad
     4.6 +
     4.7 +
     4.8 +Defines the fibonacci function.
     4.9 +
    4.10 +The original "Fib" is due to Lawrence C. Paulson, and was adapted by
    4.11 +Jeremy Avigad.
    4.12 +*)
    4.13 +
    4.14 +
    4.15 +header {* Fib *}
    4.16 +
    4.17 +theory Fib
    4.18 +imports Binomial
    4.19 +begin
    4.20 +
    4.21 +
    4.22 +subsection {* Main definitions *}
    4.23 +
    4.24 +class fib =
    4.25 +
    4.26 +fixes 
    4.27 +  fib :: "'a \<Rightarrow> 'a"
    4.28 +
    4.29 +
    4.30 +(* definition for the natural numbers *)
    4.31 +
    4.32 +instantiation nat :: fib
    4.33 +
    4.34 +begin 
    4.35 +
    4.36 +fun 
    4.37 +  fib_nat :: "nat \<Rightarrow> nat"
    4.38 +where
    4.39 +  "fib_nat n =
    4.40 +   (if n = 0 then 0 else
    4.41 +   (if n = 1 then 1 else
    4.42 +     fib (n - 1) + fib (n - 2)))"
    4.43 +
    4.44 +instance proof qed
    4.45 +
    4.46 +end
    4.47 +
    4.48 +(* definition for the integers *)
    4.49 +
    4.50 +instantiation int :: fib
    4.51 +
    4.52 +begin 
    4.53 +
    4.54 +definition
    4.55 +  fib_int :: "int \<Rightarrow> int"
    4.56 +where  
    4.57 +  "fib_int n = (if n >= 0 then int (fib (nat n)) else 0)"
    4.58 +
    4.59 +instance proof qed
    4.60 +
    4.61 +end
    4.62 +
    4.63 +
    4.64 +subsection {* Set up Transfer *}
    4.65 +
    4.66 +
    4.67 +lemma transfer_nat_int_fib:
    4.68 +  "(x::int) >= 0 \<Longrightarrow> fib (nat x) = nat (fib x)"
    4.69 +  unfolding fib_int_def by auto
    4.70 +
    4.71 +lemma transfer_nat_int_fib_closure:
    4.72 +  "n >= (0::int) \<Longrightarrow> fib n >= 0"
    4.73 +  by (auto simp add: fib_int_def)
    4.74 +
    4.75 +declare TransferMorphism_nat_int[transfer add return: 
    4.76 +    transfer_nat_int_fib transfer_nat_int_fib_closure]
    4.77 +
    4.78 +lemma transfer_int_nat_fib:
    4.79 +  "fib (int n) = int (fib n)"
    4.80 +  unfolding fib_int_def by auto
    4.81 +
    4.82 +lemma transfer_int_nat_fib_closure:
    4.83 +  "is_nat n \<Longrightarrow> fib n >= 0"
    4.84 +  unfolding fib_int_def by auto
    4.85 +
    4.86 +declare TransferMorphism_int_nat[transfer add return: 
    4.87 +    transfer_int_nat_fib transfer_int_nat_fib_closure]
    4.88 +
    4.89 +
    4.90 +subsection {* Fibonacci numbers *}
    4.91 +
    4.92 +lemma nat_fib_0 [simp]: "fib (0::nat) = 0"
    4.93 +  by simp
    4.94 +
    4.95 +lemma int_fib_0 [simp]: "fib (0::int) = 0"
    4.96 +  unfolding fib_int_def by simp
    4.97 +
    4.98 +lemma nat_fib_1 [simp]: "fib (1::nat) = 1"
    4.99 +  by simp
   4.100 +
   4.101 +lemma nat_fib_Suc_0 [simp]: "fib (Suc 0) = Suc 0"
   4.102 +  by simp
   4.103 +
   4.104 +lemma int_fib_1 [simp]: "fib (1::int) = 1"
   4.105 +  unfolding fib_int_def by simp
   4.106 +
   4.107 +lemma nat_fib_reduce: "(n::nat) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
   4.108 +  by simp
   4.109 +
   4.110 +declare fib_nat.simps [simp del]
   4.111 +
   4.112 +lemma int_fib_reduce: "(n::int) >= 2 \<Longrightarrow> fib n = fib (n - 1) + fib (n - 2)"
   4.113 +  unfolding fib_int_def
   4.114 +  by (auto simp add: nat_fib_reduce nat_diff_distrib)
   4.115 +
   4.116 +lemma int_fib_neg [simp]: "(n::int) < 0 \<Longrightarrow> fib n = 0"
   4.117 +  unfolding fib_int_def by auto
   4.118 +
   4.119 +lemma nat_fib_2 [simp]: "fib (2::nat) = 1"
   4.120 +  by (subst nat_fib_reduce, auto)
   4.121 +
   4.122 +lemma int_fib_2 [simp]: "fib (2::int) = 1"
   4.123 +  by (subst int_fib_reduce, auto)
   4.124 +
   4.125 +lemma nat_fib_plus_2: "fib ((n::nat) + 2) = fib (n + 1) + fib n"
   4.126 +  by (subst nat_fib_reduce, auto simp add: One_nat_def)
   4.127 +(* the need for One_nat_def is due to the natdiff_cancel_numerals
   4.128 +   procedure *)
   4.129 +
   4.130 +lemma nat_fib_induct: "P (0::nat) \<Longrightarrow> P (1::nat) \<Longrightarrow> 
   4.131 +    (!!n. P n \<Longrightarrow> P (n + 1) \<Longrightarrow> P (n + 2)) \<Longrightarrow> P n"
   4.132 +  apply (atomize, induct n rule: nat_less_induct)
   4.133 +  apply auto
   4.134 +  apply (case_tac "n = 0", force)
   4.135 +  apply (case_tac "n = 1", force)
   4.136 +  apply (subgoal_tac "n >= 2")
   4.137 +  apply (frule_tac x = "n - 1" in spec)
   4.138 +  apply (drule_tac x = "n - 2" in spec)
   4.139 +  apply (drule_tac x = "n - 2" in spec)
   4.140 +  apply auto
   4.141 +  apply (auto simp add: One_nat_def) (* again, natdiff_cancel *)
   4.142 +done
   4.143 +
   4.144 +lemma nat_fib_add: "fib ((n::nat) + k + 1) = fib (k + 1) * fib (n + 1) + 
   4.145 +    fib k * fib n"
   4.146 +  apply (induct n rule: nat_fib_induct)
   4.147 +  apply auto
   4.148 +  apply (subst nat_fib_reduce)
   4.149 +  apply (auto simp add: ring_simps)
   4.150 +  apply (subst (1 3 5) nat_fib_reduce)
   4.151 +  apply (auto simp add: ring_simps Suc_remove)
   4.152 +(* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
   4.153 +  apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
   4.154 +  apply (erule ssubst) back back
   4.155 +  apply (erule ssubst) back 
   4.156 +  apply auto
   4.157 +done
   4.158 +
   4.159 +lemma nat_fib_add': "fib (n + Suc k) = fib (Suc k) * fib (Suc n) + 
   4.160 +    fib k * fib n"
   4.161 +  using nat_fib_add by (auto simp add: One_nat_def)
   4.162 +
   4.163 +
   4.164 +(* transfer from nats to ints *)
   4.165 +lemma int_fib_add [rule_format]: "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow>
   4.166 +    fib (n + k + 1) = fib (k + 1) * fib (n + 1) + 
   4.167 +    fib k * fib n "
   4.168 +
   4.169 +  by (rule nat_fib_add [transferred])
   4.170 +
   4.171 +lemma nat_fib_neq_0: "(n::nat) > 0 \<Longrightarrow> fib n ~= 0"
   4.172 +  apply (induct n rule: nat_fib_induct)
   4.173 +  apply (auto simp add: nat_fib_plus_2)
   4.174 +done
   4.175 +
   4.176 +lemma nat_fib_gr_0: "(n::nat) > 0 \<Longrightarrow> fib n > 0"
   4.177 +  by (frule nat_fib_neq_0, simp)
   4.178 +
   4.179 +lemma int_fib_gr_0: "(n::int) > 0 \<Longrightarrow> fib n > 0"
   4.180 +  unfolding fib_int_def by (simp add: nat_fib_gr_0)
   4.181 +
   4.182 +text {*
   4.183 +  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
   4.184 +  much easier using integers, not natural numbers!
   4.185 +*}
   4.186 +
   4.187 +lemma int_fib_Cassini_aux: "fib (int n + 2) * fib (int n) - 
   4.188 +    (fib (int n + 1))^2 = (-1)^(n + 1)"
   4.189 +  apply (induct n)
   4.190 +  apply (auto simp add: ring_simps power2_eq_square int_fib_reduce
   4.191 +      power_add)
   4.192 +done
   4.193 +
   4.194 +lemma int_fib_Cassini: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n - 
   4.195 +    (fib (n + 1))^2 = (-1)^(nat n + 1)"
   4.196 +  by (insert int_fib_Cassini_aux [of "nat n"], auto)
   4.197 +
   4.198 +(*
   4.199 +lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib (n + 2) * fib n = 
   4.200 +    (fib (n + 1))^2 + (-1)^(nat n + 1)"
   4.201 +  by (frule int_fib_Cassini, simp) 
   4.202 +*)
   4.203 +
   4.204 +lemma int_fib_Cassini': "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
   4.205 +  (if even n then tsub ((fib (n + 1))^2) 1
   4.206 +   else (fib (n + 1))^2 + 1)"
   4.207 +  apply (frule int_fib_Cassini, auto simp add: pos_int_even_equiv_nat_even)
   4.208 +  apply (subst tsub_eq)
   4.209 +  apply (insert int_fib_gr_0 [of "n + 1"], force)
   4.210 +  apply auto
   4.211 +done
   4.212 +
   4.213 +lemma nat_fib_Cassini: "fib ((n::nat) + 2) * fib n =
   4.214 +  (if even n then (fib (n + 1))^2 - 1
   4.215 +   else (fib (n + 1))^2 + 1)"
   4.216 +
   4.217 +  by (rule int_fib_Cassini' [transferred, of n], auto)
   4.218 +
   4.219 +
   4.220 +text {* \medskip Toward Law 6.111 of Concrete Mathematics *}
   4.221 +
   4.222 +lemma nat_coprime_fib_plus_1: "coprime (fib (n::nat)) (fib (n + 1))"
   4.223 +  apply (induct n rule: nat_fib_induct)
   4.224 +  apply auto
   4.225 +  apply (subst (2) nat_fib_reduce)
   4.226 +  apply (auto simp add: Suc_remove) (* again, natdiff_cancel *)
   4.227 +  apply (subst add_commute, auto)
   4.228 +  apply (subst nat_gcd_commute, auto simp add: ring_simps)
   4.229 +done
   4.230 +
   4.231 +lemma nat_coprime_fib_Suc: "coprime (fib n) (fib (Suc n))"
   4.232 +  using nat_coprime_fib_plus_1 by (simp add: One_nat_def)
   4.233 +
   4.234 +lemma int_coprime_fib_plus_1: 
   4.235 +    "n >= 0 \<Longrightarrow> coprime (fib (n::int)) (fib (n + 1))"
   4.236 +  by (erule nat_coprime_fib_plus_1 [transferred])
   4.237 +
   4.238 +lemma nat_gcd_fib_add: "gcd (fib (m::nat)) (fib (n + m)) = gcd (fib m) (fib n)"
   4.239 +  apply (simp add: nat_gcd_commute [of "fib m"])
   4.240 +  apply (rule nat_cases [of _ m])
   4.241 +  apply simp
   4.242 +  apply (subst add_assoc [symmetric])
   4.243 +  apply (simp add: nat_fib_add)
   4.244 +  apply (subst nat_gcd_commute)
   4.245 +  apply (subst mult_commute)
   4.246 +  apply (subst nat_gcd_add_mult)
   4.247 +  apply (subst nat_gcd_commute)
   4.248 +  apply (rule nat_gcd_mult_cancel)
   4.249 +  apply (rule nat_coprime_fib_plus_1)
   4.250 +done
   4.251 +
   4.252 +lemma int_gcd_fib_add [rule_format]: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> 
   4.253 +    gcd (fib (m::int)) (fib (n + m)) = gcd (fib m) (fib n)"
   4.254 +  by (erule nat_gcd_fib_add [transferred])
   4.255 +
   4.256 +lemma nat_gcd_fib_diff: "(m::nat) \<le> n \<Longrightarrow> 
   4.257 +    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   4.258 +  by (simp add: nat_gcd_fib_add [symmetric, of _ "n-m"])
   4.259 +
   4.260 +lemma int_gcd_fib_diff: "0 <= (m::int) \<Longrightarrow> m \<le> n \<Longrightarrow> 
   4.261 +    gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   4.262 +  by (simp add: int_gcd_fib_add [symmetric, of _ "n-m"])
   4.263 +
   4.264 +lemma nat_gcd_fib_mod: "0 < (m::nat) \<Longrightarrow> 
   4.265 +    gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   4.266 +proof (induct n rule: less_induct)
   4.267 +  case (less n)
   4.268 +  from less.prems have pos_m: "0 < m" .
   4.269 +  show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   4.270 +  proof (cases "m < n")
   4.271 +    case True note m_n = True
   4.272 +    then have m_n': "m \<le> n" by auto
   4.273 +    with pos_m have pos_n: "0 < n" by auto
   4.274 +    with pos_m m_n have diff: "n - m < n" by auto
   4.275 +    have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
   4.276 +    by (simp add: mod_if [of n]) (insert m_n, auto)
   4.277 +    also have "\<dots> = gcd (fib m)  (fib (n - m))" 
   4.278 +      by (simp add: less.hyps diff pos_m)
   4.279 +    also have "\<dots> = gcd (fib m) (fib n)" by (simp add: nat_gcd_fib_diff m_n')
   4.280 +    finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
   4.281 +  next
   4.282 +    case False then show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   4.283 +    by (cases "m = n") auto
   4.284 +  qed
   4.285 +qed
   4.286 +
   4.287 +lemma int_gcd_fib_mod: 
   4.288 +  assumes "0 < (m::int)" and "0 <= n"
   4.289 +  shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
   4.290 +
   4.291 +  apply (rule nat_gcd_fib_mod [transferred])
   4.292 +  using prems apply auto
   4.293 +done
   4.294 +
   4.295 +lemma nat_fib_gcd: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"  
   4.296 +    -- {* Law 6.111 *}
   4.297 +  apply (induct m n rule: nat_gcd_induct)
   4.298 +  apply (simp_all add: nat_gcd_non_0 nat_gcd_commute nat_gcd_fib_mod)
   4.299 +done
   4.300 +
   4.301 +lemma int_fib_gcd: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   4.302 +    fib (gcd (m::int) n) = gcd (fib m) (fib n)"
   4.303 +  by (erule nat_fib_gcd [transferred])
   4.304 +
   4.305 +lemma nat_atMost_plus_one: "{..(k::nat) + 1} = insert (k + 1) {..k}" 
   4.306 +  by auto
   4.307 +
   4.308 +theorem nat_fib_mult_eq_setsum:
   4.309 +    "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   4.310 +  apply (induct n)
   4.311 +  apply (auto simp add: nat_atMost_plus_one nat_fib_plus_2 ring_simps)
   4.312 +done
   4.313 +
   4.314 +theorem nat_fib_mult_eq_setsum':
   4.315 +    "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   4.316 +  using nat_fib_mult_eq_setsum by (simp add: One_nat_def)
   4.317 +
   4.318 +theorem int_fib_mult_eq_setsum [rule_format]:
   4.319 +    "n >= 0 \<Longrightarrow> fib ((n::int) + 1) * fib n = (\<Sum>k \<in> {0..n}. fib k * fib k)"
   4.320 +  by (erule nat_fib_mult_eq_setsum [transferred])
   4.321 +
   4.322 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/NewNumberTheory/MiscAlgebra.thy	Fri Jun 19 18:33:10 2009 +0200
     5.3 @@ -0,0 +1,402 @@
     5.4 +(*  Title:      MiscAlgebra.thy
     5.5 +    ID:         
     5.6 +    Author:     Jeremy Avigad
     5.7 +
     5.8 +    These are things that can be added to the Algebra library,
     5.9 +    as well as a few things that could possibly go in Main. 
    5.10 +*)
    5.11 +
    5.12 +theory MiscAlgebra
    5.13 +imports 
    5.14 +  "~~/src/HOL/Algebra/Ring"
    5.15 +  "~~/src/HOL/Algebra/FiniteProduct"
    5.16 +begin;
    5.17 +
    5.18 +declare One_nat_def [simp del] 
    5.19 +
    5.20 +
    5.21 +(* Some things for Main? *)
    5.22 +
    5.23 +(* finiteness stuff *)
    5.24 +
    5.25 +lemma int_bounded_set1 [intro]: "finite {(x::int). a < x & x < b & P x}" 
    5.26 +  apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}")
    5.27 +  apply (erule finite_subset)
    5.28 +  apply auto
    5.29 +done
    5.30 +
    5.31 +lemma image_set_eq_image: "{ f x | x. P x} = f ` { x. P x}"
    5.32 +  unfolding image_def apply auto
    5.33 +done
    5.34 +
    5.35 +lemma finite_image_set [simp]: "finite {x. P x} \<Longrightarrow> 
    5.36 +    finite { f x | x. P x}"
    5.37 +  apply (subst image_set_eq_image)
    5.38 +  apply auto
    5.39 +done
    5.40 +
    5.41 +(* Examples:
    5.42 +
    5.43 +lemma "finite {x. 0 < x & x < 100 & prime (x::int)}"
    5.44 +  by auto
    5.45 +
    5.46 +lemma "finite { 3 * x | x. 0 < x & x < 100 & prime (x::int) }"
    5.47 +  by auto
    5.48 +
    5.49 +*)
    5.50 +
    5.51 +(* This could go in Set.thy *)
    5.52 +
    5.53 +lemma UNION_empty: "(UNION F A = {}) = (ALL x: F. (A x) = {})"
    5.54 +  by auto
    5.55 +
    5.56 +
    5.57 +(* The rest is for the algebra libraries *)
    5.58 +
    5.59 +(* This goes in FuncSet.thy. Any reason not to make it a simp rule? *)
    5.60 +
    5.61 +lemma funcset_id [simp]: "(%x. x): A \<rightarrow> A"
    5.62 +  by (auto simp add: Pi_def);
    5.63 +
    5.64 +(* These go in Group.thy. *)
    5.65 +
    5.66 +(*
    5.67 +  Show that the units in any monoid give rise to a group.
    5.68 +
    5.69 +  The file Residues.thy provides some infrastructure to use
    5.70 +  facts about the unit group within the ring locale.
    5.71 +*)
    5.72 +
    5.73 +
    5.74 +constdefs 
    5.75 +  units_of :: "('a, 'b) monoid_scheme => 'a monoid"
    5.76 +  "units_of G == (| carrier = Units G,
    5.77 +     Group.monoid.mult = Group.monoid.mult G,
    5.78 +     one  = one G |)";
    5.79 +
    5.80 +(*
    5.81 +
    5.82 +lemma (in monoid) Units_mult_closed [intro]:
    5.83 +  "x : Units G ==> y : Units G ==> x \<otimes> y : Units G"
    5.84 +  apply (unfold Units_def)
    5.85 +  apply (clarsimp)
    5.86 +  apply (rule_tac x = "xaa \<otimes> xa" in bexI)
    5.87 +  apply auto
    5.88 +  apply (subst m_assoc)
    5.89 +  apply auto
    5.90 +  apply (subst (2) m_assoc [symmetric])
    5.91 +  apply auto
    5.92 +  apply (subst m_assoc)
    5.93 +  apply auto
    5.94 +  apply (subst (2) m_assoc [symmetric])
    5.95 +  apply auto
    5.96 +done
    5.97 +
    5.98 +*)
    5.99 +
   5.100 +lemma (in monoid) units_group: "group(units_of G)"
   5.101 +  apply (unfold units_of_def)
   5.102 +  apply (rule groupI)
   5.103 +  apply auto
   5.104 +  apply (subst m_assoc)
   5.105 +  apply auto
   5.106 +  apply (rule_tac x = "inv x" in bexI)
   5.107 +  apply auto
   5.108 +done
   5.109 +
   5.110 +lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
   5.111 +  apply (rule group.group_comm_groupI)
   5.112 +  apply (rule units_group)
   5.113 +  apply (insert prems)
   5.114 +  apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
   5.115 +  apply auto;
   5.116 +done;
   5.117 +
   5.118 +lemma units_of_carrier: "carrier (units_of G) = Units G"
   5.119 +  by (unfold units_of_def, auto)
   5.120 +
   5.121 +lemma units_of_mult: "mult(units_of G) = mult G"
   5.122 +  by (unfold units_of_def, auto)
   5.123 +
   5.124 +lemma units_of_one: "one(units_of G) = one G"
   5.125 +  by (unfold units_of_def, auto)
   5.126 +
   5.127 +lemma (in monoid) units_of_inv: "x : Units G ==> 
   5.128 +    m_inv (units_of G) x = m_inv G x"
   5.129 +  apply (rule sym)
   5.130 +  apply (subst m_inv_def)
   5.131 +  apply (rule the1_equality)
   5.132 +  apply (rule ex_ex1I)
   5.133 +  apply (subst (asm) Units_def)
   5.134 +  apply auto
   5.135 +  apply (erule inv_unique)
   5.136 +  apply auto
   5.137 +  apply (rule Units_closed)
   5.138 +  apply (simp_all only: units_of_carrier [symmetric])
   5.139 +  apply (insert units_group)
   5.140 +  apply auto
   5.141 +  apply (subst units_of_mult [symmetric])
   5.142 +  apply (subst units_of_one [symmetric])
   5.143 +  apply (erule group.r_inv, assumption)
   5.144 +  apply (subst units_of_mult [symmetric])
   5.145 +  apply (subst units_of_one [symmetric])
   5.146 +  apply (erule group.l_inv, assumption)
   5.147 +done
   5.148 +
   5.149 +lemma (in group) inj_on_const_mult: "a: (carrier G) ==> 
   5.150 +    inj_on (%x. a \<otimes> x) (carrier G)"
   5.151 +  by (unfold inj_on_def, auto)
   5.152 +
   5.153 +lemma (in group) surj_const_mult: "a : (carrier G) ==>
   5.154 +    (%x. a \<otimes> x) ` (carrier G) = (carrier G)" 
   5.155 +  apply (auto simp add: image_def)
   5.156 +  apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI)
   5.157 +  apply auto
   5.158 +(* auto should get this. I suppose we need "comm_monoid_simprules"
   5.159 +   for mult_ac rewriting. *)
   5.160 +  apply (subst m_assoc [symmetric])
   5.161 +  apply auto
   5.162 +done
   5.163 +
   5.164 +lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   5.165 +    (x \<otimes> a = x) = (a = one G)"
   5.166 +  apply auto
   5.167 +  apply (subst l_cancel [symmetric])
   5.168 +  prefer 4
   5.169 +  apply (erule ssubst)
   5.170 +  apply auto
   5.171 +done
   5.172 +
   5.173 +lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   5.174 +    (a \<otimes> x = x) = (a = one G)"
   5.175 +  apply auto
   5.176 +  apply (subst r_cancel [symmetric])
   5.177 +  prefer 4
   5.178 +  apply (erule ssubst)
   5.179 +  apply auto
   5.180 +done
   5.181 +
   5.182 +(* Is there a better way to do this? *)
   5.183 +
   5.184 +lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   5.185 +    (x = x \<otimes> a) = (a = one G)"
   5.186 +  by (subst eq_commute, simp)
   5.187 +
   5.188 +lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow>
   5.189 +    (x = a \<otimes> x) = (a = one G)"
   5.190 +  by (subst eq_commute, simp)
   5.191 +
   5.192 +(* This should be generalized to arbitrary groups, not just commutative
   5.193 +   ones, using Lagrange's theorem. *)
   5.194 +
   5.195 +lemma (in comm_group) power_order_eq_one:
   5.196 +    assumes fin [simp]: "finite (carrier G)"
   5.197 +        and a [simp]: "a : carrier G" 
   5.198 +      shows "a (^) card(carrier G) = one G" 
   5.199 +proof -
   5.200 +  have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
   5.201 +    by (subst (2) finprod_reindex [symmetric], 
   5.202 +      auto simp add: Pi_def inj_on_const_mult surj_const_mult)
   5.203 +  also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
   5.204 +    by (auto simp add: finprod_multf Pi_def)
   5.205 +  also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
   5.206 +    by (auto simp add: finprod_const)
   5.207 +  finally show ?thesis
   5.208 +(* uses the preceeding lemma *)
   5.209 +    by auto
   5.210 +qed
   5.211 +
   5.212 +
   5.213 +(* Miscellaneous *)
   5.214 +
   5.215 +lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
   5.216 +    x : Units R \<Longrightarrow> field R"
   5.217 +  apply (unfold_locales)
   5.218 +  apply (insert prems, auto)
   5.219 +  apply (rule trans)
   5.220 +  apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
   5.221 +  apply assumption
   5.222 +  apply (subst m_assoc) 
   5.223 +  apply (auto simp add: Units_r_inv)
   5.224 +  apply (unfold Units_def)
   5.225 +  apply auto
   5.226 +done
   5.227 +
   5.228 +lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   5.229 +  x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
   5.230 +  apply (subgoal_tac "x : Units G")
   5.231 +  apply (subgoal_tac "y = inv x \<otimes> \<one>")
   5.232 +  apply simp
   5.233 +  apply (erule subst)
   5.234 +  apply (subst m_assoc [symmetric])
   5.235 +  apply auto
   5.236 +  apply (unfold Units_def)
   5.237 +  apply auto
   5.238 +done
   5.239 +
   5.240 +lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
   5.241 +  x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
   5.242 +  apply (rule inv_char)
   5.243 +  apply auto
   5.244 +  apply (subst m_comm, auto) 
   5.245 +done
   5.246 +
   5.247 +lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"  
   5.248 +  apply (rule inv_char)
   5.249 +  apply (auto simp add: l_minus r_minus)
   5.250 +done
   5.251 +
   5.252 +lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow> 
   5.253 +    inv x = inv y \<Longrightarrow> x = y"
   5.254 +  apply (subgoal_tac "inv(inv x) = inv(inv y)")
   5.255 +  apply (subst (asm) Units_inv_inv)+
   5.256 +  apply auto
   5.257 +done
   5.258 +
   5.259 +lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R"
   5.260 +  apply (unfold Units_def)
   5.261 +  apply auto
   5.262 +  apply (rule_tac x = "\<ominus> \<one>" in bexI)
   5.263 +  apply auto
   5.264 +  apply (simp add: l_minus r_minus)
   5.265 +done
   5.266 +
   5.267 +lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>"
   5.268 +  apply (rule inv_char)
   5.269 +  apply auto
   5.270 +done
   5.271 +
   5.272 +lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)"
   5.273 +  apply auto
   5.274 +  apply (subst Units_inv_inv [symmetric])
   5.275 +  apply auto
   5.276 +done
   5.277 +
   5.278 +lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)"
   5.279 +  apply auto
   5.280 +  apply (subst Units_inv_inv [symmetric])
   5.281 +  apply auto
   5.282 +done
   5.283 +
   5.284 +
   5.285 +(* This goes in FiniteProduct *)
   5.286 +
   5.287 +lemma (in comm_monoid) finprod_UN_disjoint:
   5.288 +  "finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow>
   5.289 +     (A i) Int (A j) = {}) \<longrightarrow>
   5.290 +      (ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow>
   5.291 +        finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I"
   5.292 +  apply (induct set: finite)
   5.293 +  apply force
   5.294 +  apply clarsimp
   5.295 +  apply (subst finprod_Un_disjoint)
   5.296 +  apply blast
   5.297 +  apply (erule finite_UN_I)
   5.298 +  apply blast
   5.299 +  apply (subst Int_UN_distrib)
   5.300 +  apply (subst UNION_empty)
   5.301 +  apply clarsimp
   5.302 +  apply (drule_tac x = xa in bspec)back
   5.303 +  apply (assumption, force)
   5.304 +  apply (auto intro!: funcsetI finprod_closed) 
   5.305 +  apply (subst finprod_insert)
   5.306 +  apply (auto intro!: funcsetI finprod_closed)
   5.307 +done
   5.308 +
   5.309 +lemma (in comm_monoid) finprod_Union_disjoint:
   5.310 +  "[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
   5.311 +      (ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] 
   5.312 +   ==> finprod G f (Union C) = finprod G (finprod G f) C" 
   5.313 +  apply (frule finprod_UN_disjoint [of C id f])
   5.314 +  apply (unfold Union_def id_def, auto)
   5.315 +done
   5.316 +
   5.317 +lemma (in comm_monoid) finprod_one [rule_format]: 
   5.318 +  "finite A \<Longrightarrow> (ALL x:A. f x = \<one>) \<longrightarrow>
   5.319 +     finprod G f A = \<one>"
   5.320 +  apply (induct set: finite)
   5.321 +  apply auto
   5.322 +  apply (subst finprod_insert)
   5.323 +  apply (auto intro!: funcsetI)
   5.324 +done
   5.325 +
   5.326 +
   5.327 +(* need better simplification rules for rings *)
   5.328 +(* the next one holds more generally for abelian groups *)
   5.329 +
   5.330 +lemma (in cring) sum_zero_eq_neg:
   5.331 +  "x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y"
   5.332 +  apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y") 
   5.333 +  apply (erule ssubst)back
   5.334 +  apply (erule subst)
   5.335 +  apply (simp add: ring_simprules)+
   5.336 +done
   5.337 +
   5.338 +(* there's a name conflict -- maybe "domain" should be
   5.339 +   "integral_domain" *)
   5.340 +
   5.341 +lemma (in Ring.domain) square_eq_one: 
   5.342 +  fixes x
   5.343 +  assumes [simp]: "x : carrier R" and
   5.344 +    "x \<otimes> x = \<one>"
   5.345 +  shows "x = \<one> | x = \<ominus>\<one>"
   5.346 +proof -
   5.347 +  have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
   5.348 +    by (simp add: ring_simprules)
   5.349 +  also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
   5.350 +    by (simp add: ring_simprules)
   5.351 +  finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
   5.352 +  hence "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
   5.353 +    by (intro integral, auto)
   5.354 +  thus ?thesis
   5.355 +    apply auto
   5.356 +    apply (erule notE)
   5.357 +    apply (rule sum_zero_eq_neg)
   5.358 +    apply auto
   5.359 +    apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)")
   5.360 +    apply (simp add: ring_simprules) 
   5.361 +    apply (rule sum_zero_eq_neg)
   5.362 +    apply auto
   5.363 +    done
   5.364 +qed
   5.365 +
   5.366 +lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow>
   5.367 +    x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>"
   5.368 +  apply (rule square_eq_one)
   5.369 +  apply auto
   5.370 +  apply (erule ssubst)back
   5.371 +  apply (erule Units_r_inv)
   5.372 +done
   5.373 +
   5.374 +
   5.375 +(*
   5.376 +  The following translates theorems about groups to the facts about
   5.377 +  the units of a ring. (The list should be expanded as more things are
   5.378 +  needed.)
   5.379 +*)
   5.380 +
   5.381 +lemma (in ring) finite_ring_finite_units [intro]: "finite (carrier R) \<Longrightarrow> 
   5.382 +    finite (Units R)"
   5.383 +  by (rule finite_subset, auto)
   5.384 +
   5.385 +(* this belongs with MiscAlgebra.thy *)
   5.386 +lemma (in monoid) units_of_pow: 
   5.387 +    "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
   5.388 +  apply (induct n)
   5.389 +  apply (auto simp add: units_group group.is_monoid  
   5.390 +    monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult
   5.391 +    One_nat_def)
   5.392 +done
   5.393 +
   5.394 +lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
   5.395 +    \<Longrightarrow> a (^) card(Units R) = \<one>"
   5.396 +  apply (subst units_of_carrier [symmetric])
   5.397 +  apply (subst units_of_one [symmetric])
   5.398 +  apply (subst units_of_pow [symmetric])
   5.399 +  apply assumption
   5.400 +  apply (rule comm_group.power_order_eq_one)
   5.401 +  apply (rule units_comm_group)
   5.402 +  apply (unfold units_of_def, auto)
   5.403 +done
   5.404 +
   5.405 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/NewNumberTheory/ROOT.ML	Fri Jun 19 18:33:10 2009 +0200
     6.3 @@ -0,0 +1,1 @@
     6.4 +use_thys ["Fib","Residues"];
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/NewNumberTheory/Residues.thy	Fri Jun 19 18:33:10 2009 +0200
     7.3 @@ -0,0 +1,474 @@
     7.4 +(*  Title:      HOL/Library/Residues.thy
     7.5 +    ID:         
     7.6 +    Author:     Jeremy Avigad
     7.7 +
     7.8 +    An algebraic treatment of residue rings, and resulting proofs of
     7.9 +    Euler's theorem and Wilson's theorem. 
    7.10 +*)
    7.11 +
    7.12 +header {* Residue rings *}
    7.13 +
    7.14 +theory Residues
    7.15 +imports
    7.16 +   UniqueFactorization
    7.17 +   Binomial
    7.18 +   MiscAlgebra
    7.19 +begin
    7.20 +
    7.21 +
    7.22 +(*
    7.23 + 
    7.24 +  A locale for residue rings
    7.25 +
    7.26 +*)
    7.27 +
    7.28 +constdefs 
    7.29 +  residue_ring :: "int => int ring"
    7.30 +  "residue_ring m == (| 
    7.31 +    carrier =       {0..m - 1}, 
    7.32 +    mult =          (%x y. (x * y) mod m),
    7.33 +    one =           1,
    7.34 +    zero =          0,
    7.35 +    add =           (%x y. (x + y) mod m) |)"
    7.36 +
    7.37 +locale residues =
    7.38 +  fixes m :: int and R (structure)
    7.39 +  assumes m_gt_one: "m > 1"
    7.40 +  defines "R == residue_ring m"
    7.41 +
    7.42 +context residues begin
    7.43 +
    7.44 +lemma abelian_group: "abelian_group R"
    7.45 +  apply (insert m_gt_one)
    7.46 +  apply (rule abelian_groupI)
    7.47 +  apply (unfold R_def residue_ring_def)
    7.48 +  apply (auto simp add: mod_pos_pos_trivial mod_add_right_eq [symmetric]
    7.49 +    add_ac)
    7.50 +  apply (case_tac "x = 0")
    7.51 +  apply force
    7.52 +  apply (subgoal_tac "(x + (m - x)) mod m = 0")
    7.53 +  apply (erule bexI)
    7.54 +  apply auto
    7.55 +done
    7.56 +
    7.57 +lemma comm_monoid: "comm_monoid R"
    7.58 +  apply (insert m_gt_one)
    7.59 +  apply (unfold R_def residue_ring_def)
    7.60 +  apply (rule comm_monoidI)
    7.61 +  apply auto
    7.62 +  apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
    7.63 +  apply (erule ssubst)
    7.64 +  apply (subst zmod_zmult1_eq [symmetric])+
    7.65 +  apply (simp_all only: mult_ac)
    7.66 +done
    7.67 +
    7.68 +lemma cring: "cring R"
    7.69 +  apply (rule cringI)
    7.70 +  apply (rule abelian_group)
    7.71 +  apply (rule comm_monoid)
    7.72 +  apply (unfold R_def residue_ring_def, auto)
    7.73 +  apply (subst mod_add_eq [symmetric])
    7.74 +  apply (subst mult_commute)
    7.75 +  apply (subst zmod_zmult1_eq [symmetric])
    7.76 +  apply (simp add: ring_simps)
    7.77 +done
    7.78 +
    7.79 +end
    7.80 +
    7.81 +sublocale residues < cring
    7.82 +  by (rule cring)
    7.83 +
    7.84 +
    7.85 +context residues begin
    7.86 +
    7.87 +(* These lemmas translate back and forth between internal and 
    7.88 +   external concepts *)
    7.89 +
    7.90 +lemma res_carrier_eq: "carrier R = {0..m - 1}"
    7.91 +  by (unfold R_def residue_ring_def, auto)
    7.92 +
    7.93 +lemma res_add_eq: "x \<oplus> y = (x + y) mod m"
    7.94 +  by (unfold R_def residue_ring_def, auto)
    7.95 +
    7.96 +lemma res_mult_eq: "x \<otimes> y = (x * y) mod m"
    7.97 +  by (unfold R_def residue_ring_def, auto)
    7.98 +
    7.99 +lemma res_zero_eq: "\<zero> = 0"
   7.100 +  by (unfold R_def residue_ring_def, auto)
   7.101 +
   7.102 +lemma res_one_eq: "\<one> = 1"
   7.103 +  by (unfold R_def residue_ring_def units_of_def residue_ring_def, auto)
   7.104 +
   7.105 +lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
   7.106 +  apply (insert m_gt_one)
   7.107 +  apply (unfold Units_def R_def residue_ring_def)
   7.108 +  apply auto
   7.109 +  apply (subgoal_tac "x ~= 0")
   7.110 +  apply auto
   7.111 +  apply (rule int_invertible_coprime)
   7.112 +  apply (subgoal_tac "x ~= 0")
   7.113 +  apply auto
   7.114 +  apply (subst (asm) int_coprime_iff_invertible')
   7.115 +  apply (rule m_gt_one)
   7.116 +  apply (auto simp add: cong_int_def mult_commute)
   7.117 +done
   7.118 +
   7.119 +lemma res_neg_eq: "\<ominus> x = (- x) mod m"
   7.120 +  apply (insert m_gt_one)
   7.121 +  apply (unfold R_def a_inv_def m_inv_def residue_ring_def)
   7.122 +  apply auto
   7.123 +  apply (rule the_equality)
   7.124 +  apply auto
   7.125 +  apply (subst mod_add_right_eq [symmetric])
   7.126 +  apply auto
   7.127 +  apply (subst mod_add_left_eq [symmetric])
   7.128 +  apply auto
   7.129 +  apply (subgoal_tac "y mod m = - x mod m")
   7.130 +  apply simp
   7.131 +  apply (subst zmod_eq_dvd_iff)
   7.132 +  apply auto
   7.133 +done
   7.134 +
   7.135 +lemma finite [iff]: "finite(carrier R)"
   7.136 +  by (subst res_carrier_eq, auto)
   7.137 +
   7.138 +lemma finite_Units [iff]: "finite(Units R)"
   7.139 +  by (subst res_units_eq, auto)
   7.140 +
   7.141 +(* The function a -> a mod m maps the integers to the 
   7.142 +   residue classes. The following lemmas show that this mapping 
   7.143 +   respects addition and multiplication on the integers. *)
   7.144 +
   7.145 +lemma mod_in_carrier [iff]: "a mod m : carrier R"
   7.146 +  apply (unfold res_carrier_eq)
   7.147 +  apply (insert m_gt_one, auto)
   7.148 +done
   7.149 +
   7.150 +lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
   7.151 +  by (unfold R_def residue_ring_def, auto, arith)
   7.152 +
   7.153 +lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m"
   7.154 +  apply (unfold R_def residue_ring_def, auto)
   7.155 +  apply (subst zmod_zmult1_eq [symmetric])
   7.156 +  apply (subst mult_commute)
   7.157 +  apply (subst zmod_zmult1_eq [symmetric])
   7.158 +  apply (subst mult_commute)
   7.159 +  apply auto
   7.160 +done  
   7.161 +
   7.162 +lemma zero_cong: "\<zero> = 0"
   7.163 +  apply (unfold R_def residue_ring_def, auto)
   7.164 +done
   7.165 +
   7.166 +lemma one_cong: "\<one> = 1 mod m"
   7.167 +  apply (insert m_gt_one)
   7.168 +  apply (unfold R_def residue_ring_def, auto)
   7.169 +done
   7.170 +
   7.171 +(* revise algebra library to use 1? *)
   7.172 +lemma pow_cong: "(x mod m) (^) n = x^n mod m"
   7.173 +  apply (insert m_gt_one)
   7.174 +  apply (induct n)
   7.175 +  apply (auto simp add: nat_pow_def one_cong One_nat_def)
   7.176 +  apply (subst mult_commute)
   7.177 +  apply (rule mult_cong)
   7.178 +done
   7.179 +
   7.180 +lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
   7.181 +  apply (rule sym)
   7.182 +  apply (rule sum_zero_eq_neg)
   7.183 +  apply auto
   7.184 +  apply (subst add_cong)
   7.185 +  apply (subst zero_cong)
   7.186 +  apply auto
   7.187 +done
   7.188 +
   7.189 +lemma (in residues) prod_cong: 
   7.190 +  "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
   7.191 +  apply (induct set: finite)
   7.192 +  apply (auto simp add: one_cong) 
   7.193 +  apply (subst finprod_insert)
   7.194 +  apply (auto intro!: funcsetI mult_cong)
   7.195 +done
   7.196 +
   7.197 +lemma (in residues) sum_cong:
   7.198 +  "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
   7.199 +  apply (induct set: finite)
   7.200 +  apply (auto simp add: zero_cong) 
   7.201 +  apply (subst finsum_insert)
   7.202 +  apply (auto intro!: funcsetI add_cong)
   7.203 +done
   7.204 +
   7.205 +lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> 
   7.206 +    a mod m : Units R"
   7.207 +  apply (subst res_units_eq, auto)
   7.208 +  apply (insert pos_mod_sign [of m a])
   7.209 +  apply (subgoal_tac "a mod m ~= 0")
   7.210 +  apply arith
   7.211 +  apply auto
   7.212 +  apply (subst (asm) int_gcd_commute)
   7.213 +  apply (subst (asm) int_gcd_mult)
   7.214 +  apply auto
   7.215 +  apply (subst (asm) int_gcd_red)
   7.216 +  apply (subst int_gcd_commute, assumption)
   7.217 +done
   7.218 +
   7.219 +lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" 
   7.220 +  unfolding cong_int_def by auto
   7.221 +
   7.222 +(* Simplifying with these will translate a ring equation in R to a 
   7.223 +   congruence. *)
   7.224 +
   7.225 +lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong
   7.226 +    prod_cong sum_cong neg_cong res_eq_to_cong
   7.227 +
   7.228 +(* Other useful facts about the residue ring *)
   7.229 +
   7.230 +lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2"
   7.231 +  apply (simp add: res_one_eq res_neg_eq)
   7.232 +  apply (insert m_gt_one)
   7.233 +  apply (subgoal_tac "~(m > 2)")
   7.234 +  apply arith
   7.235 +  apply (rule notI)
   7.236 +  apply (subgoal_tac "-1 mod m = m - 1")
   7.237 +  apply force
   7.238 +  apply (subst mod_add_self2 [symmetric])
   7.239 +  apply (subst mod_pos_pos_trivial)
   7.240 +  apply auto
   7.241 +done
   7.242 +
   7.243 +end
   7.244 +
   7.245 +
   7.246 +(* prime residues *)
   7.247 +
   7.248 +locale residues_prime =
   7.249 +  fixes p :: int and R (structure)
   7.250 +  assumes p_prime [intro]: "prime p"
   7.251 +  defines "R == residue_ring p"
   7.252 +
   7.253 +sublocale residues_prime < residues p
   7.254 +  apply (unfold R_def residues_def)
   7.255 +  using p_prime apply auto
   7.256 +done
   7.257 +
   7.258 +context residues_prime begin
   7.259 +
   7.260 +lemma is_field: "field R"
   7.261 +  apply (rule cring.field_intro2)
   7.262 +  apply (rule cring)
   7.263 +  apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq
   7.264 +    res_units_eq)
   7.265 +  apply (rule classical)
   7.266 +  apply (erule notE)
   7.267 +  apply (subst int_gcd_commute)
   7.268 +  apply (rule int_prime_imp_coprime)
   7.269 +  apply (rule p_prime)
   7.270 +  apply (rule notI)
   7.271 +  apply (frule zdvd_imp_le)
   7.272 +  apply auto
   7.273 +done
   7.274 +
   7.275 +lemma res_prime_units_eq: "Units R = {1..p - 1}"
   7.276 +  apply (subst res_units_eq)
   7.277 +  apply auto
   7.278 +  apply (subst int_gcd_commute)
   7.279 +  apply (rule int_prime_imp_coprime)
   7.280 +  apply (rule p_prime)
   7.281 +  apply (rule zdvd_not_zless)
   7.282 +  apply auto
   7.283 +done
   7.284 +
   7.285 +end
   7.286 +
   7.287 +sublocale residues_prime < field
   7.288 +  by (rule is_field)
   7.289 +
   7.290 +
   7.291 +(*
   7.292 +  Test cases: Euler's theorem and Wilson's theorem.
   7.293 +*)
   7.294 +
   7.295 +
   7.296 +subsection{* Euler's theorem *}
   7.297 +
   7.298 +(* the definition of the phi function *)
   7.299 +
   7.300 +constdefs
   7.301 +  phi :: "int => nat"
   7.302 +  "phi m == card({ x. 0 < x & x < m & gcd x m = 1})" 
   7.303 +
   7.304 +lemma phi_zero [simp]: "phi 0 = 0"
   7.305 +  apply (subst phi_def)
   7.306 +(* Auto hangs here. Once again, where is the simplification rule 
   7.307 +   1 == Suc 0 coming from? *)
   7.308 +  apply (auto simp add: card_eq_0_iff)
   7.309 +(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
   7.310 +done
   7.311 +
   7.312 +lemma phi_one [simp]: "phi 1 = 0"
   7.313 +  apply (auto simp add: phi_def card_eq_0_iff)
   7.314 +done
   7.315 +
   7.316 +lemma (in residues) phi_eq: "phi m = card(Units R)"
   7.317 +  by (simp add: phi_def res_units_eq)
   7.318 +
   7.319 +lemma (in residues) euler_theorem1: 
   7.320 +  assumes a: "gcd a m = 1"
   7.321 +  shows "[a^phi m = 1] (mod m)"
   7.322 +proof -
   7.323 +  from a m_gt_one have [simp]: "a mod m : Units R"
   7.324 +    by (intro mod_in_res_units)
   7.325 +  from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
   7.326 +    by simp
   7.327 +  also have "\<dots> = \<one>" 
   7.328 +    by (intro units_power_order_eq_one, auto)
   7.329 +  finally show ?thesis
   7.330 +    by (simp add: res_to_cong_simps)
   7.331 +qed
   7.332 +
   7.333 +(* In fact, there is a two line proof!
   7.334 +
   7.335 +lemma (in residues) euler_theorem1: 
   7.336 +  assumes a: "gcd a m = 1"
   7.337 +  shows "[a^phi m = 1] (mod m)"
   7.338 +proof -
   7.339 +  have "(a mod m) (^) (phi m) = \<one>"
   7.340 +    by (simp add: phi_eq units_power_order_eq_one a m_gt_one)
   7.341 +  thus ?thesis
   7.342 +    by (simp add: res_to_cong_simps)
   7.343 +qed
   7.344 +
   7.345 +*)
   7.346 +
   7.347 +(* outside the locale, we can relax the restriction m > 1 *)
   7.348 +
   7.349 +lemma euler_theorem:
   7.350 +  assumes "m >= 0" and "gcd a m = 1"
   7.351 +  shows "[a^phi m = 1] (mod m)"
   7.352 +proof (cases)
   7.353 +  assume "m = 0 | m = 1"
   7.354 +  thus ?thesis by auto
   7.355 +next
   7.356 +  assume "~(m = 0 | m = 1)"
   7.357 +  with prems show ?thesis
   7.358 +    by (intro residues.euler_theorem1, unfold residues_def, auto)
   7.359 +qed
   7.360 +
   7.361 +lemma (in residues_prime) phi_prime: "phi p = (nat p - 1)"
   7.362 +  apply (subst phi_eq)
   7.363 +  apply (subst res_prime_units_eq)
   7.364 +  apply auto
   7.365 +done
   7.366 +
   7.367 +lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
   7.368 +  apply (rule residues_prime.phi_prime)
   7.369 +  apply (erule residues_prime.intro)
   7.370 +done
   7.371 +
   7.372 +lemma fermat_theorem:
   7.373 +  assumes "prime p" and "~ (p dvd a)"
   7.374 +  shows "[a^(nat p - 1) = 1] (mod p)"
   7.375 +proof -
   7.376 +  from prems have "[a^phi p = 1] (mod p)"
   7.377 +    apply (intro euler_theorem)
   7.378 +    (* auto should get this next part. matching across
   7.379 +       substitutions is needed. *)
   7.380 +    apply (frule int_prime_gt_1, arith)
   7.381 +    apply (subst int_gcd_commute, erule int_prime_imp_coprime, assumption)
   7.382 +    done
   7.383 +  also have "phi p = nat p - 1"
   7.384 +    by (rule phi_prime, rule prems)
   7.385 +  finally show ?thesis .
   7.386 +qed
   7.387 +
   7.388 +
   7.389 +subsection {* Wilson's theorem *}
   7.390 +
   7.391 +lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow> 
   7.392 +  {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}" 
   7.393 +  apply auto
   7.394 +  apply (erule notE)
   7.395 +  apply (erule inv_eq_imp_eq)
   7.396 +  apply auto
   7.397 +  apply (erule notE)
   7.398 +  apply (erule inv_eq_imp_eq)
   7.399 +  apply auto
   7.400 +done
   7.401 +
   7.402 +lemma (in residues_prime) wilson_theorem1:
   7.403 +  assumes a: "p > 2"
   7.404 +  shows "[fact (p - 1) = - 1] (mod p)"
   7.405 +proof -
   7.406 +  let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}" 
   7.407 +  have "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
   7.408 +    by auto
   7.409 +  hence "(\<Otimes>i: Units R. i) = 
   7.410 +    (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
   7.411 +    apply (elim ssubst) back back
   7.412 +    apply (subst finprod_Un_disjoint)
   7.413 +    apply (auto intro!: funcsetI)
   7.414 +    apply (drule sym, subst (asm) inv_eq_one_eq)
   7.415 +    apply auto
   7.416 +    apply (drule sym, subst (asm) inv_eq_neg_one_eq)
   7.417 +    apply auto
   7.418 +    done
   7.419 +  also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>"
   7.420 +    apply (subst finprod_insert)
   7.421 +    apply auto
   7.422 +    apply (frule one_eq_neg_one)
   7.423 +    apply (insert a, force)
   7.424 +    apply (auto intro!: funcsetI)
   7.425 +    done
   7.426 +  also have "(\<Otimes>i:(Union ?InversePairs). i) = 
   7.427 +      (\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))"
   7.428 +    apply (subst finprod_Union_disjoint)
   7.429 +    apply force
   7.430 +    apply force
   7.431 +    apply clarify
   7.432 +    apply (rule inv_pair_lemma)
   7.433 +    apply auto
   7.434 +    done
   7.435 +  also have "\<dots> = \<one>"
   7.436 +    apply (rule finprod_one)
   7.437 +    apply auto
   7.438 +    apply (subst finprod_insert)
   7.439 +    apply auto
   7.440 +    apply (frule inv_eq_self)
   7.441 +    apply (auto intro!: funcsetI)
   7.442 +    done
   7.443 +  finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"
   7.444 +    by simp
   7.445 +  also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)"
   7.446 +    apply (rule finprod_cong')
   7.447 +    apply (auto intro!: funcsetI)
   7.448 +    apply (subst (asm) res_prime_units_eq)
   7.449 +    apply auto
   7.450 +    done
   7.451 +  also have "\<dots> = (PROD i: Units R. i) mod p"
   7.452 +    apply (rule prod_cong)
   7.453 +    apply auto
   7.454 +    done
   7.455 +  also have "\<dots> = fact (p - 1) mod p"
   7.456 +    apply (subst int_fact_altdef)
   7.457 +    apply (insert prems, force)
   7.458 +    apply (subst res_prime_units_eq, rule refl)
   7.459 +    done
   7.460 +  finally have "fact (p - 1) mod p = \<ominus> \<one>".
   7.461 +  thus ?thesis
   7.462 +    by (simp add: res_to_cong_simps)
   7.463 +qed
   7.464 +
   7.465 +lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)"
   7.466 +  apply (frule int_prime_gt_1)
   7.467 +  apply (case_tac "p = 2")
   7.468 +  apply (subst int_fact_altdef, simp)
   7.469 +  apply (subst cong_int_def)
   7.470 +  apply simp
   7.471 +  apply (rule residues_prime.wilson_theorem1)
   7.472 +  apply (rule residues_prime.intro)
   7.473 +  apply auto
   7.474 +done
   7.475 +
   7.476 +
   7.477 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/NewNumberTheory/UniqueFactorization.thy	Fri Jun 19 18:33:10 2009 +0200
     8.3 @@ -0,0 +1,967 @@
     8.4 +(*  Title:      UniqueFactorization.thy
     8.5 +    ID:         
     8.6 +    Author:     Jeremy Avigad
     8.7 +
     8.8 +    
     8.9 +    Unique factorization for the natural numbers and the integers.
    8.10 +
    8.11 +    Note: there were previous Isabelle formalizations of unique
    8.12 +    factorization due to Thomas Marthedal Rasmussen, and, building on
    8.13 +    that, by Jeremy Avigad and David Gray.  
    8.14 +*)
    8.15 +
    8.16 +header {* UniqueFactorization *}
    8.17 +
    8.18 +theory UniqueFactorization
    8.19 +imports Cong Multiset
    8.20 +begin
    8.21 +
    8.22 +(* inherited from Multiset *)
    8.23 +declare One_nat_def [simp del] 
    8.24 +
    8.25 +(* As a simp or intro rule,
    8.26 +
    8.27 +     prime p \<Longrightarrow> p > 0
    8.28 +
    8.29 +   wreaks havoc here. When the premise includes ALL x :# M. prime x, it 
    8.30 +   leads to the backchaining
    8.31 +
    8.32 +     x > 0  
    8.33 +     prime x 
    8.34 +     x :# M   which is, unfortunately,
    8.35 +     count M x > 0
    8.36 +*)
    8.37 +
    8.38 +
    8.39 +(* useful facts *)
    8.40 +
    8.41 +lemma setsum_Un2: "finite (A Un B) \<Longrightarrow> 
    8.42 +    setsum f (A Un B) = setsum f (A - B) + setsum f (B - A) + 
    8.43 +      setsum f (A Int B)"
    8.44 +  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
    8.45 +  apply (erule ssubst)
    8.46 +  apply (subst setsum_Un_disjoint)
    8.47 +  apply auto
    8.48 +  apply (subst setsum_Un_disjoint)
    8.49 +  apply auto
    8.50 +done
    8.51 +
    8.52 +lemma setprod_Un2: "finite (A Un B) \<Longrightarrow> 
    8.53 +    setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) * 
    8.54 +      setprod f (A Int B)"
    8.55 +  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
    8.56 +  apply (erule ssubst)
    8.57 +  apply (subst setprod_Un_disjoint)
    8.58 +  apply auto
    8.59 +  apply (subst setprod_Un_disjoint)
    8.60 +  apply auto
    8.61 +done
    8.62 + 
    8.63 +(* Should this go in Multiset.thy? *)
    8.64 +(* TN: No longer an intro-rule; needed only once and might get in the way *)
    8.65 +lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
    8.66 +  by (subst multiset_eq_conv_count_eq, blast)
    8.67 +
    8.68 +(* Here is a version of set product for multisets. Is it worth moving
    8.69 +   to multiset.thy? If so, one should similarly define msetsum for abelian 
    8.70 +   semirings, using of_nat. Also, is it worth developing bounded quantifiers 
    8.71 +   "ALL i :# M. P i"? 
    8.72 +*)
    8.73 +
    8.74 +constdefs
    8.75 +  msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b"
    8.76 +  "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
    8.77 +
    8.78 +syntax
    8.79 +  "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" 
    8.80 +      ("(3PROD _:#_. _)" [0, 51, 10] 10)
    8.81 +
    8.82 +translations
    8.83 +  "PROD i :# A. b" == "msetprod (%i. b) A"
    8.84 +
    8.85 +lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
    8.86 +  apply (simp add: msetprod_def power_add)
    8.87 +  apply (subst setprod_Un2)
    8.88 +  apply auto
    8.89 +  apply (subgoal_tac 
    8.90 +      "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
    8.91 +       (PROD x:set_of A - set_of B. f x ^ count A x)")
    8.92 +  apply (erule ssubst)
    8.93 +  apply (subgoal_tac 
    8.94 +      "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
    8.95 +       (PROD x:set_of B - set_of A. f x ^ count B x)")
    8.96 +  apply (erule ssubst)
    8.97 +  apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = 
    8.98 +    (PROD x:set_of A - set_of B. f x ^ count A x) *
    8.99 +    (PROD x:set_of A Int set_of B. f x ^ count A x)")
   8.100 +  apply (erule ssubst)
   8.101 +  apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = 
   8.102 +    (PROD x:set_of B - set_of A. f x ^ count B x) *
   8.103 +    (PROD x:set_of A Int set_of B. f x ^ count B x)")
   8.104 +  apply (erule ssubst)
   8.105 +  apply (subst setprod_timesf)
   8.106 +  apply (force simp add: mult_ac)
   8.107 +  apply (subst setprod_Un_disjoint [symmetric])
   8.108 +  apply (auto intro: setprod_cong)
   8.109 +  apply (subst setprod_Un_disjoint [symmetric])
   8.110 +  apply (auto intro: setprod_cong)
   8.111 +done
   8.112 +
   8.113 +
   8.114 +subsection {* unique factorization: multiset version *}
   8.115 +
   8.116 +lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
   8.117 +    (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
   8.118 +proof (rule nat_less_induct, clarify)
   8.119 +  fix n :: nat
   8.120 +  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = 
   8.121 +      (PROD i :# M. i))"
   8.122 +  assume "(n::nat) > 0"
   8.123 +  then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
   8.124 +    by arith
   8.125 +  moreover 
   8.126 +  {
   8.127 +    assume "n = 1"
   8.128 +    then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
   8.129 +        by (auto simp add: msetprod_def)
   8.130 +  } 
   8.131 +  moreover 
   8.132 +  {
   8.133 +    assume "n > 1" and "prime n"
   8.134 +    then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
   8.135 +      by (auto simp add: msetprod_def)
   8.136 +  } 
   8.137 +  moreover 
   8.138 +  {
   8.139 +    assume "n > 1" and "~ prime n"
   8.140 +    from prems nat_not_prime_eq_prod
   8.141 +      obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
   8.142 +        by blast
   8.143 +    with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
   8.144 +        and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
   8.145 +      by blast
   8.146 +    hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
   8.147 +      by (auto simp add: prems msetprod_Un set_of_union)
   8.148 +    then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
   8.149 +  }
   8.150 +  ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
   8.151 +    by blast
   8.152 +qed
   8.153 +
   8.154 +lemma multiset_prime_factorization_unique_aux:
   8.155 +  fixes a :: nat
   8.156 +  assumes "(ALL p : set_of M. prime p)" and
   8.157 +    "(ALL p : set_of N. prime p)" and
   8.158 +    "(PROD i :# M. i) dvd (PROD i:# N. i)"
   8.159 +  shows
   8.160 +    "count M a <= count N a"
   8.161 +proof cases
   8.162 +  assume "a : set_of M"
   8.163 +  with prems have a: "prime a"
   8.164 +    by auto
   8.165 +  with prems have "a ^ count M a dvd (PROD i :# M. i)"
   8.166 +    by (auto intro: dvd_setprod simp add: msetprod_def)
   8.167 +  also have "... dvd (PROD i :# N. i)"
   8.168 +    by (rule prems)
   8.169 +  also have "... = (PROD i : (set_of N). i ^ (count N i))"
   8.170 +    by (simp add: msetprod_def)
   8.171 +  also have "... = 
   8.172 +      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
   8.173 +    proof (cases)
   8.174 +      assume "a : set_of N"
   8.175 +      hence b: "set_of N = {a} Un (set_of N - {a})"
   8.176 +        by auto
   8.177 +      thus ?thesis
   8.178 +        by (subst (1) b, subst setprod_Un_disjoint, auto)
   8.179 +    next
   8.180 +      assume "a ~: set_of N" 
   8.181 +      thus ?thesis
   8.182 +        by auto
   8.183 +    qed
   8.184 +  finally have "a ^ count M a dvd 
   8.185 +      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
   8.186 +  moreover have "coprime (a ^ count M a)
   8.187 +      (PROD i : (set_of N - {a}). i ^ (count N i))"
   8.188 +    apply (subst nat_gcd_commute)
   8.189 +    apply (rule nat_setprod_coprime)
   8.190 +    apply (rule nat_primes_imp_powers_coprime)
   8.191 +    apply (insert prems, auto) 
   8.192 +    done
   8.193 +  ultimately have "a ^ count M a dvd a^(count N a)"
   8.194 +    by (elim nat_coprime_dvd_mult)
   8.195 +  with a show ?thesis 
   8.196 +    by (intro power_dvd_imp_le, auto)
   8.197 +next
   8.198 +  assume "a ~: set_of M"
   8.199 +  thus ?thesis by auto
   8.200 +qed
   8.201 +
   8.202 +lemma multiset_prime_factorization_unique:
   8.203 +  assumes "(ALL (p::nat) : set_of M. prime p)" and
   8.204 +    "(ALL p : set_of N. prime p)" and
   8.205 +    "(PROD i :# M. i) = (PROD i:# N. i)"
   8.206 +  shows
   8.207 +    "M = N"
   8.208 +proof -
   8.209 +  {
   8.210 +    fix a
   8.211 +    from prems have "count M a <= count N a"
   8.212 +      by (intro multiset_prime_factorization_unique_aux, auto) 
   8.213 +    moreover from prems have "count N a <= count M a"
   8.214 +      by (intro multiset_prime_factorization_unique_aux, auto) 
   8.215 +    ultimately have "count M a = count N a"
   8.216 +      by auto
   8.217 +  }
   8.218 +  thus ?thesis by (simp add:multiset_eq_conv_count_eq)
   8.219 +qed
   8.220 +
   8.221 +constdefs
   8.222 +  multiset_prime_factorization :: "nat => nat multiset"
   8.223 +  "multiset_prime_factorization n ==
   8.224 +     if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
   8.225 +       n = (PROD i :# M. i)))
   8.226 +     else {#}"
   8.227 +
   8.228 +lemma multiset_prime_factorization: "n > 0 ==>
   8.229 +    (ALL p : set_of (multiset_prime_factorization n). prime p) &
   8.230 +       n = (PROD i :# (multiset_prime_factorization n). i)"
   8.231 +  apply (unfold multiset_prime_factorization_def)
   8.232 +  apply clarsimp
   8.233 +  apply (frule multiset_prime_factorization_exists)
   8.234 +  apply clarify
   8.235 +  apply (rule theI)
   8.236 +  apply (insert multiset_prime_factorization_unique, blast)+
   8.237 +done
   8.238 +
   8.239 +
   8.240 +subsection {* Prime factors and multiplicity for nats and ints *}
   8.241 +
   8.242 +class unique_factorization =
   8.243 +
   8.244 +fixes
   8.245 +  multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and
   8.246 +  prime_factors :: "'a \<Rightarrow> 'a set"
   8.247 +
   8.248 +(* definitions for the natural numbers *)
   8.249 +
   8.250 +instantiation nat :: unique_factorization
   8.251 +
   8.252 +begin
   8.253 +
   8.254 +definition
   8.255 +  multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   8.256 +where
   8.257 +  "multiplicity_nat p n = count (multiset_prime_factorization n) p"
   8.258 +
   8.259 +definition
   8.260 +  prime_factors_nat :: "nat \<Rightarrow> nat set"
   8.261 +where
   8.262 +  "prime_factors_nat n = set_of (multiset_prime_factorization n)"
   8.263 +
   8.264 +instance proof qed
   8.265 +
   8.266 +end
   8.267 +
   8.268 +(* definitions for the integers *)
   8.269 +
   8.270 +instantiation int :: unique_factorization
   8.271 +
   8.272 +begin
   8.273 +
   8.274 +definition
   8.275 +  multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
   8.276 +where
   8.277 +  "multiplicity_int p n = multiplicity (nat p) (nat n)"
   8.278 +
   8.279 +definition
   8.280 +  prime_factors_int :: "int \<Rightarrow> int set"
   8.281 +where
   8.282 +  "prime_factors_int n = int ` (prime_factors (nat n))"
   8.283 +
   8.284 +instance proof qed
   8.285 +
   8.286 +end
   8.287 +
   8.288 +
   8.289 +subsection {* Set up transfer *}
   8.290 +
   8.291 +lemma transfer_nat_int_prime_factors: 
   8.292 +  "prime_factors (nat n) = nat ` prime_factors n"
   8.293 +  unfolding prime_factors_int_def apply auto
   8.294 +  by (subst transfer_int_nat_set_return_embed, assumption)
   8.295 +
   8.296 +lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> 
   8.297 +    nat_set (prime_factors n)"
   8.298 +  by (auto simp add: nat_set_def prime_factors_int_def)
   8.299 +
   8.300 +lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   8.301 +  multiplicity (nat p) (nat n) = multiplicity p n"
   8.302 +  by (auto simp add: multiplicity_int_def)
   8.303 +
   8.304 +declare TransferMorphism_nat_int[transfer add return: 
   8.305 +  transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
   8.306 +  transfer_nat_int_multiplicity]
   8.307 +
   8.308 +
   8.309 +lemma transfer_int_nat_prime_factors:
   8.310 +    "prime_factors (int n) = int ` prime_factors n"
   8.311 +  unfolding prime_factors_int_def by auto
   8.312 +
   8.313 +lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 
   8.314 +    nat_set (prime_factors n)"
   8.315 +  by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
   8.316 +
   8.317 +lemma transfer_int_nat_multiplicity: 
   8.318 +    "multiplicity (int p) (int n) = multiplicity p n"
   8.319 +  by (auto simp add: multiplicity_int_def)
   8.320 +
   8.321 +declare TransferMorphism_int_nat[transfer add return: 
   8.322 +  transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
   8.323 +  transfer_int_nat_multiplicity]
   8.324 +
   8.325 +
   8.326 +subsection {* Properties of prime factors and multiplicity for nats and ints *}
   8.327 +
   8.328 +lemma int_prime_factors_ge_0 [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
   8.329 +  by (unfold prime_factors_int_def, auto)
   8.330 +
   8.331 +lemma nat_prime_factors_prime [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
   8.332 +  apply (case_tac "n = 0")
   8.333 +  apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
   8.334 +  apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
   8.335 +done
   8.336 +
   8.337 +lemma int_prime_factors_prime [intro]:
   8.338 +  assumes "n >= 0" and "p : prime_factors (n::int)"
   8.339 +  shows "prime p"
   8.340 +
   8.341 +  apply (rule nat_prime_factors_prime [transferred, of n p])
   8.342 +  using prems apply auto
   8.343 +done
   8.344 +
   8.345 +lemma nat_prime_factors_gt_0 [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
   8.346 +  by (frule nat_prime_factors_prime, auto)
   8.347 +
   8.348 +lemma int_prime_factors_gt_0 [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
   8.349 +    p > (0::int)"
   8.350 +  by (frule (1) int_prime_factors_prime, auto)
   8.351 +
   8.352 +lemma nat_prime_factors_finite [iff]: "finite (prime_factors (n::nat))"
   8.353 +  by (unfold prime_factors_nat_def, auto)
   8.354 +
   8.355 +lemma int_prime_factors_finite [iff]: "finite (prime_factors (n::int))"
   8.356 +  by (unfold prime_factors_int_def, auto)
   8.357 +
   8.358 +lemma nat_prime_factors_altdef: "prime_factors (n::nat) = 
   8.359 +    {p. multiplicity p n > 0}"
   8.360 +  by (force simp add: prime_factors_nat_def multiplicity_nat_def)
   8.361 +
   8.362 +lemma int_prime_factors_altdef: "prime_factors (n::int) = 
   8.363 +    {p. p >= 0 & multiplicity p n > 0}"
   8.364 +  apply (unfold prime_factors_int_def multiplicity_int_def)
   8.365 +  apply (subst nat_prime_factors_altdef)
   8.366 +  apply (auto simp add: image_def)
   8.367 +done
   8.368 +
   8.369 +lemma nat_prime_factorization: "(n::nat) > 0 \<Longrightarrow> 
   8.370 +    n = (PROD p : prime_factors n. p^(multiplicity p n))"
   8.371 +  by (frule multiset_prime_factorization, 
   8.372 +    simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
   8.373 +
   8.374 +thm nat_prime_factorization [transferred] 
   8.375 +
   8.376 +lemma int_prime_factorization: 
   8.377 +  assumes "(n::int) > 0"
   8.378 +  shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
   8.379 +
   8.380 +  apply (rule nat_prime_factorization [transferred, of n])
   8.381 +  using prems apply auto
   8.382 +done
   8.383 +
   8.384 +lemma nat_neq_zero_eq_gt_zero: "((x::nat) ~= 0) = (x > 0)"
   8.385 +  by auto
   8.386 +
   8.387 +lemma nat_prime_factorization_unique: 
   8.388 +    "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
   8.389 +      n = (PROD p : S. p^(f p)) \<Longrightarrow>
   8.390 +        S = prime_factors n & (ALL p. f p = multiplicity p n)"
   8.391 +  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
   8.392 +      f")
   8.393 +  apply (unfold prime_factors_nat_def multiplicity_nat_def)
   8.394 +  apply (simp add: set_of_def count_def Abs_multiset_inverse multiset_def)
   8.395 +  apply (unfold multiset_prime_factorization_def)
   8.396 +  apply (subgoal_tac "n > 0")
   8.397 +  prefer 2
   8.398 +  apply force
   8.399 +  apply (subst if_P, assumption)
   8.400 +  apply (rule the1_equality)
   8.401 +  apply (rule ex_ex1I)
   8.402 +  apply (rule multiset_prime_factorization_exists, assumption)
   8.403 +  apply (rule multiset_prime_factorization_unique)
   8.404 +  apply force
   8.405 +  apply force
   8.406 +  apply force
   8.407 +  unfolding set_of_def count_def msetprod_def
   8.408 +  apply (subgoal_tac "f : multiset")
   8.409 +  apply (auto simp only: Abs_multiset_inverse)
   8.410 +  unfolding multiset_def apply force 
   8.411 +done
   8.412 +
   8.413 +lemma nat_prime_factors_characterization: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
   8.414 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   8.415 +      prime_factors n = S"
   8.416 +  by (rule nat_prime_factorization_unique [THEN conjunct1, symmetric],
   8.417 +    assumption+)
   8.418 +
   8.419 +lemma nat_prime_factors_characterization': 
   8.420 +  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
   8.421 +    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   8.422 +      prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
   8.423 +  apply (rule nat_prime_factors_characterization)
   8.424 +  apply auto
   8.425 +done
   8.426 +
   8.427 +(* A minor glitch:*)
   8.428 +
   8.429 +thm nat_prime_factors_characterization' 
   8.430 +    [where f = "%x. f (int (x::nat))", 
   8.431 +      transferred direction: nat "op <= (0::int)", rule_format]
   8.432 +
   8.433 +(*
   8.434 +  Transfer isn't smart enough to know that the "0 < f p" should 
   8.435 +  remain a comparison between nats. But the transfer still works. 
   8.436 +*)
   8.437 +
   8.438 +lemma int_primes_characterization' [rule_format]: 
   8.439 +    "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
   8.440 +      (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   8.441 +        prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) = 
   8.442 +          {p. p >= 0 & 0 < f p}"
   8.443 +
   8.444 +  apply (insert nat_prime_factors_characterization' 
   8.445 +    [where f = "%x. f (int (x::nat))", 
   8.446 +    transferred direction: nat "op <= (0::int)"])
   8.447 +  apply auto
   8.448 +done
   8.449 +
   8.450 +lemma int_prime_factors_characterization: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
   8.451 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   8.452 +      prime_factors n = S"
   8.453 +  apply simp
   8.454 +  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   8.455 +  apply (simp only:)
   8.456 +  apply (subst int_primes_characterization')
   8.457 +  apply auto
   8.458 +  apply (auto simp add: int_prime_ge_0)
   8.459 +done
   8.460 +
   8.461 +lemma nat_multiplicity_characterization: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
   8.462 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   8.463 +      multiplicity p n = f p"
   8.464 +  by (frule nat_prime_factorization_unique [THEN conjunct2, rule_format, 
   8.465 +    symmetric], auto)
   8.466 +
   8.467 +lemma nat_multiplicity_characterization': "finite {p. 0 < f (p::nat)} \<longrightarrow>
   8.468 +    (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
   8.469 +      multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
   8.470 +  apply (rule impI)+
   8.471 +  apply (rule nat_multiplicity_characterization)
   8.472 +  apply auto
   8.473 +done
   8.474 +
   8.475 +lemma int_multiplicity_characterization' [rule_format]: 
   8.476 +  "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
   8.477 +    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
   8.478 +      multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
   8.479 +
   8.480 +  apply (insert nat_multiplicity_characterization' 
   8.481 +    [where f = "%x. f (int (x::nat))", 
   8.482 +      transferred direction: nat "op <= (0::int)", rule_format])
   8.483 +  apply auto
   8.484 +done
   8.485 +
   8.486 +lemma int_multiplicity_characterization: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
   8.487 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   8.488 +      p >= 0 \<Longrightarrow> multiplicity p n = f p"
   8.489 +  apply simp
   8.490 +  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   8.491 +  apply (simp only:)
   8.492 +  apply (subst int_multiplicity_characterization')
   8.493 +  apply auto
   8.494 +  apply (auto simp add: int_prime_ge_0)
   8.495 +done
   8.496 +
   8.497 +lemma nat_multiplicity_zero [simp]: "multiplicity (p::nat) 0 = 0"
   8.498 +  by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
   8.499 +
   8.500 +lemma int_multiplicity_zero [simp]: "multiplicity (p::int) 0 = 0"
   8.501 +  by (simp add: multiplicity_int_def) 
   8.502 +
   8.503 +lemma nat_multiplicity_one [simp]: "multiplicity p (1::nat) = 0"
   8.504 +  by (subst nat_multiplicity_characterization [where f = "%x. 0"], auto)
   8.505 +
   8.506 +lemma int_multiplicity_one [simp]: "multiplicity p (1::int) = 0"
   8.507 +  by (simp add: multiplicity_int_def)
   8.508 +
   8.509 +lemma nat_multiplicity_prime [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
   8.510 +  apply (subst nat_multiplicity_characterization
   8.511 +      [where f = "(%q. if q = p then 1 else 0)"])
   8.512 +  apply auto
   8.513 +  apply (case_tac "x = p")
   8.514 +  apply auto
   8.515 +done
   8.516 +
   8.517 +lemma int_multiplicity_prime [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
   8.518 +  unfolding prime_int_def multiplicity_int_def by auto
   8.519 +
   8.520 +lemma nat_multiplicity_prime_power [simp]: "prime (p::nat) \<Longrightarrow> 
   8.521 +    multiplicity p (p^n) = n"
   8.522 +  apply (case_tac "n = 0")
   8.523 +  apply auto
   8.524 +  apply (subst nat_multiplicity_characterization
   8.525 +      [where f = "(%q. if q = p then n else 0)"])
   8.526 +  apply auto
   8.527 +  apply (case_tac "x = p")
   8.528 +  apply auto
   8.529 +done
   8.530 +
   8.531 +lemma int_multiplicity_prime_power [simp]: "prime (p::int) \<Longrightarrow> 
   8.532 +    multiplicity p (p^n) = n"
   8.533 +  apply (frule int_prime_ge_0)
   8.534 +  apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
   8.535 +done
   8.536 +
   8.537 +lemma nat_multiplicity_nonprime [simp]: "~ prime (p::nat) \<Longrightarrow> 
   8.538 +    multiplicity p n = 0"
   8.539 +  apply (case_tac "n = 0")
   8.540 +  apply auto
   8.541 +  apply (frule multiset_prime_factorization)
   8.542 +  apply (auto simp add: set_of_def multiplicity_nat_def)
   8.543 +done
   8.544 +
   8.545 +lemma int_multiplicity_nonprime [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
   8.546 +  by (unfold multiplicity_int_def prime_int_def, auto)
   8.547 +
   8.548 +lemma nat_multiplicity_not_factor [simp]: 
   8.549 +    "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
   8.550 +  by (subst (asm) nat_prime_factors_altdef, auto)
   8.551 +
   8.552 +lemma int_multiplicity_not_factor [simp]: 
   8.553 +    "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
   8.554 +  by (subst (asm) int_prime_factors_altdef, auto)
   8.555 +
   8.556 +lemma nat_multiplicity_product_aux: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
   8.557 +    (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
   8.558 +    (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   8.559 +  apply (rule nat_prime_factorization_unique)
   8.560 +  apply (simp only: nat_prime_factors_altdef)
   8.561 +  apply auto
   8.562 +  apply (subst power_add)
   8.563 +  apply (subst setprod_timesf)
   8.564 +  apply (rule arg_cong2)back back
   8.565 +  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 
   8.566 +      (prime_factors l - prime_factors k)")
   8.567 +  apply (erule ssubst)
   8.568 +  apply (subst setprod_Un_disjoint)
   8.569 +  apply auto
   8.570 +  apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = 
   8.571 +      (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
   8.572 +  apply (erule ssubst)
   8.573 +  apply (simp add: setprod_1)
   8.574 +  apply (erule nat_prime_factorization)
   8.575 +  apply (rule setprod_cong, auto)
   8.576 +  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
   8.577 +      (prime_factors k - prime_factors l)")
   8.578 +  apply (erule ssubst)
   8.579 +  apply (subst setprod_Un_disjoint)
   8.580 +  apply auto
   8.581 +  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
   8.582 +      (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
   8.583 +  apply (erule ssubst)
   8.584 +  apply (simp add: setprod_1)
   8.585 +  apply (erule nat_prime_factorization)
   8.586 +  apply (rule setprod_cong, auto)
   8.587 +done
   8.588 +
   8.589 +(* transfer doesn't have the same problem here with the right 
   8.590 +   choice of rules. *)
   8.591 +
   8.592 +lemma int_multiplicity_product_aux: 
   8.593 +  assumes "(k::int) > 0" and "l > 0"
   8.594 +  shows 
   8.595 +    "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
   8.596 +    (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   8.597 +
   8.598 +  apply (rule nat_multiplicity_product_aux [transferred, of l k])
   8.599 +  using prems apply auto
   8.600 +done
   8.601 +
   8.602 +lemma nat_prime_factors_product: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
   8.603 +    prime_factors k Un prime_factors l"
   8.604 +  by (rule nat_multiplicity_product_aux [THEN conjunct1, symmetric])
   8.605 +
   8.606 +lemma int_prime_factors_product: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
   8.607 +    prime_factors k Un prime_factors l"
   8.608 +  by (rule int_multiplicity_product_aux [THEN conjunct1, symmetric])
   8.609 +
   8.610 +lemma nat_multiplicity_product: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = 
   8.611 +    multiplicity p k + multiplicity p l"
   8.612 +  by (rule nat_multiplicity_product_aux [THEN conjunct2, rule_format, 
   8.613 +      symmetric])
   8.614 +
   8.615 +lemma int_multiplicity_product: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
   8.616 +    multiplicity p (k * l) = multiplicity p k + multiplicity p l"
   8.617 +  by (rule int_multiplicity_product_aux [THEN conjunct2, rule_format, 
   8.618 +      symmetric])
   8.619 +
   8.620 +lemma nat_multiplicity_setprod: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> 
   8.621 +    multiplicity (p::nat) (PROD x : S. f x) = 
   8.622 +      (SUM x : S. multiplicity p (f x))"
   8.623 +  apply (induct set: finite)
   8.624 +  apply auto
   8.625 +  apply (subst nat_multiplicity_product)
   8.626 +  apply auto
   8.627 +done
   8.628 +
   8.629 +(* Transfer is delicate here for two reasons: first, because there is
   8.630 +   an implicit quantifier over functions (f), and, second, because the 
   8.631 +   product over the multiplicity should not be translated to an integer 
   8.632 +   product.
   8.633 +
   8.634 +   The way to handle the first is to use quantifier rules for functions.
   8.635 +   The way to handle the second is to turn off the offending rule.
   8.636 +*)
   8.637 +
   8.638 +lemma transfer_nat_int_sum_prod_closure3:
   8.639 +  "(SUM x : A. int (f x)) >= 0"
   8.640 +  "(PROD x : A. int (f x)) >= 0"
   8.641 +  apply (rule setsum_nonneg, auto)
   8.642 +  apply (rule setprod_nonneg, auto)
   8.643 +done
   8.644 +
   8.645 +declare TransferMorphism_nat_int[transfer 
   8.646 +  add return: transfer_nat_int_sum_prod_closure3
   8.647 +  del: transfer_nat_int_sum_prod2 (1)]
   8.648 +
   8.649 +lemma int_multiplicity_setprod: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
   8.650 +  (ALL x : S. f x > 0) \<Longrightarrow> 
   8.651 +    multiplicity (p::int) (PROD x : S. f x) = 
   8.652 +      (SUM x : S. multiplicity p (f x))"
   8.653 +
   8.654 +  apply (frule nat_multiplicity_setprod
   8.655 +    [where f = "%x. nat(int(nat(f x)))", 
   8.656 +      transferred direction: nat "op <= (0::int)"])
   8.657 +  apply auto
   8.658 +  apply (subst (asm) setprod_cong)
   8.659 +  apply (rule refl)
   8.660 +  apply (rule if_P)
   8.661 +  apply auto
   8.662 +  apply (rule setsum_cong)
   8.663 +  apply auto
   8.664 +done
   8.665 +
   8.666 +declare TransferMorphism_nat_int[transfer 
   8.667 +  add return: transfer_nat_int_sum_prod2 (1)]
   8.668 +
   8.669 +lemma nat_multiplicity_prod_prime_powers:
   8.670 +    "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
   8.671 +       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   8.672 +  apply (subgoal_tac "(PROD p : S. p ^ f p) = 
   8.673 +      (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
   8.674 +  apply (erule ssubst)
   8.675 +  apply (subst nat_multiplicity_characterization)
   8.676 +  prefer 5 apply (rule refl)
   8.677 +  apply (rule refl)
   8.678 +  apply auto
   8.679 +  apply (subst setprod_mono_one_right)
   8.680 +  apply assumption
   8.681 +  prefer 3
   8.682 +  apply (rule setprod_cong)
   8.683 +  apply (rule refl)
   8.684 +  apply auto
   8.685 +done
   8.686 +
   8.687 +(* Here the issue with transfer is the implicit quantifier over S *)
   8.688 +
   8.689 +lemma int_multiplicity_prod_prime_powers:
   8.690 +    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
   8.691 +       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   8.692 +
   8.693 +  apply (subgoal_tac "int ` nat ` S = S")
   8.694 +  apply (frule nat_multiplicity_prod_prime_powers [where f = "%x. f(int x)" 
   8.695 +    and S = "nat ` S", transferred])
   8.696 +  apply auto
   8.697 +  apply (subst prime_int_def [symmetric])
   8.698 +  apply auto
   8.699 +  apply (subgoal_tac "xb >= 0")
   8.700 +  apply force
   8.701 +  apply (rule int_prime_ge_0)
   8.702 +  apply force
   8.703 +  apply (subst transfer_nat_int_set_return_embed)
   8.704 +  apply (unfold nat_set_def, auto)
   8.705 +done
   8.706 +
   8.707 +lemma nat_multiplicity_distinct_prime_power: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
   8.708 +    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   8.709 +  apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
   8.710 +  apply (erule ssubst)
   8.711 +  apply (subst nat_multiplicity_prod_prime_powers)
   8.712 +  apply auto
   8.713 +done
   8.714 +
   8.715 +lemma int_multiplicity_distinct_prime_power: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
   8.716 +    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   8.717 +  apply (frule int_prime_ge_0 [of q])
   8.718 +  apply (frule nat_multiplicity_distinct_prime_power [transferred leaving: n]) 
   8.719 +  prefer 4
   8.720 +  apply assumption
   8.721 +  apply auto
   8.722 +done
   8.723 +
   8.724 +lemma nat_dvd_multiplicity: 
   8.725 +    "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
   8.726 +  apply (case_tac "x = 0")
   8.727 +  apply (auto simp add: dvd_def nat_multiplicity_product)
   8.728 +done
   8.729 +
   8.730 +lemma int_dvd_multiplicity: 
   8.731 +    "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
   8.732 +      multiplicity p x <= multiplicity p y"
   8.733 +  apply (case_tac "x = 0")
   8.734 +  apply (auto simp add: dvd_def)
   8.735 +  apply (subgoal_tac "0 < k")
   8.736 +  apply (auto simp add: int_multiplicity_product)
   8.737 +  apply (erule zero_less_mult_pos)
   8.738 +  apply arith
   8.739 +done
   8.740 +
   8.741 +lemma nat_dvd_prime_factors [intro]:
   8.742 +    "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   8.743 +  apply (simp only: nat_prime_factors_altdef)
   8.744 +  apply auto
   8.745 +  apply (frule nat_dvd_multiplicity)
   8.746 +  apply auto
   8.747 +(* It is a shame that auto and arith don't get this. *)
   8.748 +  apply (erule order_less_le_trans)back
   8.749 +  apply assumption
   8.750 +done
   8.751 +
   8.752 +lemma int_dvd_prime_factors [intro]:
   8.753 +    "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   8.754 +  apply (auto simp add: int_prime_factors_altdef)
   8.755 +  apply (erule order_less_le_trans)
   8.756 +  apply (rule int_dvd_multiplicity)
   8.757 +  apply auto
   8.758 +done
   8.759 +
   8.760 +lemma nat_multiplicity_dvd: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
   8.761 +    ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
   8.762 +      x dvd y"
   8.763 +  apply (subst nat_prime_factorization [of x], assumption)
   8.764 +  apply (subst nat_prime_factorization [of y], assumption)
   8.765 +  apply (rule setprod_dvd_setprod_subset2)
   8.766 +  apply force
   8.767 +  apply (subst nat_prime_factors_altdef)+
   8.768 +  apply auto
   8.769 +(* Again, a shame that auto and arith don't get this. *)
   8.770 +  apply (drule_tac x = xa in spec, auto)
   8.771 +  apply (rule le_imp_power_dvd)
   8.772 +  apply blast
   8.773 +done
   8.774 +
   8.775 +lemma int_multiplicity_dvd: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
   8.776 +    ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
   8.777 +      x dvd y"
   8.778 +  apply (subst int_prime_factorization [of x], assumption)
   8.779 +  apply (subst int_prime_factorization [of y], assumption)
   8.780 +  apply (rule setprod_dvd_setprod_subset2)
   8.781 +  apply force
   8.782 +  apply (subst int_prime_factors_altdef)+
   8.783 +  apply auto
   8.784 +  apply (rule dvd_power_le)
   8.785 +  apply auto
   8.786 +  apply (drule_tac x = xa in spec)
   8.787 +  apply (erule impE)
   8.788 +  apply auto
   8.789 +done
   8.790 +
   8.791 +lemma nat_multiplicity_dvd': "(0::nat) < x \<Longrightarrow> 
   8.792 +    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   8.793 +  apply (cases "y = 0")
   8.794 +  apply auto
   8.795 +  apply (rule nat_multiplicity_dvd, auto)
   8.796 +  apply (case_tac "prime p")
   8.797 +  apply auto
   8.798 +done
   8.799 +
   8.800 +lemma int_multiplicity_dvd': "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
   8.801 +    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   8.802 +  apply (cases "y = 0")
   8.803 +  apply auto
   8.804 +  apply (rule int_multiplicity_dvd, auto)
   8.805 +  apply (case_tac "prime p")
   8.806 +  apply auto
   8.807 +done
   8.808 +
   8.809 +lemma nat_dvd_multiplicity_eq: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
   8.810 +    (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
   8.811 +  by (auto intro: nat_dvd_multiplicity nat_multiplicity_dvd)
   8.812 +
   8.813 +lemma int_dvd_multiplicity_eq: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
   8.814 +    (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
   8.815 +  by (auto intro: int_dvd_multiplicity int_multiplicity_dvd)
   8.816 +
   8.817 +lemma nat_prime_factors_altdef2: "(n::nat) > 0 \<Longrightarrow> 
   8.818 +    (p : prime_factors n) = (prime p & p dvd n)"
   8.819 +  apply (case_tac "prime p")
   8.820 +  apply auto
   8.821 +  apply (subst nat_prime_factorization [where n = n], assumption)
   8.822 +  apply (rule dvd_trans) 
   8.823 +  apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   8.824 +  apply (subst (asm) nat_prime_factors_altdef, force)
   8.825 +  apply (rule dvd_setprod)
   8.826 +  apply auto  
   8.827 +  apply (subst nat_prime_factors_altdef)
   8.828 +  apply (subst (asm) nat_dvd_multiplicity_eq)
   8.829 +  apply auto
   8.830 +  apply (drule spec [where x = p])
   8.831 +  apply auto
   8.832 +done
   8.833 +
   8.834 +lemma int_prime_factors_altdef2: 
   8.835 +  assumes "(n::int) > 0" 
   8.836 +  shows "(p : prime_factors n) = (prime p & p dvd n)"
   8.837 +
   8.838 +  apply (case_tac "p >= 0")
   8.839 +  apply (rule nat_prime_factors_altdef2 [transferred])
   8.840 +  using prems apply auto
   8.841 +  apply (auto simp add: int_prime_ge_0 int_prime_factors_ge_0)
   8.842 +done
   8.843 +
   8.844 +lemma nat_multiplicity_eq:
   8.845 +  fixes x and y::nat 
   8.846 +  assumes [arith]: "x > 0" "y > 0" and
   8.847 +    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   8.848 +  shows "x = y"
   8.849 +
   8.850 +  apply (rule dvd_anti_sym)
   8.851 +  apply (auto intro: nat_multiplicity_dvd') 
   8.852 +done
   8.853 +
   8.854 +lemma int_multiplicity_eq:
   8.855 +  fixes x and y::int 
   8.856 +  assumes [arith]: "x > 0" "y > 0" and
   8.857 +    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   8.858 +  shows "x = y"
   8.859 +
   8.860 +  apply (rule dvd_anti_sym [transferred])
   8.861 +  apply (auto intro: int_multiplicity_dvd') 
   8.862 +done
   8.863 +
   8.864 +
   8.865 +subsection {* An application *}
   8.866 +
   8.867 +lemma nat_gcd_eq: 
   8.868 +  assumes pos [arith]: "x > 0" "y > 0"
   8.869 +  shows "gcd (x::nat) y = 
   8.870 +    (PROD p: prime_factors x Un prime_factors y. 
   8.871 +      p ^ (min (multiplicity p x) (multiplicity p y)))"
   8.872 +proof -
   8.873 +  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   8.874 +      p ^ (min (multiplicity p x) (multiplicity p y)))"
   8.875 +  have [arith]: "z > 0"
   8.876 +    unfolding z_def by (rule setprod_pos_nat, auto)
   8.877 +  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   8.878 +      min (multiplicity p x) (multiplicity p y)"
   8.879 +    unfolding z_def
   8.880 +    apply (subst nat_multiplicity_prod_prime_powers)
   8.881 +    apply (auto simp add: nat_multiplicity_not_factor)
   8.882 +    done
   8.883 +  have "z dvd x" 
   8.884 +    by (intro nat_multiplicity_dvd', auto simp add: aux)
   8.885 +  moreover have "z dvd y" 
   8.886 +    by (intro nat_multiplicity_dvd', auto simp add: aux)
   8.887 +  moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
   8.888 +    apply auto
   8.889 +    apply (case_tac "w = 0", auto)
   8.890 +    apply (erule nat_multiplicity_dvd')
   8.891 +    apply (auto intro: nat_dvd_multiplicity simp add: aux)
   8.892 +    done
   8.893 +  ultimately have "z = gcd x y"
   8.894 +    by (subst nat_gcd_unique [symmetric], blast)
   8.895 +  thus ?thesis
   8.896 +    unfolding z_def by auto
   8.897 +qed
   8.898 +
   8.899 +lemma nat_lcm_eq: 
   8.900 +  assumes pos [arith]: "x > 0" "y > 0"
   8.901 +  shows "lcm (x::nat) y = 
   8.902 +    (PROD p: prime_factors x Un prime_factors y. 
   8.903 +      p ^ (max (multiplicity p x) (multiplicity p y)))"
   8.904 +proof -
   8.905 +  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   8.906 +      p ^ (max (multiplicity p x) (multiplicity p y)))"
   8.907 +  have [arith]: "z > 0"
   8.908 +    unfolding z_def by (rule setprod_pos_nat, auto)
   8.909 +  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   8.910 +      max (multiplicity p x) (multiplicity p y)"
   8.911 +    unfolding z_def
   8.912 +    apply (subst nat_multiplicity_prod_prime_powers)
   8.913 +    apply (auto simp add: nat_multiplicity_not_factor)
   8.914 +    done
   8.915 +  have "x dvd z" 
   8.916 +    by (intro nat_multiplicity_dvd', auto simp add: aux)
   8.917 +  moreover have "y dvd z" 
   8.918 +    by (intro nat_multiplicity_dvd', auto simp add: aux)
   8.919 +  moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
   8.920 +    apply auto
   8.921 +    apply (case_tac "w = 0", auto)
   8.922 +    apply (rule nat_multiplicity_dvd')
   8.923 +    apply (auto intro: nat_dvd_multiplicity simp add: aux)
   8.924 +    done
   8.925 +  ultimately have "z = lcm x y"
   8.926 +    by (subst nat_lcm_unique [symmetric], blast)
   8.927 +  thus ?thesis
   8.928 +    unfolding z_def by auto
   8.929 +qed
   8.930 +
   8.931 +lemma nat_multiplicity_gcd: 
   8.932 +  assumes [arith]: "x > 0" "y > 0"
   8.933 +  shows "multiplicity (p::nat) (gcd x y) = 
   8.934 +    min (multiplicity p x) (multiplicity p y)"
   8.935 +
   8.936 +  apply (subst nat_gcd_eq)
   8.937 +  apply auto
   8.938 +  apply (subst nat_multiplicity_prod_prime_powers)
   8.939 +  apply auto
   8.940 +done
   8.941 +
   8.942 +lemma nat_multiplicity_lcm: 
   8.943 +  assumes [arith]: "x > 0" "y > 0"
   8.944 +  shows "multiplicity (p::nat) (lcm x y) = 
   8.945 +    max (multiplicity p x) (multiplicity p y)"
   8.946 +
   8.947 +  apply (subst nat_lcm_eq)
   8.948 +  apply auto
   8.949 +  apply (subst nat_multiplicity_prod_prime_powers)
   8.950 +  apply auto
   8.951 +done
   8.952 +
   8.953 +lemma nat_gcd_lcm_distrib: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
   8.954 +  apply (case_tac "x = 0 | y = 0 | z = 0") 
   8.955 +  apply auto
   8.956 +  apply (rule nat_multiplicity_eq)
   8.957 +  apply (auto simp add: nat_multiplicity_gcd nat_multiplicity_lcm 
   8.958 +      nat_lcm_pos)
   8.959 +done
   8.960 +
   8.961 +lemma int_gcd_lcm_distrib: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
   8.962 +  apply (subst (1 2 3) int_gcd_abs)
   8.963 +  apply (subst int_lcm_abs)
   8.964 +  apply (subst (2) abs_of_nonneg)
   8.965 +  apply force
   8.966 +  apply (rule nat_gcd_lcm_distrib [transferred])
   8.967 +  apply auto
   8.968 +done
   8.969 +
   8.970 +end