src/HOL/Number_Theory/Cong.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58860 fee7cfa69c50
child 58937 49e8115f70d8
permissions -rw-r--r--
modernized header uniformly as section;
wenzelm@41959
     1
(*  Title:      HOL/Number_Theory/Cong.thy
nipkow@31719
     2
    Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
nipkow@31719
     3
                Thomas M. Rasmussen, Jeremy Avigad
nipkow@31719
     4
nipkow@31719
     5
Defines congruence (notation: [x = y] (mod z)) for natural numbers and
nipkow@31719
     6
integers.
nipkow@31719
     7
nipkow@31719
     8
This file combines and revises a number of prior developments.
nipkow@31719
     9
nipkow@31719
    10
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
wenzelm@58623
    11
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
nipkow@31719
    12
gcd, lcm, and prime for the natural numbers.
nipkow@31719
    13
nipkow@31719
    14
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
nipkow@31719
    15
extended gcd, lcm, primes to the integers. Amine Chaieb provided
nipkow@31719
    16
another extension of the notions to the integers, and added a number
wenzelm@44872
    17
of results to "Primes" and "GCD".
nipkow@31719
    18
nipkow@31719
    19
The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
nipkow@31719
    20
developed the congruence relations on the integers. The notion was
webertj@33718
    21
extended to the natural numbers by Chaieb. Jeremy Avigad combined
nipkow@31719
    22
these, revised and tidied them, made the development uniform for the
nipkow@31719
    23
natural numbers and the integers, and added a number of new theorems.
nipkow@31719
    24
*)
nipkow@31719
    25
wenzelm@58889
    26
section {* Congruence *}
nipkow@31719
    27
nipkow@31719
    28
theory Cong
haftmann@37293
    29
imports Primes
nipkow@31719
    30
begin
nipkow@31719
    31
wenzelm@44872
    32
subsection {* Turn off @{text One_nat_def} *}
nipkow@31719
    33
wenzelm@44872
    34
lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)"
wenzelm@44872
    35
  by (induct m) auto
nipkow@31719
    36
nipkow@31719
    37
declare mod_pos_pos_trivial [simp]
nipkow@31719
    38
nipkow@31719
    39
nipkow@31719
    40
subsection {* Main definitions *}
nipkow@31719
    41
nipkow@31719
    42
class cong =
wenzelm@44872
    43
  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
nipkow@31719
    44
begin
nipkow@31719
    45
wenzelm@44872
    46
abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(mod _'))")
wenzelm@44872
    47
  where "notcong x y m \<equiv> \<not> cong x y m"
nipkow@31719
    48
nipkow@31719
    49
end
nipkow@31719
    50
nipkow@31719
    51
(* definitions for the natural numbers *)
nipkow@31719
    52
nipkow@31719
    53
instantiation nat :: cong
wenzelm@44872
    54
begin
nipkow@31719
    55
wenzelm@44872
    56
definition cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
wenzelm@44872
    57
  where "cong_nat x y m = ((x mod m) = (y mod m))"
nipkow@31719
    58
wenzelm@44872
    59
instance ..
nipkow@31719
    60
nipkow@31719
    61
end
nipkow@31719
    62
nipkow@31719
    63
nipkow@31719
    64
(* definitions for the integers *)
nipkow@31719
    65
nipkow@31719
    66
instantiation int :: cong
wenzelm@44872
    67
begin
nipkow@31719
    68
wenzelm@44872
    69
definition cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
wenzelm@44872
    70
  where "cong_int x y m = ((x mod m) = (y mod m))"
nipkow@31719
    71
wenzelm@44872
    72
instance ..
nipkow@31719
    73
nipkow@31719
    74
end
nipkow@31719
    75
nipkow@31719
    76
nipkow@31719
    77
subsection {* Set up Transfer *}
nipkow@31719
    78
nipkow@31719
    79
nipkow@31719
    80
lemma transfer_nat_int_cong:
wenzelm@44872
    81
  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow>
nipkow@31719
    82
    ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
wenzelm@44872
    83
  unfolding cong_int_def cong_nat_def
lp15@55130
    84
  by (metis Divides.transfer_int_nat_functions(2) nat_0_le nat_mod_distrib)
lp15@55130
    85
nipkow@31719
    86
wenzelm@44872
    87
declare transfer_morphism_nat_int[transfer add return:
nipkow@31719
    88
    transfer_nat_int_cong]
nipkow@31719
    89
nipkow@31719
    90
lemma transfer_int_nat_cong:
nipkow@31719
    91
  "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
nipkow@31719
    92
  apply (auto simp add: cong_int_def cong_nat_def)
nipkow@31719
    93
  apply (auto simp add: zmod_int [symmetric])
wenzelm@44872
    94
  done
nipkow@31719
    95
wenzelm@44872
    96
declare transfer_morphism_int_nat[transfer add return:
nipkow@31719
    97
    transfer_int_nat_cong]
nipkow@31719
    98
nipkow@31719
    99
nipkow@31719
   100
subsection {* Congruence *}
nipkow@31719
   101
nipkow@31719
   102
(* was zcong_0, etc. *)
nipkow@31952
   103
lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
wenzelm@44872
   104
  unfolding cong_nat_def by auto
nipkow@31719
   105
nipkow@31952
   106
lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
wenzelm@44872
   107
  unfolding cong_int_def by auto
nipkow@31719
   108
nipkow@31952
   109
lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
wenzelm@44872
   110
  unfolding cong_nat_def by auto
nipkow@31719
   111
nipkow@31952
   112
lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
lp15@55130
   113
  unfolding cong_nat_def by auto
nipkow@31719
   114
nipkow@31952
   115
lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
wenzelm@44872
   116
  unfolding cong_int_def by auto
nipkow@31719
   117
nipkow@31952
   118
lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
wenzelm@44872
   119
  unfolding cong_nat_def by auto
nipkow@31719
   120
nipkow@31952
   121
lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
wenzelm@44872
   122
  unfolding cong_int_def by auto
nipkow@31719
   123
nipkow@31952
   124
lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
wenzelm@44872
   125
  unfolding cong_nat_def by auto
nipkow@31719
   126
nipkow@31952
   127
lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
wenzelm@44872
   128
  unfolding cong_int_def by auto
nipkow@31719
   129
nipkow@31952
   130
lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
wenzelm@44872
   131
  unfolding cong_nat_def by auto
nipkow@31719
   132
nipkow@31952
   133
lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
wenzelm@44872
   134
  unfolding cong_int_def by auto
nipkow@31719
   135
nipkow@31952
   136
lemma cong_trans_nat [trans]:
nipkow@31719
   137
    "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
wenzelm@44872
   138
  unfolding cong_nat_def by auto
nipkow@31719
   139
nipkow@31952
   140
lemma cong_trans_int [trans]:
nipkow@31719
   141
    "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
wenzelm@44872
   142
  unfolding cong_int_def by auto
nipkow@31719
   143
nipkow@31952
   144
lemma cong_add_nat:
nipkow@31719
   145
    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
lp15@55130
   146
  unfolding cong_nat_def  by (metis mod_add_cong)
nipkow@31719
   147
nipkow@31952
   148
lemma cong_add_int:
nipkow@31719
   149
    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
lp15@55130
   150
  unfolding cong_int_def  by (metis mod_add_cong)
nipkow@31719
   151
nipkow@31952
   152
lemma cong_diff_int:
nipkow@31719
   153
    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
lp15@55130
   154
  unfolding cong_int_def  by (metis mod_diff_cong) 
nipkow@31719
   155
nipkow@31952
   156
lemma cong_diff_aux_int:
lp15@55321
   157
  "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow>
lp15@55321
   158
   (a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
lp15@55130
   159
  by (metis cong_diff_int tsub_eq)
nipkow@31719
   160
nipkow@31952
   161
lemma cong_diff_nat:
lp15@55321
   162
  assumes"[a = b] (mod m)" "[c = d] (mod m)" "(a::nat) >= c" "b >= d" 
nipkow@31719
   163
  shows "[a - c = b - d] (mod m)"
wenzelm@58860
   164
  using assms by (rule cong_diff_aux_int [transferred])
nipkow@31719
   165
nipkow@31952
   166
lemma cong_mult_nat:
nipkow@31719
   167
    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
lp15@55130
   168
  unfolding cong_nat_def  by (metis mod_mult_cong) 
nipkow@31719
   169
nipkow@31952
   170
lemma cong_mult_int:
nipkow@31719
   171
    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
lp15@55130
   172
  unfolding cong_int_def  by (metis mod_mult_cong) 
nipkow@31719
   173
wenzelm@44872
   174
lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
wenzelm@44872
   175
  by (induct k) (auto simp add: cong_mult_nat)
wenzelm@44872
   176
wenzelm@44872
   177
lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
wenzelm@44872
   178
  by (induct k) (auto simp add: cong_mult_int)
wenzelm@44872
   179
wenzelm@44872
   180
lemma cong_setsum_nat [rule_format]:
wenzelm@44872
   181
    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
nipkow@31719
   182
      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
wenzelm@44872
   183
  apply (cases "finite A")
nipkow@31719
   184
  apply (induct set: finite)
nipkow@31952
   185
  apply (auto intro: cong_add_nat)
wenzelm@44872
   186
  done
nipkow@31719
   187
nipkow@31952
   188
lemma cong_setsum_int [rule_format]:
wenzelm@44872
   189
    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
nipkow@31719
   190
      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
wenzelm@44872
   191
  apply (cases "finite A")
nipkow@31719
   192
  apply (induct set: finite)
nipkow@31952
   193
  apply (auto intro: cong_add_int)
wenzelm@44872
   194
  done
nipkow@31719
   195
wenzelm@44872
   196
lemma cong_setprod_nat [rule_format]:
wenzelm@44872
   197
    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
nipkow@31719
   198
      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
wenzelm@44872
   199
  apply (cases "finite A")
nipkow@31719
   200
  apply (induct set: finite)
nipkow@31952
   201
  apply (auto intro: cong_mult_nat)
wenzelm@44872
   202
  done
nipkow@31719
   203
wenzelm@44872
   204
lemma cong_setprod_int [rule_format]:
wenzelm@44872
   205
    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
nipkow@31719
   206
      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
wenzelm@44872
   207
  apply (cases "finite A")
nipkow@31719
   208
  apply (induct set: finite)
nipkow@31952
   209
  apply (auto intro: cong_mult_int)
wenzelm@44872
   210
  done
nipkow@31719
   211
nipkow@31952
   212
lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
wenzelm@44872
   213
  by (rule cong_mult_nat) simp_all
nipkow@31719
   214
nipkow@31952
   215
lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
wenzelm@44872
   216
  by (rule cong_mult_int) simp_all
nipkow@31719
   217
nipkow@31952
   218
lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
wenzelm@44872
   219
  by (rule cong_mult_nat) simp_all
nipkow@31719
   220
nipkow@31952
   221
lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
wenzelm@44872
   222
  by (rule cong_mult_int) simp_all
nipkow@31719
   223
nipkow@31952
   224
lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
wenzelm@44872
   225
  unfolding cong_nat_def by auto
nipkow@31719
   226
nipkow@31952
   227
lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
wenzelm@44872
   228
  unfolding cong_int_def by auto
nipkow@31719
   229
nipkow@31952
   230
lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
lp15@55130
   231
  by (metis cong_add_int cong_diff_int cong_refl_int diff_add_cancel diff_self)
nipkow@31719
   232
nipkow@31952
   233
lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
nipkow@31719
   234
    [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
nipkow@31952
   235
  by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
nipkow@31719
   236
nipkow@31952
   237
lemma cong_eq_diff_cong_0_nat:
nipkow@31719
   238
  assumes "(a::nat) >= b"
nipkow@31719
   239
  shows "[a = b] (mod m) = [a - b = 0] (mod m)"
wenzelm@41541
   240
  using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
nipkow@31719
   241
wenzelm@44872
   242
lemma cong_diff_cong_0'_nat:
wenzelm@44872
   243
  "[(x::nat) = y] (mod n) \<longleftrightarrow>
nipkow@31719
   244
    (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
lp15@55130
   245
  by (metis cong_eq_diff_cong_0_nat cong_sym_nat nat_le_linear)
nipkow@31719
   246
nipkow@31952
   247
lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
nipkow@31952
   248
  apply (subst cong_eq_diff_cong_0_nat, assumption)
nipkow@31719
   249
  apply (unfold cong_nat_def)
nipkow@31719
   250
  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
wenzelm@44872
   251
  done
nipkow@31719
   252
nipkow@31952
   253
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
lp15@55371
   254
  by (metis cong_int_def zmod_eq_dvd_iff)
nipkow@31719
   255
nipkow@31952
   256
lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
nipkow@31952
   257
  by (simp add: cong_altdef_int)
nipkow@31719
   258
nipkow@31952
   259
lemma cong_square_int:
lp15@55242
   260
  fixes a::int
lp15@55242
   261
  shows "\<lbrakk> prime p; 0 < a; [a * a = 1] (mod p) \<rbrakk>
nipkow@31719
   262
    \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
nipkow@31952
   263
  apply (simp only: cong_altdef_int)
nipkow@31952
   264
  apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
haftmann@36350
   265
  apply (auto simp add: field_simps)
wenzelm@44872
   266
  done
nipkow@31719
   267
nipkow@31952
   268
lemma cong_mult_rcancel_int:
wenzelm@44872
   269
    "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
lp15@55371
   270
  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd_int.commute)
nipkow@31719
   271
nipkow@31952
   272
lemma cong_mult_rcancel_nat:
lp15@55371
   273
    "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
lp15@55371
   274
  by (metis cong_mult_rcancel_int [transferred])
nipkow@31719
   275
nipkow@31952
   276
lemma cong_mult_lcancel_nat:
wenzelm@44872
   277
    "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
haftmann@57512
   278
  by (simp add: mult.commute cong_mult_rcancel_nat)
nipkow@31719
   279
nipkow@31952
   280
lemma cong_mult_lcancel_int:
wenzelm@44872
   281
    "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
haftmann@57512
   282
  by (simp add: mult.commute cong_mult_rcancel_int)
nipkow@31719
   283
nipkow@31719
   284
(* was zcong_zgcd_zmult_zmod *)
nipkow@31952
   285
lemma coprime_cong_mult_int:
nipkow@31719
   286
  "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
nipkow@31719
   287
    \<Longrightarrow> [a = b] (mod m * n)"
lp15@55371
   288
by (metis divides_mult_int cong_altdef_int)
nipkow@31719
   289
nipkow@31952
   290
lemma coprime_cong_mult_nat:
nipkow@31719
   291
  assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
nipkow@31719
   292
  shows "[a = b] (mod m * n)"
lp15@55371
   293
  by (metis assms coprime_cong_mult_int [transferred])
nipkow@31719
   294
nipkow@31952
   295
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
nipkow@31719
   296
    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
wenzelm@41541
   297
  by (auto simp add: cong_nat_def)
nipkow@31719
   298
nipkow@31952
   299
lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
nipkow@31719
   300
    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
wenzelm@41541
   301
  by (auto simp add: cong_int_def)
nipkow@31719
   302
nipkow@31952
   303
lemma cong_less_unique_nat:
nipkow@31719
   304
    "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
lp15@55371
   305
  by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial)
nipkow@31719
   306
nipkow@31952
   307
lemma cong_less_unique_int:
nipkow@31719
   308
    "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
lp15@55371
   309
  by (auto simp: cong_int_def)  (metis mod_mod_trivial pos_mod_conj)
nipkow@31719
   310
nipkow@31952
   311
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
lp15@55371
   312
  apply (auto simp add: cong_altdef_int dvd_def)
nipkow@31719
   313
  apply (rule_tac [!] x = "-k" in exI, auto)
wenzelm@44872
   314
  done
nipkow@31719
   315
lp15@55371
   316
lemma cong_iff_lin_nat: 
lp15@55371
   317
   "([(a::nat) = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" (is "?lhs = ?rhs")
lp15@55371
   318
proof (rule iffI)
lp15@55371
   319
  assume eqm: ?lhs
lp15@55371
   320
  show ?rhs
lp15@55371
   321
  proof (cases "b \<le> a")
lp15@55371
   322
    case True
lp15@55371
   323
    then show ?rhs using eqm
haftmann@57512
   324
      by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult.commute)
lp15@55371
   325
  next
lp15@55371
   326
    case False
lp15@55371
   327
    then show ?rhs using eqm 
lp15@55371
   328
      apply (subst (asm) cong_sym_eq_nat)
lp15@55371
   329
      apply (auto simp: cong_altdef_nat)
lp15@55371
   330
      apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
lp15@55371
   331
      done
lp15@55371
   332
  qed
lp15@55371
   333
next
lp15@55371
   334
  assume ?rhs
lp15@55371
   335
  then show ?lhs
haftmann@57512
   336
    by (metis cong_nat_def mod_mult_self2 mult.commute)
lp15@55371
   337
qed
nipkow@31719
   338
nipkow@31952
   339
lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
lp15@55371
   340
  by (metis cong_int_def gcd_red_int)
nipkow@31719
   341
wenzelm@44872
   342
lemma cong_gcd_eq_nat:
lp15@55371
   343
    "[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
lp15@55371
   344
  by (metis assms cong_gcd_eq_int [transferred])
nipkow@31719
   345
wenzelm@44872
   346
lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
nipkow@31952
   347
  by (auto simp add: cong_gcd_eq_nat)
nipkow@31719
   348
wenzelm@44872
   349
lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
nipkow@31952
   350
  by (auto simp add: cong_gcd_eq_int)
nipkow@31719
   351
wenzelm@44872
   352
lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = [a mod m = b mod m] (mod m)"
nipkow@31719
   353
  by (auto simp add: cong_nat_def)
nipkow@31719
   354
wenzelm@44872
   355
lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = [a mod m = b mod m] (mod m)"
nipkow@31719
   356
  by (auto simp add: cong_int_def)
nipkow@31719
   357
nipkow@31952
   358
lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
lp15@55371
   359
  by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
nipkow@31719
   360
nipkow@31719
   361
(*
nipkow@31952
   362
lemma mod_dvd_mod_int:
nipkow@31719
   363
    "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
nipkow@31719
   364
  apply (unfold dvd_def, auto)
nipkow@31719
   365
  apply (rule mod_mod_cancel)
nipkow@31719
   366
  apply auto
wenzelm@44872
   367
  done
nipkow@31719
   368
nipkow@31719
   369
lemma mod_dvd_mod:
nipkow@31719
   370
  assumes "0 < (m::nat)" and "m dvd b"
nipkow@31719
   371
  shows "(a mod b mod m) = (a mod m)"
nipkow@31719
   372
nipkow@31952
   373
  apply (rule mod_dvd_mod_int [transferred])
wenzelm@41541
   374
  using assms apply auto
wenzelm@41541
   375
  done
nipkow@31719
   376
*)
nipkow@31719
   377
wenzelm@44872
   378
lemma cong_add_lcancel_nat:
wenzelm@44872
   379
    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
nipkow@31952
   380
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   381
wenzelm@44872
   382
lemma cong_add_lcancel_int:
wenzelm@44872
   383
    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
nipkow@31952
   384
  by (simp add: cong_iff_lin_int)
nipkow@31719
   385
nipkow@31952
   386
lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
nipkow@31952
   387
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   388
nipkow@31952
   389
lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
nipkow@31952
   390
  by (simp add: cong_iff_lin_int)
nipkow@31719
   391
wenzelm@44872
   392
lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
nipkow@31952
   393
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   394
wenzelm@44872
   395
lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
nipkow@31952
   396
  by (simp add: cong_iff_lin_int)
nipkow@31719
   397
wenzelm@44872
   398
lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
nipkow@31952
   399
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   400
wenzelm@44872
   401
lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
nipkow@31952
   402
  by (simp add: cong_iff_lin_int)
nipkow@31719
   403
wenzelm@44872
   404
lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow>
nipkow@31719
   405
    [x = y] (mod n)"
nipkow@31952
   406
  apply (auto simp add: cong_iff_lin_nat dvd_def)
nipkow@31719
   407
  apply (rule_tac x="k1 * k" in exI)
nipkow@31719
   408
  apply (rule_tac x="k2 * k" in exI)
haftmann@36350
   409
  apply (simp add: field_simps)
wenzelm@44872
   410
  done
nipkow@31719
   411
wenzelm@44872
   412
lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
nipkow@31952
   413
  by (auto simp add: cong_altdef_int dvd_def)
nipkow@31719
   414
nipkow@31952
   415
lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
wenzelm@44872
   416
  unfolding cong_nat_def by (auto simp add: dvd_eq_mod_eq_0)
nipkow@31719
   417
nipkow@31952
   418
lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
wenzelm@44872
   419
  unfolding cong_int_def by (auto simp add: dvd_eq_mod_eq_0)
nipkow@31719
   420
wenzelm@44872
   421
lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
nipkow@31719
   422
  by (simp add: cong_nat_def)
nipkow@31719
   423
wenzelm@44872
   424
lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)"
nipkow@31719
   425
  by (simp add: cong_int_def)
