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