--- a/src/HOL/NumberTheory/Chinese.thy Sat Feb 03 17:43:34 2001 +0100
+++ b/src/HOL/NumberTheory/Chinese.thy Sun Feb 04 19:31:13 2001 +0100
@@ -1,55 +1,260 @@
-(* Title: Chinese.thy
+(* Title: HOL/NumberTheory/Chinese.thy
ID: $Id$
- Author: Thomas M. Rasmussen
- Copyright 2000 University of Cambridge
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
*)
-Chinese = IntPrimes +
+header {* The Chinese Remainder Theorem *}
+
+theory Chinese = IntPrimes:
+
+text {*
+ The Chinese Remainder Theorem for an arbitrary finite number of
+ equations. (The one-equation case is included in theory @{text
+ IntPrimes}. Uses functions for indexing.\footnote{Maybe @{term
+ funprod} and @{term funsum} should be based on general @{term fold}
+ on indices?}
+*}
+
+
+subsection {* Definitions *}
consts
- funprod :: (nat => int) => nat => nat => int
- funsum :: (nat => int) => nat => nat => int
+ funprod :: "(nat => int) => nat => nat => int"
+ funsum :: "(nat => int) => nat => nat => int"
primrec
- "funprod f i 0 = f i"
- "funprod f i (Suc n) = (f (Suc (i+n)))*(funprod f i n)"
+ "funprod f i 0 = f i"
+ "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
primrec
- "funsum f i 0 = f i"
- "funsum f i (Suc n) = (f (Suc (i+n)))+(funsum f i n)"
-
+ "funsum f i 0 = f i"
+ "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
consts
- m_cond :: [nat,nat => int] => bool
- km_cond :: [nat,nat => int,nat => int] => bool
- lincong_sol :: [nat,nat => int,nat => int,nat => int,int] => bool
+ m_cond :: "nat => (nat => int) => bool"
+ km_cond :: "nat => (nat => int) => (nat => int) => bool"
+ lincong_sol ::
+ "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
- mhf :: (nat => int) => nat => nat => int
- xilin_sol :: [nat,nat,nat => int,nat => int,nat => int] => int
- x_sol :: [nat,nat => int,nat => int,nat => int] => int
+ mhf :: "(nat => int) => nat => nat => int"
+ xilin_sol ::
+ "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
+ x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
defs
- m_cond_def "m_cond n mf ==
- (ALL i. i<=n --> #0 < mf i) &
- (ALL i j. i<=n & j<=n & i ~= j --> zgcd(mf i,mf j) = #1)"
+ m_cond_def:
+ "m_cond n mf ==
+ (\<forall>i. i \<le> n --> #0 < mf i) \<and>
+ (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = #1)"
+
+ km_cond_def:
+ "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = #1"
+
+ lincong_sol_def:
+ "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
+
+ mhf_def:
+ "mhf mf n i ==
+ if i = 0 then funprod mf 1 (n - 1)
+ else if i = n then funprod mf 0 (n - 1)
+ else funprod mf 0 (i - 1) * funprod mf (i + 1) (n - 1 - i)"
+
+ xilin_sol_def:
+ "xilin_sol i n kf bf mf ==
+ if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
+ (SOME x. #0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
+ else #0"
+
+ x_sol_def:
+ "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
+
+
+text {* \medskip @{term funprod} and @{term funsum} *}
+
+lemma funprod_pos: "(\<forall>i. i \<le> n --> #0 < mf i) ==> #0 < funprod mf 0 n"
+ apply (induct n)
+ apply auto
+ apply (simp add: int_0_less_mult_iff)
+ done
+
+lemma funprod_zgcd [rule_format (no_asm)]:
+ "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = #1) -->
+ zgcd (funprod mf k l, mf m) = #1"
+ apply (induct l)
+ apply simp_all
+ apply (rule impI)+
+ apply (subst zgcd_zmult_cancel)
+ apply auto
+ done
- km_cond_def "km_cond n kf mf == (ALL i. i<=n --> zgcd(kf i,mf i) = #1)"
+lemma funprod_zdvd [rule_format]:
+ "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
+ apply (induct l)
+ apply auto
+ apply (rule_tac [2] zdvd_zmult2)
+ apply (rule_tac [3] zdvd_zmult)
+ apply (subgoal_tac "i = k")
+ apply (subgoal_tac [3] "i = Suc (k + n)")
+ apply (simp_all (no_asm_simp))
+ done
+
+lemma funsum_mod:
+ "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
+ apply (induct l)
+ apply auto
+ apply (rule trans)
+ apply (rule zmod_zadd1_eq)
+ apply simp
+ apply (rule zmod_zadd_right_eq [symmetric])
+ done
- lincong_sol_def "lincong_sol n kf bf mf x ==
- (ALL i. i<=n --> zcong ((kf i)*x) (bf i) (mf i))"
+lemma funsum_zero [rule_format (no_asm)]:
+ "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = #0) --> (funsum f k l) = #0"
+ apply (induct l)
+ apply auto
+ done
+
+lemma funsum_oneelem [rule_format (no_asm)]:
+ "k \<le> j --> j \<le> k + l -->
+ (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = #0) -->
+ funsum f k l = f j"
+ apply (induct l)
+ prefer 2
+ apply clarify
+ defer
+ apply clarify
+ apply (subgoal_tac "k = j")
+ apply (simp_all (no_asm_simp))
+ apply (case_tac "Suc (k + n) = j")
+ apply (subgoal_tac "funsum f k n = #0")
+ apply (rule_tac [2] funsum_zero)
+ apply (subgoal_tac [3] "f (Suc (k + n)) = #0")
+ apply (subgoal_tac [3] "j \<le> k + n")
+ prefer 4
+ apply arith
+ apply auto
+ done
+
+
+subsection {* Chinese: uniqueness *}
- mhf_def "mhf mf n i == (if i=0 then (funprod mf 1 (n-1))
- else (if i=n then (funprod mf 0 (n-1))
- else ((funprod mf 0 (i-1)) *
- (funprod mf (i+1) (n-1-i)))))"
+lemma aux:
+ "m_cond n mf ==> km_cond n kf mf
+ ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
+ ==> [x = y] (mod mf n)"
+ apply (unfold m_cond_def km_cond_def lincong_sol_def)
+ apply (rule iffD1)
+ apply (rule_tac k = "kf n" in zcong_cancel2)
+ apply (rule_tac [3] b = "bf n" in zcong_trans)
+ prefer 4
+ apply (subst zcong_sym)
+ defer
+ apply (rule order_less_imp_le)
+ apply simp_all
+ done
+
+lemma zcong_funprod [rule_format]:
+ "m_cond n mf --> km_cond n kf mf -->
+ lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
+ [x = y] (mod funprod mf 0 n)"
+ apply (induct n)
+ apply (simp_all (no_asm))
+ apply (blast intro: aux)
+ apply (rule impI)+
+ apply (rule zcong_zgcd_zmult_zmod)
+ apply (blast intro: aux)
+ prefer 2
+ apply (subst zgcd_commute)
+ apply (rule funprod_zgcd)
+ apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
+ done
+
+
+subsection {* Chinese: existence *}
+
+lemma unique_xi_sol:
+ "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
+ ==> \<exists>!x. #0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
+ apply (rule zcong_lineq_unique)
+ apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
+ apply (unfold m_cond_def km_cond_def mhf_def)
+ apply (simp_all (no_asm_simp))
+ apply safe
+ apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
+ apply (rule_tac [!] funprod_zgcd)
+ apply safe
+ apply simp_all
+ apply (subgoal_tac [3] "ia \<le> n")
+ prefer 4
+ apply arith
+ apply (subgoal_tac "i<n")
+ prefer 2
+ apply arith
+ apply (case_tac [2] i)
+ apply simp_all
+ done
- xilin_sol_def "xilin_sol i n kf bf mf ==
- (if 0<n & i<=n & m_cond n mf & km_cond n kf mf then
- (@ x. #0<=x & x<(mf i) &
- zcong ((kf i)*(mhf mf n i)*x) (bf i) (mf i))
- else #0)"
+lemma aux:
+ "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
+ apply (unfold mhf_def)
+ apply (case_tac "i = 0")
+ apply (case_tac [2] "i = n")
+ apply (simp_all (no_asm_simp))
+ apply (case_tac [3] "j < i")
+ apply (rule_tac [3] zdvd_zmult2)
+ apply (rule_tac [4] zdvd_zmult)
+ apply (rule_tac [!] funprod_zdvd)
+ apply arith+
+ done
+
+lemma x_sol_lin:
+ "0 < n ==> i \<le> n
+ ==> x_sol n kf bf mf mod mf i =
+ xilin_sol i n kf bf mf * mhf mf n i mod mf i"
+ apply (unfold x_sol_def)
+ apply (subst funsum_mod)
+ apply (subst funsum_oneelem)
+ apply auto
+ apply (subst zdvd_iff_zmod_eq_0 [symmetric])
+ apply (rule zdvd_zmult)
+ apply (rule aux)
+ apply auto
+ done
+
+
+subsection {* Chinese *}
- x_sol_def "x_sol n kf bf mf ==
- (funsum (%i. (xilin_sol i n kf bf mf)*(mhf mf n i)) 0 n)"
+lemma chinese_remainder:
+ "0 < n ==> m_cond n mf ==> km_cond n kf mf
+ ==> \<exists>!x. #0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
+ apply safe
+ apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
+ apply (rule_tac [6] zcong_funprod)
+ apply auto
+ apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
+ apply (unfold lincong_sol_def)
+ apply safe
+ apply (tactic {* stac (thm "zcong_zmod") 3 *})
+ apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
+ apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
+ apply (tactic {* stac (thm "x_sol_lin") 5 *})
+ apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
+ apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
+ apply (subgoal_tac [7]
+ "#0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
+ \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
+ prefer 7
+ apply (simp add: zmult_ac)
+ apply (unfold xilin_sol_def)
+ apply (tactic {* Asm_simp_tac 7 *})
+ apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
+ apply (rule_tac [7] unique_xi_sol)
+ apply (rule_tac [4] funprod_zdvd)
+ apply (unfold m_cond_def)
+ apply (rule funprod_pos [THEN pos_mod_sign])
+ apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
+ apply auto
+ done
end