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