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