src/HOL/Number_Theory/Primes.thy
changeset 55238 7ddb889e23bd
parent 55215 b6c926e67350
child 55242 413ec965f95d
     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.12 +by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
    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.34 +  from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
    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