tuned
authorhaftmann
Thu Nov 23 17:03:26 2017 +0000 (3 months ago)
changeset 6708659d07a95be0e
parent 67085 f5d7f37b4143
child 67087 733017b19de9
tuned
src/HOL/Number_Theory/Cong.thy
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:21 2017 +0000
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:26 2017 +0000
     1.3 @@ -558,50 +558,27 @@
     1.4    apply (metis coprime_cong_mult_int prod_coprime_right)
     1.5    done
     1.6  
     1.7 -lemma binary_chinese_remainder_aux_nat:
     1.8 -  fixes m1 m2 :: nat
     1.9 -  assumes a: "coprime m1 m2"
    1.10 -  shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
    1.11 -proof -
    1.12 -  from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
    1.13 -    by auto
    1.14 -  from a have b: "coprime m2 m1"
    1.15 -    by (simp add: ac_simps)
    1.16 -  from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
    1.17 -    by auto
    1.18 -  have "[m1 * x1 = 0] (mod m1)"
    1.19 -    by (simp add: cong_mult_self_left)
    1.20 -  moreover have "[m2 * x2 = 0] (mod m2)"
    1.21 -    by (simp add: cong_mult_self_left)
    1.22 -  ultimately show ?thesis
    1.23 -    using 1 2 by blast
    1.24 -qed
    1.25 -
    1.26 -lemma binary_chinese_remainder_aux_int:
    1.27 -  fixes m1 m2 :: int
    1.28 -  assumes a: "coprime m1 m2"
    1.29 -  shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
    1.30 -proof -
    1.31 -  from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
    1.32 -    by auto
    1.33 -  from a have b: "coprime m2 m1"
    1.34 -    by (simp add: ac_simps)
    1.35 -  from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
    1.36 -    by auto
    1.37 -  have "[m1 * x1 = 0] (mod m1)"
    1.38 -    by (simp add: cong_mult_self_left)
    1.39 -  moreover have "[m2 * x2 = 0] (mod m2)"
    1.40 -    by (simp add: cong_mult_self_left)
    1.41 -  ultimately show ?thesis
    1.42 -    using 1 2 by blast
    1.43 -qed
    1.44 -
    1.45  lemma binary_chinese_remainder_nat:
    1.46    fixes m1 m2 :: nat
    1.47    assumes a: "coprime m1 m2"
    1.48    shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
    1.49  proof -
    1.50 -  from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
    1.51 +  have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
    1.52 +  proof -
    1.53 +    from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
    1.54 +      by auto
    1.55 +    from a have b: "coprime m2 m1"
    1.56 +      by (simp add: ac_simps)
    1.57 +    from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
    1.58 +      by auto
    1.59 +    have "[m1 * x1 = 0] (mod m1)"
    1.60 +      by (simp add: cong_mult_self_left)
    1.61 +    moreover have "[m2 * x2 = 0] (mod m2)"
    1.62 +      by (simp add: cong_mult_self_left)
    1.63 +    ultimately show ?thesis
    1.64 +      using 1 2 by blast
    1.65 +  qed
    1.66 +  then obtain b1 b2
    1.67      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
    1.68        and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
    1.69      by blast
    1.70 @@ -622,7 +599,22 @@
    1.71    assumes a: "coprime m1 m2"
    1.72    shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
    1.73  proof -
    1.74 -  from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
    1.75 +  have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
    1.76 +  proof -
    1.77 +    from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
    1.78 +      by auto
    1.79 +    from a have b: "coprime m2 m1"
    1.80 +      by (simp add: ac_simps)
    1.81 +    from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
    1.82 +      by auto
    1.83 +    have "[m1 * x1 = 0] (mod m1)"
    1.84 +     by (simp add: cong_mult_self_left)
    1.85 +    moreover have "[m2 * x2 = 0] (mod m2)"
    1.86 +      by (simp add: cong_mult_self_left)
    1.87 +    ultimately show ?thesis
    1.88 +      using 1 2 by blast
    1.89 +  qed
    1.90 +  then obtain b1 b2
    1.91      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)"
    1.92        and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
    1.93      by blast
    1.94 @@ -706,27 +698,6 @@
    1.95    with less 1 2 show ?thesis by auto
    1.96   qed
    1.97  
    1.98 -lemma chinese_remainder_aux_nat:
    1.99 -  fixes A :: "'a set"
   1.100 -    and m :: "'a \<Rightarrow> nat"
   1.101 -  assumes fin: "finite A"
   1.102 -    and cop: "\<forall>i \<in> A. (\<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
   1.103 -  shows "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
   1.104 -proof (rule finite_set_choice, rule fin, rule ballI)
   1.105 -  fix i
   1.106 -  assume "i \<in> A"
   1.107 -  with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
   1.108 -    by (intro prod_coprime_left) auto
   1.109 -  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)"
   1.110 -    by (elim cong_solve_coprime_nat)
   1.111 -  then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
   1.112 -    by auto
   1.113 -  moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
   1.114 -    by (simp add: cong_0_iff)
   1.115 -  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
   1.116 -    by blast
   1.117 -qed
   1.118 -
   1.119  lemma chinese_remainder_nat:
   1.120    fixes A :: "'a set"
   1.121      and m :: "'a \<Rightarrow> nat"
   1.122 @@ -735,8 +706,22 @@
   1.123      and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)"
   1.124    shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)"
   1.125  proof -
   1.126 -  from chinese_remainder_aux_nat [OF fin cop]
   1.127 -  obtain b where b: "\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
   1.128 +  have "\<exists>b. (\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
   1.129 +  proof (rule finite_set_choice, rule fin, rule ballI)
   1.130 +    fix i
   1.131 +    assume "i \<in> A"
   1.132 +    with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
   1.133 +      by (intro prod_coprime_left) auto
   1.134 +    then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)"
   1.135 +      by (elim cong_solve_coprime_nat)
   1.136 +    then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
   1.137 +      by auto
   1.138 +    moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
   1.139 +      by (simp add: cong_0_iff)
   1.140 +    ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))"
   1.141 +      by blast
   1.142 +  qed
   1.143 +  then obtain b where b: "\<forall>i \<in> A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
   1.144      by blast
   1.145    let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
   1.146    show ?thesis