summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Thu, 23 Nov 2017 17:03:26 +0000 | |

changeset 67086 | 59d07a95be0e |

parent 67085 | f5d7f37b4143 |

child 67087 | 733017b19de9 |

tuned

--- a/src/HOL/Number_Theory/Cong.thy Thu Nov 23 17:03:21 2017 +0000 +++ b/src/HOL/Number_Theory/Cong.thy Thu Nov 23 17:03:26 2017 +0000 @@ -558,50 +558,27 @@ apply (metis coprime_cong_mult_int prod_coprime_right) done -lemma binary_chinese_remainder_aux_nat: - fixes m1 m2 :: nat - assumes a: "coprime m1 m2" - shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" -proof - - from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" - by auto - from a have b: "coprime m2 m1" - by (simp add: ac_simps) - from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" - by auto - have "[m1 * x1 = 0] (mod m1)" - by (simp add: cong_mult_self_left) - moreover have "[m2 * x2 = 0] (mod m2)" - by (simp add: cong_mult_self_left) - ultimately show ?thesis - using 1 2 by blast -qed - -lemma binary_chinese_remainder_aux_int: - fixes m1 m2 :: int - assumes a: "coprime m1 m2" - shows "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" -proof - - from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" - by auto - from a have b: "coprime m2 m1" - by (simp add: ac_simps) - from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" - by auto - have "[m1 * x1 = 0] (mod m1)" - by (simp add: cong_mult_self_left) - moreover have "[m2 * x2 = 0] (mod m2)" - by (simp add: cong_mult_self_left) - ultimately show ?thesis - using 1 2 by blast -qed - lemma binary_chinese_remainder_nat: fixes m1 m2 :: nat assumes a: "coprime m1 m2" shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" proof - - from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2 + have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" + proof - + from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" + by auto + from a have b: "coprime m2 m1" + by (simp add: ac_simps) + from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" + by auto + have "[m1 * x1 = 0] (mod m1)" + by (simp add: cong_mult_self_left) + moreover have "[m2 * x2 = 0] (mod m2)" + by (simp add: cong_mult_self_left) + ultimately show ?thesis + using 1 2 by blast + qed + then obtain b1 b2 where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" by blast @@ -622,7 +599,22 @@ assumes a: "coprime m1 m2" shows "\<exists>x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)" proof - - from binary_chinese_remainder_aux_int [OF a] obtain b1 b2 + have "\<exists>b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and> [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)" + proof - + from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)" + by auto + from a have b: "coprime m2 m1" + by (simp add: ac_simps) + from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)" + by auto + have "[m1 * x1 = 0] (mod m1)" + by (simp add: cong_mult_self_left) + moreover have "[m2 * x2 = 0] (mod m2)" + by (simp add: cong_mult_self_left) + ultimately show ?thesis + using 1 2 by blast + qed + then obtain b1 b2 where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)" by blast @@ -706,27 +698,6 @@ with less 1 2 show ?thesis by auto qed -lemma chinese_remainder_aux_nat: - fixes A :: "'a set" - and m :: "'a \<Rightarrow> nat" - assumes fin: "finite A" - and cop: "\<forall>i \<in> A. (\<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))" - 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)))" -proof (rule finite_set_choice, rule fin, rule ballI) - fix i - assume "i \<in> A" - with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)" - by (intro prod_coprime_left) auto - then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)" - by (elim cong_solve_coprime_nat) - then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)" - by auto - moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))" - by (simp add: cong_0_iff) - ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))" - by blast -qed - lemma chinese_remainder_nat: fixes A :: "'a set" and m :: "'a \<Rightarrow> nat" @@ -735,8 +706,22 @@ and cop: "\<forall>i \<in> A. \<forall>j \<in> A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)" shows "\<exists>x. \<forall>i \<in> A. [x = u i] (mod m i)" proof - - from chinese_remainder_aux_nat [OF fin cop] - 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))" + 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)))" + proof (rule finite_set_choice, rule fin, rule ballI) + fix i + assume "i \<in> A" + with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)" + by (intro prod_coprime_left) auto + then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)" + by (elim cong_solve_coprime_nat) + then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)" + by auto + moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0] (mod (\<Prod>j \<in> A - {i}. m j))" + by (simp add: cong_0_iff) + ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] (mod prod m (A - {i}))" + by blast + qed + 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))" by blast let ?x = "\<Sum>i\<in>A. (u i) * (b i)" show ?thesis