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