src/HOL/NumberTheory/Chinese.thy
author webertj
Wed Aug 30 03:19:08 2006 +0200 (2006-08-30)
changeset 20432 07ec57376051
parent 20272 0ca998e83447
child 21404 eb85850d3eb7
permissions -rw-r--r--
lin_arith_prover: splitting reverted because of performance loss
     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 imports IntPrimes begin
    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 definition
    35   m_cond :: "nat => (nat => int) => bool"
    36   "m_cond n mf =
    37     ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
    38       (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
    39 
    40   km_cond :: "nat => (nat => int) => (nat => int) => bool"
    41   "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
    42 
    43   lincong_sol ::
    44     "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
    45   "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
    46 
    47   mhf :: "(nat => int) => nat => nat => int"
    48   "mhf mf n i =
    49     (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
    50      else if i = n then funprod mf 0 (n - Suc 0)
    51      else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
    52 
    53   xilin_sol ::
    54     "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
    55   "xilin_sol i n kf bf mf =
    56     (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    57         (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    58      else 0)"
    59 
    60   x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
    61   "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    62 
    63 
    64 text {* \medskip @{term funprod} and @{term funsum} *}
    65 
    66 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
    67   apply (induct n)
    68    apply auto
    69   apply (simp add: zero_less_mult_iff)
    70   done
    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 (rule_tac [1] zdvd_zmult2)
    87     apply (rule_tac [2] zdvd_zmult)
    88     apply (subgoal_tac "i = Suc (k + l)")
    89     apply (simp_all (no_asm_simp))
    90   done
    91 
    92 lemma funsum_mod:
    93     "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
    94   apply (induct l)
    95    apply auto
    96   apply (rule trans)
    97    apply (rule zmod_zadd1_eq)
    98   apply simp
    99   apply (rule zmod_zadd_right_eq [symmetric])
   100   done
   101 
   102 lemma funsum_zero [rule_format (no_asm)]:
   103     "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0"
   104   apply (induct l)
   105    apply auto
   106   done
   107 
   108 lemma funsum_oneelem [rule_format (no_asm)]:
   109   "k \<le> j --> j \<le> k + l -->
   110     (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) -->
   111     funsum f k l = f j"
   112   apply (induct l)
   113    prefer 2
   114    apply clarify
   115    defer
   116    apply clarify
   117    apply (subgoal_tac "k = j")
   118     apply (simp_all (no_asm_simp))
   119   apply (case_tac "Suc (k + l) = j")
   120    apply (subgoal_tac "funsum f k l = 0")
   121     apply (rule_tac [2] funsum_zero)
   122     apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
   123      apply (subgoal_tac [3] "j \<le> k + l")
   124       prefer 4
   125       apply arith
   126      apply auto
   127   done
   128 
   129 
   130 subsection {* Chinese: uniqueness *}
   131 
   132 lemma zcong_funprod_aux:
   133   "m_cond n mf ==> km_cond n kf mf
   134     ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
   135     ==> [x = y] (mod mf n)"
   136   apply (unfold m_cond_def km_cond_def lincong_sol_def)
   137   apply (rule iffD1)
   138    apply (rule_tac k = "kf n" in zcong_cancel2)
   139     apply (rule_tac [3] b = "bf n" in zcong_trans)
   140      prefer 4
   141      apply (subst zcong_sym)
   142      defer
   143      apply (rule order_less_imp_le)
   144      apply simp_all
   145   done
   146 
   147 lemma zcong_funprod [rule_format]:
   148   "m_cond n mf --> km_cond n kf mf -->
   149     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
   150     [x = y] (mod funprod mf 0 n)"
   151   apply (induct n)
   152    apply (simp_all (no_asm))
   153    apply (blast intro: zcong_funprod_aux)
   154   apply (rule impI)+
   155   apply (rule zcong_zgcd_zmult_zmod)
   156     apply (blast intro: zcong_funprod_aux)
   157     prefer 2
   158     apply (subst zgcd_commute)
   159     apply (rule funprod_zgcd)
   160    apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
   161   done
   162 
   163 
   164 subsection {* Chinese: existence *}
   165 
   166 lemma unique_xi_sol:
   167   "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
   168     ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
   169   apply (rule zcong_lineq_unique)
   170    apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
   171     apply (unfold m_cond_def km_cond_def mhf_def)
   172     apply (simp_all (no_asm_simp))
   173   apply safe
   174     apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
   175      apply (rule_tac [!] funprod_zgcd)
   176      apply safe
   177      apply simp_all
   178    apply (subgoal_tac "i<n")
   179     prefer 2
   180     apply arith
   181    apply (case_tac [2] i)
   182     apply simp_all
   183   done
   184 
   185 lemma x_sol_lin_aux:
   186     "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
   187   apply (unfold mhf_def)
   188   apply (case_tac "i = 0")
   189    apply (case_tac [2] "i = n")
   190     apply (simp_all (no_asm_simp))
   191     apply (case_tac [3] "j < i")
   192      apply (rule_tac [3] zdvd_zmult2)
   193      apply (rule_tac [4] zdvd_zmult)
   194      apply (rule_tac [!] funprod_zdvd)
   195           apply arith+
   196   done
   197 
   198 lemma x_sol_lin:
   199   "0 < n ==> i \<le> n
   200     ==> x_sol n kf bf mf mod mf i =
   201       xilin_sol i n kf bf mf * mhf mf n i mod mf i"
   202   apply (unfold x_sol_def)
   203   apply (subst funsum_mod)
   204   apply (subst funsum_oneelem)
   205      apply auto
   206   apply (subst zdvd_iff_zmod_eq_0 [symmetric])
   207   apply (rule zdvd_zmult)
   208   apply (rule x_sol_lin_aux)
   209   apply auto
   210   done
   211 
   212 
   213 subsection {* Chinese *}
   214 
   215 lemma chinese_remainder:
   216   "0 < n ==> m_cond n mf ==> km_cond n kf mf
   217     ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
   218   apply safe
   219    apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
   220        apply (rule_tac [6] zcong_funprod)
   221           apply auto
   222   apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
   223   apply (unfold lincong_sol_def)
   224   apply safe
   225     apply (tactic {* stac (thm "zcong_zmod") 3 *})
   226     apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
   227     apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
   228       apply (tactic {* stac (thm "x_sol_lin") 5 *})
   229         apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
   230         apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
   231         apply (subgoal_tac [7]
   232           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   233           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
   234          prefer 7
   235          apply (simp add: zmult_ac)
   236         apply (unfold xilin_sol_def)
   237         apply (tactic {* Asm_simp_tac 7 *})
   238         apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
   239         apply (rule_tac [7] unique_xi_sol)
   240            apply (rule_tac [4] funprod_zdvd)
   241             apply (unfold m_cond_def)
   242             apply (rule funprod_pos [THEN pos_mod_sign])
   243             apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
   244             apply auto
   245   done
   246 
   247 end