src/HOL/Old_Number_Theory/Chinese.thy

-(*  Title:      HOL/Old_Number_Theory/Chinese.thy
-    Author:     Thomas M. Rasmussen
-    Copyright   2000  University of Cambridge
-*)
-
-section \<open>The Chinese Remainder Theorem\<close>
-
-theory Chinese 
-imports IntPrimes
-begin
-
-text \<open>
-  The Chinese Remainder Theorem for an arbitrary finite number of
-  equations.  (The one-equation case is included in theory \<open>IntPrimes\<close>.  Uses functions for indexing.\footnote{Maybe @{term
-  funprod} and @{term funsum} should be based on general @{term fold}
-  on indices?}
-\<close>
-
-
-subsection \<open>Definitions\<close>
-
-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 =
-    ((\<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))"
-
-definition
-  km_cond :: "nat => (nat => int) => (nat => int) => bool" where
-  "km_cond n kf mf = (\<forall>i. i \<le> 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 = (\<forall>i. i \<le> 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 \<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)"
-
-definition
-  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" where
-  "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
-
-
-text \<open>\medskip @{term funprod} and @{term funsum}\<close>
-
-lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
-by (induct n) auto
-
-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
-
-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 (subgoal_tac "i = Suc (k + l)")
-   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 mod_add_eq)
-  apply simp
-  apply (rule mod_add_right_eq [symmetric])
-  done
-
-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 + 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 \<le> k + l")
-      prefer 4
-      apply arith
-     apply auto
-  done
-
-
-subsection \<open>Chinese: uniqueness\<close>
-
-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 \<open>Chinese: existence\<close>
-
-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 \<open>stac @{context} @{thm zgcd_zmult_cancel} 2\<close>)
-    apply (unfold m_cond_def km_cond_def mhf_def)
-    apply (simp_all (no_asm_simp))
-  apply safe
-    apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 3\<close>)
-     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 \<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] 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 \<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 dvd_eq_mod_eq_0 [symmetric])
-  apply (rule dvd_mult)
-  apply (rule x_sol_lin_aux)
-  apply auto
-  done
-
-
-subsection \<open>Chinese\<close>
-
-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 \<open>stac @{context} @{thm zcong_zmod} 3\<close>)
-    apply (tactic \<open>stac @{context} @{thm mod_mult_eq} 3\<close>)
-    apply (tactic \<open>stac @{context} @{thm mod_mod_cancel} 3\<close>)
-      apply (tactic \<open>stac @{context} @{thm x_sol_lin} 4\<close>)
-        apply (tactic \<open>stac @{context} (@{thm mod_mult_eq} RS sym) 6\<close>)
-        apply (tactic \<open>stac @{context} (@{thm zcong_zmod} RS sym) 6\<close>)
-        apply (subgoal_tac [6]
-          "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 6
-         apply (simp add: ac_simps)
-        apply (unfold xilin_sol_def)
-        apply (tactic \<open>asm_simp_tac @{context} 6\<close>)
-        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