nipkow@31719
   426
wenzelm@44872
   427
lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0
nipkow@31719
   428
    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
nipkow@31719
   429
  by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
nipkow@31719
   430
nipkow@31952
   431
lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
lp15@55371
   432
  by (metis cong_int_def minus_minus zminus_zmod)
nipkow@31719
   433
nipkow@31952
   434
lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
nipkow@31952
   435
  by (auto simp add: cong_altdef_int)
nipkow@31719
   436
wenzelm@44872
   437
lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
nipkow@31719
   438
    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
lp15@55371
   439
  apply (cases "b > 0", simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
nipkow@31952
   440
  apply (subst (1 2) cong_modulus_neg_int)
nipkow@31719
   441
  apply (unfold cong_int_def)
nipkow@31719
   442
  apply (subgoal_tac "a * b = (-a * -b)")
nipkow@31719
   443
  apply (erule ssubst)
nipkow@31719
   444
  apply (subst zmod_zmult2_eq)
haftmann@54230
   445
  apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
haftmann@54230
   446
  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+
wenzelm@44872
   447
  done
nipkow@31719
   448
nipkow@31952
   449
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
lp15@55371
   450
  apply (cases "a = 0", force)
lp15@55371
   451
  by (metis cong_altdef_nat leI less_one)
nipkow@31719
   452
lp15@55130
   453
lemma cong_0_1_nat': "[(0::nat) = Suc 0] (mod n) = (n = Suc 0)"
lp15@55130
   454
  unfolding cong_nat_def by auto
lp15@55130
   455
nipkow@31952
   456
lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
wenzelm@44872
   457
  unfolding cong_nat_def by auto
nipkow@31719
   458
nipkow@31952
   459
lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
wenzelm@44872
   460
  unfolding cong_int_def by (auto simp add: zmult_eq_1_iff)
nipkow@31719
   461
wenzelm@44872
   462
lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
nipkow@31719
   463
    a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
wenzelm@44872
   464
  apply (cases "n = 1")
nipkow@31719
   465
  apply auto [1]
nipkow@31719
   466
  apply (drule_tac x = "a - 1" in spec)
nipkow@31719
   467
  apply force
lp15@55371
   468
  apply (cases "a = 0", simp add: cong_0_1_nat)
nipkow@31719
   469
  apply (rule iffI)
haftmann@57512
   470
  apply (metis cong_to_1_nat dvd_def monoid_mult_class.mult.right_neutral mult.commute mult_eq_if)
lp15@55371
   471
  apply (metis cong_add_lcancel_0_nat cong_mult_self_nat)
wenzelm@44872
   472
  done
nipkow@31719
   473
nipkow@31952
   474
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
haftmann@57512
   475
  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
nipkow@31719
   476
nipkow@31952
   477
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
wenzelm@44872
   478
  apply (cases "n = 0")
nipkow@31719
   479
  apply force
nipkow@31952
   480
  apply (frule bezout_nat [of a n], auto)
haftmann@57512
   481
  by (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute)
nipkow@31719
   482
nipkow@31952
   483
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
wenzelm@44872
   484
  apply (cases "n = 0")
wenzelm@44872
   485
  apply (cases "a \<ge> 0")
nipkow@31719
   486
  apply auto
nipkow@31719
   487
  apply (rule_tac x = "-1" in exI)
nipkow@31719
   488
  apply auto
nipkow@31952
   489
  apply (insert bezout_int [of a n], auto)
haftmann@57512
   490
  by (metis cong_iff_lin_int mult.commute)
wenzelm@44872
   491
wenzelm@44872
   492
lemma cong_solve_dvd_nat:
nipkow@31719
   493
  assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
nipkow@31719
   494
  shows "EX x. [a * x = d] (mod n)"
nipkow@31719
   495
proof -
wenzelm@44872
   496
  from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
nipkow@31719
   497
    by auto
wenzelm@44872
   498
  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
nipkow@31952
   499
    by (elim cong_scalar2_nat)
nipkow@31719
   500
  also from b have "(d div gcd a n) * gcd a n = d"
nipkow@31719
   501
    by (rule dvd_div_mult_self)
nipkow@31719
   502
  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
nipkow@31719
   503
    by auto
nipkow@31719
   504
  finally show ?thesis
nipkow@31719
   505
    by auto
nipkow@31719
   506
qed
nipkow@31719
   507
wenzelm@44872
   508
lemma cong_solve_dvd_int:
nipkow@31719
   509
  assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
nipkow@31719
   510
  shows "EX x. [a * x = d] (mod n)"
nipkow@31719
   511
proof -
wenzelm@44872
   512
  from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
nipkow@31719
   513
    by auto
wenzelm@44872
   514
  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
nipkow@31952
   515
    by (elim cong_scalar2_int)
nipkow@31719
   516
  also from b have "(d div gcd a n) * gcd a n = d"
nipkow@31719
   517
    by (rule dvd_div_mult_self)
nipkow@31719
   518
  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
nipkow@31719
   519
    by auto
nipkow@31719
   520
  finally show ?thesis
nipkow@31719
   521
    by auto
nipkow@31719
   522
qed
nipkow@31719
   523
wenzelm@44872
   524
lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
wenzelm@44872
   525
  apply (cases "a = 0")
nipkow@31719
   526
  apply force
lp15@55161
   527
  apply (metis cong_solve_nat)
wenzelm@44872
   528
  done
nipkow@31719
   529
wenzelm@44872
   530
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
wenzelm@44872
   531
  apply (cases "a = 0")
nipkow@31719
   532
  apply auto
wenzelm@44872
   533
  apply (cases "n \<ge> 0")
nipkow@31719
   534
  apply auto
lp15@55161
   535
  apply (metis cong_solve_int)
lp15@55161
   536
  done
lp15@55161
   537
lp15@55161
   538
lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
lp15@55337
   539
  apply (auto intro: cong_solve_coprime_nat simp: One_nat_def)
lp15@55161
   540
  apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
lp15@55161
   541
  apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
lp15@55161
   542
      gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute)
