src/HOL/Old_Number_Theory/Chinese.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Old_Number_Theory/Chinese.thy
     2     Author:     Thomas M. Rasmussen
     3     Copyright   2000  University of Cambridge
     4 *)
     5 
     6 section \<open>The Chinese Remainder Theorem\<close>
     7 
     8 theory Chinese 
     9 imports IntPrimes
    10 begin
    11 
    12 text \<open>
    13   The Chinese Remainder Theorem for an arbitrary finite number of
    14   equations.  (The one-equation case is included in theory \<open>IntPrimes\<close>.  Uses functions for indexing.\footnote{Maybe @{term
    15   funprod} and @{term funsum} should be based on general @{term fold}
    16   on indices?}
    17 \<close>
    18 
    19 
    20 subsection \<open>Definitions\<close>
    21 
    22 primrec funprod :: "(nat => int) => nat => nat => int"
    23 where
    24   "funprod f i 0 = f i"
    25 | "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
    26 
    27 primrec funsum :: "(nat => int) => nat => nat => int"
    28 where
    29   "funsum f i 0 = f i"
    30 | "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
    31 
    32 definition
    33   m_cond :: "nat => (nat => int) => bool" where
    34   "m_cond n mf =
    35     ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
    36       (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i) (mf j) = 1))"
    37 
    38 definition
    39   km_cond :: "nat => (nat => int) => (nat => int) => bool" where
    40   "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i) (mf i) = 1)"
    41 
    42 definition
    43   lincong_sol ::
    44     "nat => (nat => int) => (nat => int) => (nat => int) => int => bool" where
    45   "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
    46 
    47 definition
    48   mhf :: "(nat => int) => nat => nat => int" where
    49   "mhf mf n i =
    50     (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
    51      else if i = n then funprod mf 0 (n - Suc 0)
    52      else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
    53 
    54 definition
    55   xilin_sol ::
    56     "nat => nat => (nat => int) => (nat => int) => (nat => int) => int" where
    57   "xilin_sol i n kf bf mf =
    58     (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    59         (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    60      else 0)"
    61 
    62 definition
    63   x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" where
    64   "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    65 
    66 
    67 text \<open>\medskip @{term funprod} and @{term funsum}\<close>
    68 
    69 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
    70 by (induct n) auto
    71 
    72 lemma funprod_zgcd [rule_format (no_asm)]:
    73   "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i) (mf m) = 1) -->
    74     zgcd (funprod mf k l) (mf m) = 1"
    75   apply (induct l)
    76    apply simp_all
    77   apply (rule impI)+
    78   apply (subst zgcd_zmult_cancel)
    79   apply auto
    80   done
    81 
    82 lemma funprod_zdvd [rule_format]:
    83     "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
    84   apply (induct l)
    85    apply auto
    86   apply (subgoal_tac "i = Suc (k + l)")
    87    apply (simp_all (no_asm_simp))
    88   done
    89 
    90 lemma funsum_mod:
    91     "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
    92   apply (induct l)
    93    apply auto
    94   apply (rule trans)
    95    apply (rule mod_add_eq)
    96   apply simp
    97   apply (rule mod_add_right_eq [symmetric])
    98   done
    99 
   100 lemma funsum_zero [rule_format (no_asm)]:
   101     "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0"
   102   apply (induct l)
   103    apply auto
   104   done
   105 
   106 lemma funsum_oneelem [rule_format (no_asm)]:
   107   "k \<le> j --> j \<le> k + l -->
   108     (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) -->
   109     funsum f k l = f j"
   110   apply (induct l)
   111    prefer 2
   112    apply clarify
   113    defer
   114    apply clarify
   115    apply (subgoal_tac "k = j")
   116     apply (simp_all (no_asm_simp))
   117   apply (case_tac "Suc (k + l) = j")
   118    apply (subgoal_tac "funsum f k l = 0")
   119     apply (rule_tac [2] funsum_zero)
   120     apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
   121      apply (subgoal_tac [3] "j \<le> k + l")
   122       prefer 4
   123       apply arith
   124      apply auto
   125   done
   126 
   127 
   128 subsection \<open>Chinese: uniqueness\<close>
   129 
   130 lemma zcong_funprod_aux:
   131   "m_cond n mf ==> km_cond n kf mf
   132     ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
   133     ==> [x = y] (mod mf n)"
   134   apply (unfold m_cond_def km_cond_def lincong_sol_def)
   135   apply (rule iffD1)
   136    apply (rule_tac k = "kf n" in zcong_cancel2)
   137     apply (rule_tac [3] b = "bf n" in zcong_trans)
   138      prefer 4
   139      apply (subst zcong_sym)
   140      defer
   141      apply (rule order_less_imp_le)
   142      apply simp_all
   143   done
   144 
   145 lemma zcong_funprod [rule_format]:
   146   "m_cond n mf --> km_cond n kf mf -->
   147     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
   148     [x = y] (mod funprod mf 0 n)"
   149   apply (induct n)
   150    apply (simp_all (no_asm))
   151    apply (blast intro: zcong_funprod_aux)
   152   apply (rule impI)+
   153   apply (rule zcong_zgcd_zmult_zmod)
   154     apply (blast intro: zcong_funprod_aux)
   155     prefer 2
   156     apply (subst zgcd_commute)
   157     apply (rule funprod_zgcd)
   158    apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
   159   done
   160 
   161 
   162 subsection \<open>Chinese: existence\<close>
   163 
   164 lemma unique_xi_sol:
   165   "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
   166     ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
   167   apply (rule zcong_lineq_unique)
   168    apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 2\<close>)
   169     apply (unfold m_cond_def km_cond_def mhf_def)
   170     apply (simp_all (no_asm_simp))
   171   apply safe
   172     apply (tactic \<open>stac @{context} @{thm zgcd_zmult_cancel} 3\<close>)
   173      apply (rule_tac [!] funprod_zgcd)
   174      apply safe
   175      apply simp_all
   176    apply (subgoal_tac "ia<n")
   177     prefer 2
   178     apply arith
   179    apply (case_tac [2] i)
   180     apply simp_all
   181   done
   182 
   183 lemma x_sol_lin_aux:
   184     "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
   185   apply (unfold mhf_def)
   186   apply (case_tac "i = 0")
   187    apply (case_tac [2] "i = n")
   188     apply (simp_all (no_asm_simp))
   189     apply (case_tac [3] "j < i")
   190      apply (rule_tac [3] dvd_mult2)
   191      apply (rule_tac [4] dvd_mult)
   192      apply (rule_tac [!] funprod_zdvd)
   193      apply arith
   194      apply arith
   195      apply arith
   196      apply arith
   197      apply arith
   198      apply arith
   199      apply arith
   200      apply arith
   201   done
   202 
   203 lemma x_sol_lin:
   204   "0 < n ==> i \<le> n
   205     ==> x_sol n kf bf mf mod mf i =
   206       xilin_sol i n kf bf mf * mhf mf n i mod mf i"
   207   apply (unfold x_sol_def)
   208   apply (subst funsum_mod)
   209   apply (subst funsum_oneelem)
   210      apply auto
   211   apply (subst dvd_eq_mod_eq_0 [symmetric])
   212   apply (rule dvd_mult)
   213   apply (rule x_sol_lin_aux)
   214   apply auto
   215   done
   216 
   217 
   218 subsection \<open>Chinese\<close>
   219 
   220 lemma chinese_remainder:
   221   "0 < n ==> m_cond n mf ==> km_cond n kf mf
   222     ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
   223   apply safe
   224    apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
   225        apply (rule_tac [6] zcong_funprod)
   226           apply auto
   227   apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
   228   apply (unfold lincong_sol_def)
   229   apply safe
   230     apply (tactic \<open>stac @{context} @{thm zcong_zmod} 3\<close>)
   231     apply (tactic \<open>stac @{context} @{thm mod_mult_eq} 3\<close>)
   232     apply (tactic \<open>stac @{context} @{thm mod_mod_cancel} 3\<close>)
   233       apply (tactic \<open>stac @{context} @{thm x_sol_lin} 4\<close>)
   234         apply (tactic \<open>stac @{context} (@{thm mod_mult_eq} RS sym) 6\<close>)
   235         apply (tactic \<open>stac @{context} (@{thm zcong_zmod} RS sym) 6\<close>)
   236         apply (subgoal_tac [6]
   237           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   238           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
   239          prefer 6
   240          apply (simp add: ac_simps)
   241         apply (unfold xilin_sol_def)
   242         apply (tactic \<open>asm_simp_tac @{context} 6\<close>)
   243         apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
   244         apply (rule_tac [6] unique_xi_sol)
   245            apply (rule_tac [3] funprod_zdvd)
   246             apply (unfold m_cond_def)
   247             apply (rule funprod_pos [THEN pos_mod_sign])
   248             apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
   249             apply auto
   250   done
   251 
   252 end