section ‹The Chinese Remainder Theorem›
theory Chinese
imports IntPrimes
begin
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›
primrec funprod :: "(nat => int) => nat => nat => int"
where
"funprod f i 0 = f i"
| "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
primrec funsum :: "(nat => int) => nat => nat => int"
where
"funsum f i 0 = f i"
| "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
definition
m_cond :: "nat => (nat => int) => bool" where
"m_cond n mf =
((∀i. i ≤ n --> 0 < mf i) ∧
(∀i j. i ≤ n ∧ j ≤ n ∧ i ≠ j --> zgcd (mf i) (mf j) = 1))"
definition
km_cond :: "nat => (nat => int) => (nat => int) => bool" where
"km_cond n kf mf = (∀i. i ≤ n --> zgcd (kf i) (mf i) = 1)"
definition
lincong_sol ::
"nat => (nat => int) => (nat => int) => (nat => int) => int => bool" where
"lincong_sol n kf bf mf x = (∀i. i ≤ n --> zcong (kf i * x) (bf i) (mf i))"
definition
mhf :: "(nat => int) => nat => nat => int" where
"mhf mf n i =
(if i = 0 then funprod mf (Suc 0) (n - Suc 0)
else if i = n then funprod mf 0 (n - Suc 0)
else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
definition
xilin_sol ::
"nat => nat => (nat => int) => (nat => int) => (nat => int) => int" where
"xilin_sol i n kf bf mf =
(if 0 < n ∧ i ≤ n ∧ m_cond n mf ∧ km_cond n kf mf then
(SOME x. 0 ≤ x ∧ x < mf i ∧ zcong (kf i * mhf mf n i * x) (bf i) (mf i))
else 0)"
definition
x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" where
"x_sol n kf bf mf = funsum (λi. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
text ‹\medskip @{term funprod} and @{term funsum}›
lemma funprod_pos: "(∀i. i ≤ n --> 0 < mf i) ==> 0 < funprod mf 0 n"
by (induct n) auto
lemma funprod_zgcd [rule_format (no_asm)]:
"(∀i. k ≤ i ∧ i ≤ 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
lemma funprod_zdvd [rule_format]:
"k ≤ i --> i ≤ k + l --> mf i dvd funprod mf k l"
apply (induct l)
apply auto
apply (subgoal_tac "i = Suc (k + l)")
apply (simp_all (no_asm_simp))
done
lemma funsum_mod:
"funsum f k l mod m = funsum (λi. (f i) mod m) k l mod m"
apply (induct l)
apply auto
apply (rule trans)
apply (rule mod_add_eq)
apply simp
apply (rule mod_add_right_eq [symmetric])
done
lemma funsum_zero [rule_format (no_asm)]:
"(∀i. k ≤ i ∧ i ≤ k + l --> f i = 0) --> (funsum f k l) = 0"
apply (induct l)
apply auto
done
lemma funsum_oneelem [rule_format (no_asm)]:
"k ≤ j --> j ≤ k + l -->
(∀i. k ≤ i ∧ i ≤ k + l ∧ i ≠ 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 + l) = j")
apply (subgoal_tac "funsum f k l = 0")
apply (rule_tac [2] funsum_zero)
apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
apply (subgoal_tac [3] "j ≤ k + l")
prefer 4
apply arith
apply auto
done
subsection ‹Chinese: uniqueness›
lemma zcong_funprod_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: zcong_funprod_aux)
apply (rule impI)+
apply (rule zcong_zgcd_zmult_zmod)
apply (blast intro: zcong_funprod_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 ≤ n ==> m_cond n mf ==> km_cond n kf mf
==> ∃!x. 0 ≤ x ∧ x < mf i ∧ [kf i * mhf mf n i * x = bf i] (mod mf i)"
apply (rule zcong_lineq_unique)
apply (tactic ‹stac @{context} @{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 @{context} @{thm zgcd_zmult_cancel} 3›)
apply (rule_tac [!] funprod_zgcd)
apply safe
apply simp_all
apply (subgoal_tac "ia<n")
prefer 2
apply arith
apply (case_tac [2] i)
apply simp_all
done
lemma x_sol_lin_aux:
"0 < n ==> i ≤ n ==> j ≤ n ==> j ≠ 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] dvd_mult2)
apply (rule_tac [4] dvd_mult)
apply (rule_tac [!] funprod_zdvd)
apply arith
apply arith
apply arith
apply arith
apply arith
apply arith
apply arith
apply arith
done
lemma x_sol_lin:
"0 < n ==> i ≤ 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 dvd_eq_mod_eq_0 [symmetric])
apply (rule dvd_mult)
apply (rule x_sol_lin_aux)
apply auto
done
subsection ‹Chinese›
lemma chinese_remainder:
"0 < n ==> m_cond n mf ==> km_cond n kf mf
==> ∃!x. 0 ≤ x ∧ x < funprod mf 0 n ∧ 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 @{context} @{thm zcong_zmod} 3›)
apply (tactic ‹stac @{context} @{thm mod_mult_eq} 3›)
apply (tactic ‹stac @{context} @{thm mod_mod_cancel} 3›)
apply (tactic ‹stac @{context} @{thm x_sol_lin} 4›)
apply (tactic ‹stac @{context} (@{thm mod_mult_eq} RS sym) 6›)
apply (tactic ‹stac @{context} (@{thm zcong_zmod} RS sym) 6›)
apply (subgoal_tac [6]
"0 ≤ xilin_sol i n kf bf mf ∧ xilin_sol i n kf bf mf < mf i
∧ [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
prefer 6
apply (simp add: ac_simps)
apply (unfold xilin_sol_def)
apply (tactic ‹asm_simp_tac @{context} 6›)
apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
apply (rule_tac [6] unique_xi_sol)
apply (rule_tac [3] 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