wenzelm@44872
   543
  done
nipkow@31719
   544
lp15@55161
   545
lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
lp15@55161
   546
  apply (auto intro: cong_solve_coprime_int)
lp15@55161
   547
  apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd_int.commute gcd_red_int)
wenzelm@44872
   548
  done
nipkow@31719
   549
lp15@55161
   550
lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m =
lp15@55161
   551
    (EX x. 0 \<le> x & x < m & [a * x = Suc 0] (mod m))"
lp15@55161
   552
  apply (subst coprime_iff_invertible_nat)
lp15@55161
   553
  apply auto
lp15@55161
   554
  apply (auto simp add: cong_nat_def)
lp15@55161
   555
  apply (metis mod_less_divisor mod_mult_right_eq)
wenzelm@44872
   556
  done
nipkow@31719
   557
lp15@55161
   558
lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
nipkow@31719
   559
    (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
nipkow@31952
   560
  apply (subst coprime_iff_invertible_int)
nipkow@31719
   561
  apply (auto simp add: cong_int_def)
lp15@55371
   562
  apply (metis mod_mult_right_eq pos_mod_conj)
wenzelm@44872
   563
  done
nipkow@31719
   564
nipkow@31952
   565
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
nipkow@31719
   566
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
wenzelm@44872
   567
  apply (cases "y \<le> x")
lp15@55371
   568
  apply (metis cong_altdef_nat lcm_least_nat)
lp15@55371
   569
  apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
wenzelm@44872
   570
  done
nipkow@31719
   571
nipkow@31952
   572
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
nipkow@31719
   573
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
nipkow@31952
   574
  by (auto simp add: cong_altdef_int lcm_least_int) [1]
nipkow@31719
   575
nipkow@31952
   576
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   577
    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   578
    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
nipkow@31719
   579
      [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   580
  apply (induct set: finite)
nipkow@31719
   581
  apply auto
lp15@55371
   582
  apply (metis coprime_cong_mult_nat gcd_semilattice_nat.inf_commute setprod_coprime_nat)
wenzelm@44872
   583
  done
nipkow@31719
   584
nipkow@31952
   585
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   586
    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   587
    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
nipkow@31719
   588
      [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   589
  apply (induct set: finite)
nipkow@31719
   590
  apply auto
lp15@55371
   591
  apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int)
wenzelm@44872
   592
  done
nipkow@31719
   593
wenzelm@44872
   594
lemma binary_chinese_remainder_aux_nat:
nipkow@31719
   595
  assumes a: "coprime (m1::nat) m2"
nipkow@31719
   596
  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
nipkow@31719
   597
    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
nipkow@31719
   598
proof -
wenzelm@44872
   599
  from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
nipkow@31719
   600
    by auto
wenzelm@44872
   601
  from a have b: "coprime m2 m1"
nipkow@31952
   602
    by (subst gcd_commute_nat)
wenzelm@44872
   603
  from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
nipkow@31719
   604
    by auto
nipkow@31719
   605
  have "[m1 * x1 = 0] (mod m1)"
haftmann@57512
   606
    by (subst mult.commute, rule cong_mult_self_nat)
nipkow@31719
   607
  moreover have "[m2 * x2 = 0] (mod m2)"
haftmann@57512
   608
    by (subst mult.commute, rule cong_mult_self_nat)
nipkow@31719
   609
  moreover note one two
nipkow@31719
   610
  ultimately show ?thesis by blast
nipkow@31719
   611
qed
nipkow@31719
   612
wenzelm@44872
   613
lemma binary_chinese_remainder_aux_int:
nipkow@31719
   614
  assumes a: "coprime (m1::int) m2"
nipkow@31719
   615
  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
nipkow@31719
   616
    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
nipkow@31719
   617
proof -
wenzelm@44872
   618
  from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
nipkow@31719
   619
    by auto
wenzelm@44872
   620
  from a have b: "coprime m2 m1"
nipkow@31952
   621
    by (subst gcd_commute_int)
wenzelm@44872
   622
  from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
nipkow@31719
   623
    by auto
nipkow@31719
   624
  have "[m1 * x1 = 0] (mod m1)"
haftmann@57512
   625
    by (subst mult.commute, rule cong_mult_self_int)
nipkow@31719
   626
  moreover have "[m2 * x2 = 0] (mod m2)"
haftmann@57512
   627
    by (subst mult.commute, rule cong_mult_self_int)
nipkow@31719
   628
  moreover note one two
nipkow@31719
   629
  ultimately show ?thesis by blast
nipkow@31719
   630
qed
nipkow@31719
   631
nipkow@31952
   632
lemma binary_chinese_remainder_nat:
nipkow@31719
   633
  assumes a: "coprime (m1::nat) m2"
nipkow@31719
   634
  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   635
proof -
nipkow@31952
   636
  from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
wenzelm@44872
   637
      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
wenzelm@44872
   638
            "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
nipkow@31719
   639
    by blast
nipkow@31719
   640
  let ?x = "u1 * b1 + u2 * b2"
nipkow@31719
   641
  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
nipkow@31952
   642
    apply (rule cong_add_nat)
nipkow@31952
   643
    apply (rule cong_scalar2_nat)
nipkow@31719
   644
    apply (rule `[b1 = 1] (mod m1)`)
nipkow@31952
   645
    apply (rule cong_scalar2_nat)
nipkow@31719
   646
    apply (rule `[b2 = 0] (mod m1)`)
nipkow@31719
   647
    done
wenzelm@44872
   648
  then have "[?x = u1] (mod m1)" by simp
nipkow@31719
   649
  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
nipkow@31952
   650
    apply (rule cong_add_nat)
nipkow@31952
   651
    apply (rule cong_scalar2_nat)
nipkow@31719
   652
    apply (rule `[b1 = 0] (mod m2)`)
nipkow@31952
   653
    apply (rule cong_scalar2_nat)
nipkow@31719
   654
    apply (rule `[b2 = 1] (mod m2)`)
nipkow@31719
   655
    done
wenzelm@44872
   656
  then have "[?x = u2] (mod m2)" by simp
nipkow@31719
   657
  with `[?x = u1] (mod m1)` show ?thesis by blast
nipkow@31719
   658
qed
nipkow@31719
   659
nipkow@31952
   660
lemma binary_chinese_remainder_int:
nipkow@31719
   661
  assumes a: "coprime (m1::int) m2"
nipkow@31719
   662
  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   663
proof -
nipkow@31952
   664
  from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
nipkow@31719
   665
    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
nipkow@31719
   666
          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
nipkow@31719
   667
    by blast
nipkow@31719
   668
  let ?x = "u1 * b1 + u2 * b2"
nipkow@31719
   669
  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
nipkow@31952
   670
    apply (rule cong_add_int)
nipkow@31952
   671
    apply (rule cong_scalar2_int)
nipkow@31719
   672
    apply (rule `[b1 = 1] (mod m1)`)
nipkow@31952
   673
    apply (rule cong_scalar2_int)
nipkow@31719
   674
    apply (rule `[b2 = 0] (mod m1)`)
nipkow@31719
   675
    done
wenzelm@44872
   676
  then have "[?x = u1] (mod m1)" by simp
nipkow@31719
   677
  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
nipkow@31952
   678
    apply (rule cong_add_int)
nipkow@31952
   679
    apply (rule cong_scalar2_int)
nipkow@31719
   680
    apply (rule `[b1 = 0] (mod m2)`)
nipkow@31952
   681
    apply (rule cong_scalar2_int)
nipkow@31719
   682
    apply (rule `[b2 = 1] (mod m2)`)
nipkow@31719
   683
    done
wenzelm@44872
   684
  then have "[?x = u2] (mod m2)" by simp
nipkow@31719
   685
  with `[?x = u1] (mod m1)` show ?thesis by blast
nipkow@31719
   686
qed
nipkow@31719
   687
wenzelm@44872
   688
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
nipkow@31719
   689
    [x = y] (mod m)"
wenzelm@44872
   690
  apply (cases "y \<le> x")
nipkow@31952
   691
  apply (simp add: cong_altdef_nat)
nipkow@31719
   692
  apply (erule dvd_mult_left)
nipkow@31952
   693
  apply (rule cong_sym_nat)
nipkow@31952
   694
  apply (subst (asm) cong_sym_eq_nat)
wenzelm@44872
   695
  apply (simp add: cong_altdef_nat)
nipkow@31719
   696
  apply (erule dvd_mult_left)
wenzelm@44872
   697
  done
nipkow@31719
   698
wenzelm@44872
   699
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
nipkow@31719
   700
    [x = y] (mod m)"
wenzelm@44872
   701
  apply (simp add: cong_altdef_int)
nipkow@31719
   702
  apply (erule dvd_mult_left)
wenzelm@44872
   703
  done
nipkow@31719
   704
wenzelm@44872
   705
lemma cong_less_modulus_unique_nat:
nipkow@31719
   706
    "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
nipkow@31719
   707
  by (simp add: cong_nat_def)
nipkow@31719
   708
nipkow@31952
   709
lemma binary_chinese_remainder_unique_nat:
wenzelm@44872
   710
  assumes a: "coprime (m1::nat) m2"
wenzelm@44872
   711
    and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
nipkow@31719
   712
  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   713
proof -
wenzelm@44872
   714
  from binary_chinese_remainder_nat [OF a] obtain y where
nipkow@31719
   715
      "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
nipkow@31719
   716
    by blast
nipkow@31719
   717
  let ?x = "y mod (m1 * m2)"
nipkow@31719
   718
  from nz have less: "?x < m1 * m2"
wenzelm@44872
   719
    by auto
nipkow@31719
   720
  have one: "[?x = u1] (mod m1)"
nipkow@31952
   721
    apply (rule cong_trans_nat)
nipkow@31719
   722
    prefer 2
nipkow@31719
   723
    apply (rule `[y = u1] (mod m1)`)
nipkow@31952
   724
    apply (rule cong_modulus_mult_nat)
nipkow@31952
   725
    apply (rule cong_mod_nat)
nipkow@31719
   726
    using nz apply auto
nipkow@31719
   727
    done
nipkow@31719
   728
  have two: "[?x = u2] (mod m2)"
nipkow@31952
   729
    apply (rule cong_trans_nat)
nipkow@31719
   730
    prefer 2
nipkow@31719
   731
    apply (rule `[y = u2] (mod m2)`)
haftmann@57512
   732
    apply (subst mult.commute)
nipkow@31952
   733
    apply (rule cong_modulus_mult_nat)
nipkow@31952
   734
    apply (rule cong_mod_nat)
nipkow@31719
   735
    using nz apply auto
nipkow@31719
   736
    done
wenzelm@44872
   737
  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
wenzelm@44872
   738
  proof clarify
nipkow@31719
   739
    fix z
nipkow@31719
   740
    assume "z < m1 * m2"
nipkow@31719
   741
    assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
nipkow@31719
   742
    have "[?x = z] (mod m1)"
nipkow@31952
   743
      apply (rule cong_trans_nat)
nipkow@31719
   744
      apply (rule `[?x = u1] (mod m1)`)
nipkow@31952
   745
      apply (rule cong_sym_nat)
nipkow@31719
   746
      apply (rule `[z = u1] (mod m1)`)
nipkow@31719
   747
      done
nipkow@31719
   748
    moreover have "[?x = z] (mod m2)"
nipkow@31952
   749
      apply (rule cong_trans_nat)
nipkow@31719
   750
      apply (rule `[?x = u2] (mod m2)`)
nipkow@31952
   751
      apply (rule cong_sym_nat)
nipkow@31719
   752
      apply (rule `[z = u2] (mod m2)`)
nipkow@31719
   753
      done
nipkow@31719
   754
    ultimately have "[?x = z] (mod m1 * m2)"
nipkow@31952
   755
      by (auto intro: coprime_cong_mult_nat a)
nipkow@31719
   756
    with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
nipkow@31952
   757
      apply (intro cong_less_modulus_unique_nat)
nipkow@31952
   758
      apply (auto, erule cong_sym_nat)
nipkow@31719
   759
      done
wenzelm@44872
   760
  qed
wenzelm@44872
   761
  with less one two show ?thesis by auto
nipkow@31719
   762
 qed
nipkow@31719
   763
nipkow@31952
   764
lemma chinese_remainder_aux_nat:
wenzelm@44872
   765
  fixes A :: "'a set"
wenzelm@44872
   766
    and m :: "'a \<Rightarrow> nat"
wenzelm@44872
   767
  assumes fin: "finite A"
wenzelm@44872
   768
    and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
wenzelm@44872
   769
  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
nipkow@31719
   770
proof (rule finite_set_choice, rule fin, rule ballI)
nipkow@31719
   771
  fix i
nipkow@31719
   772
  assume "i : A"
nipkow@31719
   773
  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
nipkow@31952
   774
    by (intro setprod_coprime_nat, auto)
wenzelm@44872
   775
  then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
nipkow@31952
   776
    by (elim cong_solve_coprime_nat)
nipkow@31719
   777
  then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
nipkow@31719
   778
    by auto
wenzelm@44872
   779
  moreover have "[(PROD j : A - {i}. m j) * x = 0]
nipkow@31719
   780
    (mod (PROD j : A - {i}. m j))"
haftmann@57512
   781
    by (subst mult.commute, rule cong_mult_self_nat)
wenzelm@44872
   782
  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
nipkow@31719
   783
      (mod setprod m (A - {i}))"
nipkow@31719
   784
    by blast
nipkow@31719
   785
qed
nipkow@31719
   786
nipkow@31952
   787
lemma chinese_remainder_nat:
wenzelm@44872
   788
  fixes A :: "'a set"
wenzelm@44872
   789
    and m :: "'a \<Rightarrow> nat"
wenzelm@44872
   790
    and u :: "'a \<Rightarrow> nat"
wenzelm@44872
   791
  assumes fin: "finite A"
wenzelm@44872
   792
    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
nipkow@31719
   793
  shows "EX x. (ALL i:A. [x = u i] (mod m i))"
nipkow@31719
   794
proof -
nipkow@31952
   795
  from chinese_remainder_aux_nat [OF fin cop] obtain b where
wenzelm@44872
   796
    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
nipkow@31719
   797
      [b i = 0] (mod (PROD j : A - {i}. m j))"
nipkow@31719
   798
    by blast
nipkow@31719
   799
  let ?x = "SUM i:A. (u i) * (b i)"
nipkow@31719
   800
  show "?thesis"
nipkow@31719
   801
  proof (rule exI, clarify)
nipkow@31719
   802
    fix i
nipkow@31719
   803
    assume a: "i : A"
wenzelm@44872
   804
    show "[?x = u i] (mod m i)"
nipkow@31719
   805
    proof -
wenzelm@44872
   806
      from fin a have "?x = (SUM j:{i}. u j * b j) +
nipkow@31719
   807
          (SUM j:A-{i}. u j * b j)"
haftmann@57418
   808
        by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong)
wenzelm@44872
   809
      then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
nipkow@31719
   810
        by auto
nipkow@31719
   811
      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
nipkow@31719
   812
                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
nipkow@31952
   813
        apply (rule cong_add_nat)
nipkow@31952
   814
        apply (rule cong_scalar2_nat)
nipkow@31719
   815
        using bprop a apply blast
nipkow@31952
   816
        apply (rule cong_setsum_nat)
nipkow@31952
   817
        apply (rule cong_scalar2_nat)
nipkow@31719
   818
        using bprop apply auto
nipkow@31952
   819
        apply (rule cong_dvd_modulus_nat)
nipkow@31719
   820
        apply (drule (1) bspec)
nipkow@31719
   821
        apply (erule conjE)
nipkow@31719
   822
        apply assumption
nipkow@31719
   823
        apply (rule dvd_setprod)
nipkow@31719
   824
        using fin a apply auto
nipkow@31719
   825
        done
nipkow@31719
   826
      finally show ?thesis
nipkow@31719
   827
        by simp
nipkow@31719
   828
    qed
nipkow@31719
   829
  qed
nipkow@31719
   830
qed
nipkow@31719
   831
wenzelm@44872
   832
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   833
    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   834
      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
wenzelm@44872
   835
         [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   836
  apply (induct set: finite)
nipkow@31719
   837
  apply auto
haftmann@57512
   838
  apply (metis coprime_cong_mult_nat mult.commute setprod_coprime_nat)
wenzelm@44872
   839
  done
nipkow@31719
   840
nipkow@31952
   841
lemma chinese_remainder_unique_nat:
wenzelm@44872
   842
  fixes A :: "'a set"
wenzelm@44872
   843
    and m :: "'a \<Rightarrow> nat"
wenzelm@44872
   844
    and u :: "'a \<Rightarrow> nat"
wenzelm@44872
   845
  assumes fin: "finite A"
wenzelm@44872
   846
    and nz: "ALL i:A. m i \<noteq> 0"
wenzelm@44872
   847
    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
nipkow@31719
   848
  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
nipkow@31719
   849
proof -
wenzelm@44872
   850
  from chinese_remainder_nat [OF fin cop]
wenzelm@44872
   851
  obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
nipkow@31719
   852
    by blast
nipkow@31719
   853
  let ?x = "y mod (PROD i:A. m i)"
nipkow@31719
   854
  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
nipkow@31719
   855
    by auto
wenzelm@44872
   856
  then have less: "?x < (PROD i:A. m i)"
nipkow@31719
   857
    by auto
nipkow@31719
   858
  have cong: "ALL i:A. [?x = u i] (mod m i)"
nipkow@31719
   859
    apply auto
nipkow@31952
   860
    apply (rule cong_trans_nat)
nipkow@31719
   861
    prefer 2
nipkow@31719
   862
    using one apply auto
nipkow@31952
   863
    apply (rule cong_dvd_modulus_nat)
nipkow@31952
   864
    apply (rule cong_mod_nat)
nipkow@31719
   865
    using prodnz apply auto
nipkow@31719
   866
    apply (rule dvd_setprod)
nipkow@31719
   867
    apply (rule fin)
nipkow@31719
   868
    apply assumption
nipkow@31719
   869
    done
wenzelm@44872
   870
  have unique: "ALL z. z < (PROD i:A. m i) \<and>
nipkow@31719
   871
      (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
nipkow@31719
   872
  proof (clarify)
nipkow@31719
   873
    fix z
nipkow@31719
   874
    assume zless: "z < (PROD i:A. m i)"
nipkow@31719
   875
    assume zcong: "(ALL i:A. [z = u i] (mod m i))"
nipkow@31719
   876
    have "ALL i:A. [?x = z] (mod m i)"
wenzelm@44872
   877
      apply clarify
nipkow@31952
   878
      apply (rule cong_trans_nat)
nipkow@31719
   879
      using cong apply (erule bspec)
nipkow@31952
   880
      apply (rule cong_sym_nat)
nipkow@31719
   881
      using zcong apply auto
nipkow@31719
   882
      done
nipkow@31719
   883
    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
wenzelm@44872
   884
      apply (intro coprime_cong_prod_nat)
wenzelm@44872
   885
      apply auto
wenzelm@44872
   886
      done
nipkow@31719
   887
    with zless less show "z = ?x"
nipkow@31952
   888
      apply (intro cong_less_modulus_unique_nat)
nipkow@31952
   889
      apply (auto, erule cong_sym_nat)
nipkow@31719
   890
      done
wenzelm@44872
   891
  qed
wenzelm@44872
   892
  from less cong unique show ?thesis by blast
nipkow@31719
   893
qed
nipkow@31719
   894
nipkow@31719
   895
end