src/HOL/Old_Number_Theory/Chinese.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 32479 521cc9bf2958
child 38159 e9b4835a54ee
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
     1 (*  Author:     Thomas M. Rasmussen
     2     Copyright   2000  University of Cambridge
     3 *)
     4 
     5 header {* The Chinese Remainder Theorem *}
     6 
     7 theory Chinese 
     8 imports IntPrimes
     9 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" where
    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 definition
    41   km_cond :: "nat => (nat => int) => (nat => int) => bool" where
    42   "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i) (mf i) = 1)"
    43 
    44 definition
    45   lincong_sol ::
    46     "nat => (nat => int) => (nat => int) => (nat => int) => int => bool" where
    47   "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
    48 
    49 definition
    50   mhf :: "(nat => int) => nat => nat => int" where
    51   "mhf mf n i =
    52     (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
    53      else if i = n then funprod mf 0 (n - Suc 0)
    54      else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
    55 
    56 definition
    57   xilin_sol ::
    58     "nat => nat => (nat => int) => (nat => int) => (nat => int) => int" where
    59   "xilin_sol i n kf bf mf =
    60     (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
    61         (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
    62      else 0)"
    63 
    64 definition
    65   x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" where
    66   "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
    67 
    68 
    69 text {* \medskip @{term funprod} and @{term funsum} *}
    70 
    71 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
    72   apply (induct n)
    73    apply auto
    74   apply (simp add: zero_less_mult_iff)
    75   done
    76 
    77 lemma funprod_zgcd [rule_format (no_asm)]:
    78   "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i) (mf m) = 1) -->
    79     zgcd (funprod mf k l) (mf m) = 1"
    80   apply (induct l)
    81    apply simp_all
    82   apply (rule impI)+
    83   apply (subst zgcd_zmult_cancel)
    84   apply auto
    85   done
    86 
    87 lemma funprod_zdvd [rule_format]:
    88     "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
    89   apply (induct l)
    90    apply auto
    91   apply (subgoal_tac "i = Suc (k + l)")
    92    apply (simp_all (no_asm_simp))
    93   done
    94 
    95 lemma funsum_mod:
    96     "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
    97   apply (induct l)
    98    apply auto
    99   apply (rule trans)
   100    apply (rule mod_add_eq)
   101   apply simp
   102   apply (rule mod_add_right_eq [symmetric])
   103   done
   104 
   105 lemma funsum_zero [rule_format (no_asm)]:
   106     "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0"
   107   apply (induct l)
   108    apply auto
   109   done
   110 
   111 lemma funsum_oneelem [rule_format (no_asm)]:
   112   "k \<le> j --> j \<le> k + l -->
   113     (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) -->
   114     funsum f k l = f j"
   115   apply (induct l)
   116    prefer 2
   117    apply clarify
   118    defer
   119    apply clarify
   120    apply (subgoal_tac "k = j")
   121     apply (simp_all (no_asm_simp))
   122   apply (case_tac "Suc (k + l) = j")
   123    apply (subgoal_tac "funsum f k l = 0")
   124     apply (rule_tac [2] funsum_zero)
   125     apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
   126      apply (subgoal_tac [3] "j \<le> k + l")
   127       prefer 4
   128       apply arith
   129      apply auto
   130   done
   131 
   132 
   133 subsection {* Chinese: uniqueness *}
   134 
   135 lemma zcong_funprod_aux:
   136   "m_cond n mf ==> km_cond n kf mf
   137     ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
   138     ==> [x = y] (mod mf n)"
   139   apply (unfold m_cond_def km_cond_def lincong_sol_def)
   140   apply (rule iffD1)
   141    apply (rule_tac k = "kf n" in zcong_cancel2)
   142     apply (rule_tac [3] b = "bf n" in zcong_trans)
   143      prefer 4
   144      apply (subst zcong_sym)
   145      defer
   146      apply (rule order_less_imp_le)
   147      apply simp_all
   148   done
   149 
   150 lemma zcong_funprod [rule_format]:
   151   "m_cond n mf --> km_cond n kf mf -->
   152     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
   153     [x = y] (mod funprod mf 0 n)"
   154   apply (induct n)
   155    apply (simp_all (no_asm))
   156    apply (blast intro: zcong_funprod_aux)
   157   apply (rule impI)+
   158   apply (rule zcong_zgcd_zmult_zmod)
   159     apply (blast intro: zcong_funprod_aux)
   160     prefer 2
   161     apply (subst zgcd_commute)
   162     apply (rule funprod_zgcd)
   163    apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
   164   done
   165 
   166 
   167 subsection {* Chinese: existence *}
   168 
   169 lemma unique_xi_sol:
   170   "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
   171     ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
   172   apply (rule zcong_lineq_unique)
   173    apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
   174     apply (unfold m_cond_def km_cond_def mhf_def)
   175     apply (simp_all (no_asm_simp))
   176   apply safe
   177     apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
   178      apply (rule_tac [!] funprod_zgcd)
   179      apply safe
   180      apply simp_all
   181    apply (subgoal_tac "i<n")
   182     prefer 2
   183     apply arith
   184    apply (case_tac [2] i)
   185     apply simp_all
   186   done
   187 
   188 lemma x_sol_lin_aux:
   189     "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
   190   apply (unfold mhf_def)
   191   apply (case_tac "i = 0")
   192    apply (case_tac [2] "i = n")
   193     apply (simp_all (no_asm_simp))
   194     apply (case_tac [3] "j < i")
   195      apply (rule_tac [3] dvd_mult2)
   196      apply (rule_tac [4] dvd_mult)
   197      apply (rule_tac [!] funprod_zdvd)
   198      apply arith
   199      apply arith
   200      apply arith
   201      apply arith
   202      apply arith
   203      apply arith
   204      apply arith
   205      apply arith
   206   done
   207 
   208 lemma x_sol_lin:
   209   "0 < n ==> i \<le> n
   210     ==> x_sol n kf bf mf mod mf i =
   211       xilin_sol i n kf bf mf * mhf mf n i mod mf i"
   212   apply (unfold x_sol_def)
   213   apply (subst funsum_mod)
   214   apply (subst funsum_oneelem)
   215      apply auto
   216   apply (subst dvd_eq_mod_eq_0 [symmetric])
   217   apply (rule dvd_mult)
   218   apply (rule x_sol_lin_aux)
   219   apply auto
   220   done
   221 
   222 
   223 subsection {* Chinese *}
   224 
   225 lemma chinese_remainder:
   226   "0 < n ==> m_cond n mf ==> km_cond n kf mf
   227     ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
   228   apply safe
   229    apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
   230        apply (rule_tac [6] zcong_funprod)
   231           apply auto
   232   apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
   233   apply (unfold lincong_sol_def)
   234   apply safe
   235     apply (tactic {* stac (thm "zcong_zmod") 3 *})
   236     apply (tactic {* stac (thm "mod_mult_eq") 3 *})
   237     apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
   238       apply (tactic {* stac (thm "x_sol_lin") 4 *})
   239         apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
   240         apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
   241         apply (subgoal_tac [6]
   242           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   243           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
   244          prefer 6
   245          apply (simp add: zmult_ac)
   246         apply (unfold xilin_sol_def)
   247         apply (tactic {* asm_simp_tac @{simpset} 6 *})
   248         apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
   249         apply (rule_tac [6] unique_xi_sol)
   250            apply (rule_tac [3] funprod_zdvd)
   251             apply (unfold m_cond_def)
   252             apply (rule funprod_pos [THEN pos_mod_sign])
   253             apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
   254             apply auto
   255   done
   256 
   257 end