author paulson Sat Feb 01 20:38:29 2014 +0000 (2014-02-01) changeset 55238 7ddb889e23bd parent 55237 1e341728bae9 child 55241 ef601c60ccbe
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Sat Feb 01 20:46:19 2014 +0100
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Sat Feb 01 20:38:29 2014 +0000
1.3 @@ -462,4 +462,64 @@
1.4    thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
1.5  qed
1.6
1.7 +subsection {*Chinese Remainder Theorem Variants*}
1.8 +
1.9 +lemma bezout_gcd_nat:
1.10 +  fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
1.11 +  using bezout_nat[of a b]
1.13 +  gcd_nat.right_neutral mult_0)
1.14 +
1.15 +lemma gcd_bezout_sum_nat:
1.16 +  fixes a::nat
1.17 +  assumes "a * x + b * y = d"
1.18 +  shows "gcd a b dvd d"
1.19 +proof-
1.20 +  let ?g = "gcd a b"
1.21 +    have dv: "?g dvd a*x" "?g dvd b * y"
1.22 +      by simp_all
1.23 +    from dvd_add[OF dv] assms
1.24 +    show ?thesis by auto
1.25 +qed
1.26 +
1.27 +
1.28 +text {* A binary form of the Chinese Remainder Theorem. *}
1.29 +
1.30 +lemma chinese_remainder:
1.31 +  fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
1.32 +  shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
1.33 +proof-
1.35 +  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
1.36 +    and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
1.37 +  then have d12: "d1 = 1" "d2 =1"
1.38 +    by (metis ab coprime_nat)+
1.39 +  let ?x = "v * a * x1 + u * b * x2"
1.40 +  let ?q1 = "v * x1 + u * y2"
1.41 +  let ?q2 = "v * y1 + u * x2"
1.42 +  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
1.43 +  have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
1.44 +    apply (auto simp add: algebra_simps)
1.45 +    apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
1.46 +    done
1.47 +  thus ?thesis by blast
1.48 +qed
1.49 +
1.50 +text {* Primality *}
1.51 +
1.52 +lemma coprime_bezout_strong:
1.53 +  fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
1.54 +  shows "\<exists>x y. a * x = b * y + 1"
1.55 +by (metis assms bezout_nat gcd_nat.left_neutral)
1.56 +
1.57 +lemma bezout_prime:
1.58 +  assumes p: "prime p" and pa: "\<not> p dvd a"
1.59 +  shows "\<exists>x y. a*x = Suc (p*y)"
1.60 +proof-
1.61 +  have ap: "coprime a p"
1.62 +    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
1.63 +  from coprime_bezout_strong[OF ap] show ?thesis
1.64 +    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
1.65 +qed
1.66 +
1.67  end
```