author haftmann Thu Nov 23 17:03:26 2017 +0000 (17 months ago) changeset 67086 59d07a95be0e parent 67085 f5d7f37b4143 child 67087 733017b19de9
tuned
```     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
```