src/HOL/Number_Theory/Cong.thy
author haftmann
Wed Jul 08 14:01:41 2015 +0200 (2015-07-08)
changeset 60688 01488b559910
parent 60526 fad653acf58f
child 61954 1d43f86f48be
permissions -rw-r--r--
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
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@60526
    26
section \<open>Congruence\<close>
nipkow@31719
    27
nipkow@31719
    28
theory Cong
haftmann@37293
    29
imports Primes
nipkow@31719
    30
begin
nipkow@31719
    31
wenzelm@60526
    32
subsection \<open>Turn off @{text One_nat_def}\<close>
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
wenzelm@60526
    40
subsection \<open>Main definitions\<close>
nipkow@31719
    41
nipkow@31719
    42
class cong =
wenzelm@58937
    43
  fixes cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(()mod _'))")
nipkow@31719
    44
begin
nipkow@31719
    45
wenzelm@58937
    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
wenzelm@60526
    77
subsection \<open>Set up Transfer\<close>
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
wenzelm@60526
   100
subsection \<open>Congruence\<close>
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)"
haftmann@60688
   270
  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd.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@59816
   446
  apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 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)"
lp15@59667
   464
by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if)
nipkow@31719
   465
nipkow@31952
   466
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
haftmann@57512
   467
  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
nipkow@31719
   468
nipkow@31952
   469
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
wenzelm@44872
   470
  apply (cases "n = 0")
nipkow@31719
   471
  apply force
nipkow@31952
   472
  apply (frule bezout_nat [of a n], auto)
haftmann@57512
   473
  by (metis cong_add_rcancel_0_nat cong_mult_self_nat mult.commute)
nipkow@31719
   474
nipkow@31952
   475
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
wenzelm@44872
   476
  apply (cases "n = 0")
wenzelm@44872
   477
  apply (cases "a \<ge> 0")
nipkow@31719
   478
  apply auto
nipkow@31719
   479
  apply (rule_tac x = "-1" in exI)
nipkow@31719
   480
  apply auto
nipkow@31952
   481
  apply (insert bezout_int [of a n], auto)
haftmann@57512
   482
  by (metis cong_iff_lin_int mult.commute)
wenzelm@44872
   483
wenzelm@44872
   484
lemma cong_solve_dvd_nat:
nipkow@31719
   485
  assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
nipkow@31719
   486
  shows "EX x. [a * x = d] (mod n)"
nipkow@31719
   487
proof -
wenzelm@44872
   488
  from cong_solve_nat [OF a] obtain x where "[a * x = gcd a n](mod n)"
nipkow@31719
   489
    by auto
wenzelm@44872
   490
  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
nipkow@31952
   491
    by (elim cong_scalar2_nat)
nipkow@31719
   492
  also from b have "(d div gcd a n) * gcd a n = d"
nipkow@31719
   493
    by (rule dvd_div_mult_self)
nipkow@31719
   494
  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
nipkow@31719
   495
    by auto
nipkow@31719
   496
  finally show ?thesis
nipkow@31719
   497
    by auto
nipkow@31719
   498
qed
nipkow@31719
   499
wenzelm@44872
   500
lemma cong_solve_dvd_int:
nipkow@31719
   501
  assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
nipkow@31719
   502
  shows "EX x. [a * x = d] (mod n)"
nipkow@31719
   503
proof -
wenzelm@44872
   504
  from cong_solve_int [OF a] obtain x where "[a * x = gcd a n](mod n)"
nipkow@31719
   505
    by auto
wenzelm@44872
   506
  then have "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)"
nipkow@31952
   507
    by (elim cong_scalar2_int)
nipkow@31719
   508
  also from b have "(d div gcd a n) * gcd a n = d"
nipkow@31719
   509
    by (rule dvd_div_mult_self)
nipkow@31719
   510
  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
nipkow@31719
   511
    by auto
nipkow@31719
   512
  finally show ?thesis
nipkow@31719
   513
    by auto
nipkow@31719
   514
qed
nipkow@31719
   515
wenzelm@44872
   516
lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
wenzelm@44872
   517
  apply (cases "a = 0")
nipkow@31719
   518
  apply force
lp15@55161
   519
  apply (metis cong_solve_nat)
wenzelm@44872
   520
  done
nipkow@31719
   521
wenzelm@44872
   522
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> EX x. [a * x = 1] (mod n)"
wenzelm@44872
   523
  apply (cases "a = 0")
nipkow@31719
   524
  apply auto
wenzelm@44872
   525
  apply (cases "n \<ge> 0")
nipkow@31719
   526
  apply auto
lp15@55161
   527
  apply (metis cong_solve_int)
lp15@55161
   528
  done
lp15@55161
   529
lp15@55161
   530
lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
haftmann@60688
   531
  apply (auto intro: cong_solve_coprime_nat)
lp15@55161
   532
  apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
lp15@55161
   533
  apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
haftmann@60688
   534
      gcd_lcm_complete_lattice_nat.inf_bot_right gcd.commute)
wenzelm@44872
   535
  done
nipkow@31719
   536
lp15@55161
   537
lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
lp15@55161
   538
  apply (auto intro: cong_solve_coprime_int)
haftmann@60688
   539
  apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd.commute gcd_red_int)
wenzelm@44872
   540
  done
nipkow@31719
   541
lp15@55161
   542
lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m =
lp15@55161
   543
    (EX x. 0 \<le> x & x < m & [a * x = Suc 0] (mod m))"
lp15@55161
   544
  apply (subst coprime_iff_invertible_nat)
lp15@55161
   545
  apply auto
lp15@55161
   546
  apply (auto simp add: cong_nat_def)
lp15@55161
   547
  apply (metis mod_less_divisor mod_mult_right_eq)
wenzelm@44872
   548
  done
nipkow@31719
   549
lp15@55161
   550
lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
nipkow@31719
   551
    (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
nipkow@31952
   552
  apply (subst coprime_iff_invertible_int)
nipkow@31719
   553
  apply (auto simp add: cong_int_def)
lp15@55371
   554
  apply (metis mod_mult_right_eq pos_mod_conj)
wenzelm@44872
   555
  done
nipkow@31719
   556
nipkow@31952
   557
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
nipkow@31719
   558
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
wenzelm@44872
   559
  apply (cases "y \<le> x")
lp15@55371
   560
  apply (metis cong_altdef_nat lcm_least_nat)
lp15@55371
   561
  apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
wenzelm@44872
   562
  done
nipkow@31719
   563
nipkow@31952
   564
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
nipkow@31719
   565
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
nipkow@31952
   566
  by (auto simp add: cong_altdef_int lcm_least_int) [1]
nipkow@31719
   567
nipkow@31952
   568
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   569
    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   570
    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
nipkow@31719
   571
      [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   572
  apply (induct set: finite)
nipkow@31719
   573
  apply auto
haftmann@60688
   574
  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
wenzelm@44872
   575
  done
nipkow@31719
   576
nipkow@31952
   577
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   578
    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   579
    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
nipkow@31719
   580
      [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   581
  apply (induct set: finite)
nipkow@31719
   582
  apply auto
haftmann@60688
   583
  apply (metis coprime_cong_mult_int gcd.commute setprod_coprime_int)
wenzelm@44872
   584
  done
nipkow@31719
   585
wenzelm@44872
   586
lemma binary_chinese_remainder_aux_nat:
nipkow@31719
   587
  assumes a: "coprime (m1::nat) m2"
nipkow@31719
   588
  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
nipkow@31719
   589
    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
nipkow@31719
   590
proof -
wenzelm@44872
   591
  from cong_solve_coprime_nat [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
nipkow@31719
   592
    by auto
wenzelm@44872
   593
  from a have b: "coprime m2 m1"
nipkow@31952
   594
    by (subst gcd_commute_nat)
wenzelm@44872
   595
  from cong_solve_coprime_nat [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
nipkow@31719
   596
    by auto
nipkow@31719
   597
  have "[m1 * x1 = 0] (mod m1)"
haftmann@57512
   598
    by (subst mult.commute, rule cong_mult_self_nat)
nipkow@31719
   599
  moreover have "[m2 * x2 = 0] (mod m2)"
haftmann@57512
   600
    by (subst mult.commute, rule cong_mult_self_nat)
nipkow@31719
   601
  moreover note one two
nipkow@31719
   602
  ultimately show ?thesis by blast
nipkow@31719
   603
qed
nipkow@31719
   604
wenzelm@44872
   605
lemma binary_chinese_remainder_aux_int:
nipkow@31719
   606
  assumes a: "coprime (m1::int) m2"
nipkow@31719
   607
  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
nipkow@31719
   608
    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
nipkow@31719
   609
proof -
wenzelm@44872
   610
  from cong_solve_coprime_int [OF a] obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
nipkow@31719
   611
    by auto
wenzelm@44872
   612
  from a have b: "coprime m2 m1"
nipkow@31952
   613
    by (subst gcd_commute_int)
wenzelm@44872
   614
  from cong_solve_coprime_int [OF b] obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
nipkow@31719
   615
    by auto
nipkow@31719
   616
  have "[m1 * x1 = 0] (mod m1)"
haftmann@57512
   617
    by (subst mult.commute, rule cong_mult_self_int)
nipkow@31719
   618
  moreover have "[m2 * x2 = 0] (mod m2)"
haftmann@57512
   619
    by (subst mult.commute, rule cong_mult_self_int)
nipkow@31719
   620
  moreover note one two
nipkow@31719
   621
  ultimately show ?thesis by blast
nipkow@31719
   622
qed
nipkow@31719
   623
nipkow@31952
   624
lemma binary_chinese_remainder_nat:
nipkow@31719
   625
  assumes a: "coprime (m1::nat) m2"
nipkow@31719
   626
  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   627
proof -
nipkow@31952
   628
  from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
wenzelm@44872
   629
      where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
wenzelm@44872
   630
            "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
nipkow@31719
   631
    by blast
nipkow@31719
   632
  let ?x = "u1 * b1 + u2 * b2"
nipkow@31719
   633
  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
nipkow@31952
   634
    apply (rule cong_add_nat)
nipkow@31952
   635
    apply (rule cong_scalar2_nat)
wenzelm@60526
   636
    apply (rule \<open>[b1 = 1] (mod m1)\<close>)
nipkow@31952
   637
    apply (rule cong_scalar2_nat)
wenzelm@60526
   638
    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
nipkow@31719
   639
    done
wenzelm@44872
   640
  then have "[?x = u1] (mod m1)" by simp
nipkow@31719
   641
  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
nipkow@31952
   642
    apply (rule cong_add_nat)
nipkow@31952
   643
    apply (rule cong_scalar2_nat)
wenzelm@60526
   644
    apply (rule \<open>[b1 = 0] (mod m2)\<close>)
nipkow@31952
   645
    apply (rule cong_scalar2_nat)
wenzelm@60526
   646
    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
nipkow@31719
   647
    done
wenzelm@44872
   648
  then have "[?x = u2] (mod m2)" by simp
wenzelm@60526
   649
  with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
nipkow@31719
   650
qed
nipkow@31719
   651
nipkow@31952
   652
lemma binary_chinese_remainder_int:
nipkow@31719
   653
  assumes a: "coprime (m1::int) m2"
nipkow@31719
   654
  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   655
proof -
nipkow@31952
   656
  from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
nipkow@31719
   657
    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
nipkow@31719
   658
          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
nipkow@31719
   659
    by blast
nipkow@31719
   660
  let ?x = "u1 * b1 + u2 * b2"
nipkow@31719
   661
  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
nipkow@31952
   662
    apply (rule cong_add_int)
nipkow@31952
   663
    apply (rule cong_scalar2_int)
wenzelm@60526
   664
    apply (rule \<open>[b1 = 1] (mod m1)\<close>)
nipkow@31952
   665
    apply (rule cong_scalar2_int)
wenzelm@60526
   666
    apply (rule \<open>[b2 = 0] (mod m1)\<close>)
nipkow@31719
   667
    done
wenzelm@44872
   668
  then have "[?x = u1] (mod m1)" by simp
nipkow@31719
   669
  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
nipkow@31952
   670
    apply (rule cong_add_int)
nipkow@31952
   671
    apply (rule cong_scalar2_int)
wenzelm@60526
   672
    apply (rule \<open>[b1 = 0] (mod m2)\<close>)
nipkow@31952
   673
    apply (rule cong_scalar2_int)
wenzelm@60526
   674
    apply (rule \<open>[b2 = 1] (mod m2)\<close>)
nipkow@31719
   675
    done
wenzelm@44872
   676
  then have "[?x = u2] (mod m2)" by simp
wenzelm@60526
   677
  with \<open>[?x = u1] (mod m1)\<close> show ?thesis by blast
nipkow@31719
   678
qed
nipkow@31719
   679
wenzelm@44872
   680
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow>
nipkow@31719
   681
    [x = y] (mod m)"
wenzelm@44872
   682
  apply (cases "y \<le> x")
nipkow@31952
   683
  apply (simp add: cong_altdef_nat)
nipkow@31719
   684
  apply (erule dvd_mult_left)
nipkow@31952
   685
  apply (rule cong_sym_nat)
nipkow@31952
   686
  apply (subst (asm) cong_sym_eq_nat)
wenzelm@44872
   687
  apply (simp add: cong_altdef_nat)
nipkow@31719
   688
  apply (erule dvd_mult_left)
wenzelm@44872
   689
  done
nipkow@31719
   690
wenzelm@44872
   691
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow>
nipkow@31719
   692
    [x = y] (mod m)"
wenzelm@44872
   693
  apply (simp add: cong_altdef_int)
nipkow@31719
   694
  apply (erule dvd_mult_left)
wenzelm@44872
   695
  done
nipkow@31719
   696
wenzelm@44872
   697
lemma cong_less_modulus_unique_nat:
nipkow@31719
   698
    "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
nipkow@31719
   699
  by (simp add: cong_nat_def)
nipkow@31719
   700
nipkow@31952
   701
lemma binary_chinese_remainder_unique_nat:
wenzelm@44872
   702
  assumes a: "coprime (m1::nat) m2"
wenzelm@44872
   703
    and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
nipkow@31719
   704
  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   705
proof -
wenzelm@44872
   706
  from binary_chinese_remainder_nat [OF a] obtain y where
nipkow@31719
   707
      "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
nipkow@31719
   708
    by blast
nipkow@31719
   709
  let ?x = "y mod (m1 * m2)"
nipkow@31719
   710
  from nz have less: "?x < m1 * m2"
wenzelm@44872
   711
    by auto
nipkow@31719
   712
  have one: "[?x = u1] (mod m1)"
nipkow@31952
   713
    apply (rule cong_trans_nat)
nipkow@31719
   714
    prefer 2
wenzelm@60526
   715
    apply (rule \<open>[y = u1] (mod m1)\<close>)
nipkow@31952
   716
    apply (rule cong_modulus_mult_nat)
nipkow@31952
   717
    apply (rule cong_mod_nat)
nipkow@31719
   718
    using nz apply auto
nipkow@31719
   719
    done
nipkow@31719
   720
  have two: "[?x = u2] (mod m2)"
nipkow@31952
   721
    apply (rule cong_trans_nat)
nipkow@31719
   722
    prefer 2
wenzelm@60526
   723
    apply (rule \<open>[y = u2] (mod m2)\<close>)
haftmann@57512
   724
    apply (subst mult.commute)
nipkow@31952
   725
    apply (rule cong_modulus_mult_nat)
nipkow@31952
   726
    apply (rule cong_mod_nat)
nipkow@31719
   727
    using nz apply auto
nipkow@31719
   728
    done
wenzelm@44872
   729
  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow> z = ?x"
wenzelm@44872
   730
  proof clarify
nipkow@31719
   731
    fix z
nipkow@31719
   732
    assume "z < m1 * m2"
nipkow@31719
   733
    assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
nipkow@31719
   734
    have "[?x = z] (mod m1)"
nipkow@31952
   735
      apply (rule cong_trans_nat)
wenzelm@60526
   736
      apply (rule \<open>[?x = u1] (mod m1)\<close>)
nipkow@31952
   737
      apply (rule cong_sym_nat)
wenzelm@60526
   738
      apply (rule \<open>[z = u1] (mod m1)\<close>)
nipkow@31719
   739
      done
nipkow@31719
   740
    moreover have "[?x = z] (mod m2)"
nipkow@31952
   741
      apply (rule cong_trans_nat)
wenzelm@60526
   742
      apply (rule \<open>[?x = u2] (mod m2)\<close>)
nipkow@31952
   743
      apply (rule cong_sym_nat)
wenzelm@60526
   744
      apply (rule \<open>[z = u2] (mod m2)\<close>)
nipkow@31719
   745
      done
nipkow@31719
   746
    ultimately have "[?x = z] (mod m1 * m2)"
nipkow@31952
   747
      by (auto intro: coprime_cong_mult_nat a)
wenzelm@60526
   748
    with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
nipkow@31952
   749
      apply (intro cong_less_modulus_unique_nat)
nipkow@31952
   750
      apply (auto, erule cong_sym_nat)
nipkow@31719
   751
      done
wenzelm@44872
   752
  qed
wenzelm@44872
   753
  with less one two show ?thesis by auto
nipkow@31719
   754
 qed
nipkow@31719
   755
nipkow@31952
   756
lemma chinese_remainder_aux_nat:
wenzelm@44872
   757
  fixes A :: "'a set"
wenzelm@44872
   758
    and m :: "'a \<Rightarrow> nat"
wenzelm@44872
   759
  assumes fin: "finite A"
wenzelm@44872
   760
    and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
wenzelm@44872
   761
  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
   762
proof (rule finite_set_choice, rule fin, rule ballI)
nipkow@31719
   763
  fix i
nipkow@31719
   764
  assume "i : A"
nipkow@31719
   765
  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
nipkow@31952
   766
    by (intro setprod_coprime_nat, auto)
wenzelm@44872
   767
  then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
nipkow@31952
   768
    by (elim cong_solve_coprime_nat)
nipkow@31719
   769
  then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
nipkow@31719
   770
    by auto
wenzelm@44872
   771
  moreover have "[(PROD j : A - {i}. m j) * x = 0]
nipkow@31719
   772
    (mod (PROD j : A - {i}. m j))"
haftmann@57512
   773
    by (subst mult.commute, rule cong_mult_self_nat)
wenzelm@44872
   774
  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
nipkow@31719
   775
      (mod setprod m (A - {i}))"
nipkow@31719
   776
    by blast
nipkow@31719
   777
qed
nipkow@31719
   778
nipkow@31952
   779
lemma chinese_remainder_nat:
wenzelm@44872
   780
  fixes A :: "'a set"
wenzelm@44872
   781
    and m :: "'a \<Rightarrow> nat"
wenzelm@44872
   782
    and u :: "'a \<Rightarrow> nat"
wenzelm@44872
   783
  assumes fin: "finite A"
wenzelm@44872
   784
    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
nipkow@31719
   785
  shows "EX x. (ALL i:A. [x = u i] (mod m i))"
nipkow@31719
   786
proof -
nipkow@31952
   787
  from chinese_remainder_aux_nat [OF fin cop] obtain b where
wenzelm@44872
   788
    bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
nipkow@31719
   789
      [b i = 0] (mod (PROD j : A - {i}. m j))"
nipkow@31719
   790
    by blast
nipkow@31719
   791
  let ?x = "SUM i:A. (u i) * (b i)"
nipkow@31719
   792
  show "?thesis"
nipkow@31719
   793
  proof (rule exI, clarify)
nipkow@31719
   794
    fix i
nipkow@31719
   795
    assume a: "i : A"
wenzelm@44872
   796
    show "[?x = u i] (mod m i)"
nipkow@31719
   797
    proof -
wenzelm@44872
   798
      from fin a have "?x = (SUM j:{i}. u j * b j) +
nipkow@31719
   799
          (SUM j:A-{i}. u j * b j)"
haftmann@57418
   800
        by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong)
wenzelm@44872
   801
      then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
nipkow@31719
   802
        by auto
nipkow@31719
   803
      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
nipkow@31719
   804
                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
nipkow@31952
   805
        apply (rule cong_add_nat)
nipkow@31952
   806
        apply (rule cong_scalar2_nat)
nipkow@31719
   807
        using bprop a apply blast
nipkow@31952
   808
        apply (rule cong_setsum_nat)
nipkow@31952
   809
        apply (rule cong_scalar2_nat)
nipkow@31719
   810
        using bprop apply auto
nipkow@31952
   811
        apply (rule cong_dvd_modulus_nat)
nipkow@31719
   812
        apply (drule (1) bspec)
nipkow@31719
   813
        apply (erule conjE)
nipkow@31719
   814
        apply assumption
haftmann@59010
   815
        apply rule
nipkow@31719
   816
        using fin a apply auto
nipkow@31719
   817
        done
nipkow@31719
   818
      finally show ?thesis
nipkow@31719
   819
        by simp
nipkow@31719
   820
    qed
nipkow@31719
   821
  qed
nipkow@31719
   822
qed
nipkow@31719
   823
wenzelm@44872
   824
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   825
    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   826
      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
wenzelm@44872
   827
         [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   828
  apply (induct set: finite)
nipkow@31719
   829
  apply auto
haftmann@60688
   830
  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
wenzelm@44872
   831
  done
nipkow@31719
   832
nipkow@31952
   833
lemma chinese_remainder_unique_nat:
wenzelm@44872
   834
  fixes A :: "'a set"
wenzelm@44872
   835
    and m :: "'a \<Rightarrow> nat"
wenzelm@44872
   836
    and u :: "'a \<Rightarrow> nat"
wenzelm@44872
   837
  assumes fin: "finite A"
wenzelm@44872
   838
    and nz: "ALL i:A. m i \<noteq> 0"
wenzelm@44872
   839
    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
nipkow@31719
   840
  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
nipkow@31719
   841
proof -
wenzelm@44872
   842
  from chinese_remainder_nat [OF fin cop]
wenzelm@44872
   843
  obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
nipkow@31719
   844
    by blast
nipkow@31719
   845
  let ?x = "y mod (PROD i:A. m i)"
nipkow@31719
   846
  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
nipkow@31719
   847
    by auto
wenzelm@44872
   848
  then have less: "?x < (PROD i:A. m i)"
nipkow@31719
   849
    by auto
nipkow@31719
   850
  have cong: "ALL i:A. [?x = u i] (mod m i)"
nipkow@31719
   851
    apply auto
nipkow@31952
   852
    apply (rule cong_trans_nat)
nipkow@31719
   853
    prefer 2
nipkow@31719
   854
    using one apply auto
nipkow@31952
   855
    apply (rule cong_dvd_modulus_nat)
nipkow@31952
   856
    apply (rule cong_mod_nat)
nipkow@31719
   857
    using prodnz apply auto
haftmann@59010
   858
    apply rule
nipkow@31719
   859
    apply (rule fin)
nipkow@31719
   860
    apply assumption
nipkow@31719
   861
    done
wenzelm@44872
   862
  have unique: "ALL z. z < (PROD i:A. m i) \<and>
nipkow@31719
   863
      (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
nipkow@31719
   864
  proof (clarify)
nipkow@31719
   865
    fix z
nipkow@31719
   866
    assume zless: "z < (PROD i:A. m i)"
nipkow@31719
   867
    assume zcong: "(ALL i:A. [z = u i] (mod m i))"
nipkow@31719
   868
    have "ALL i:A. [?x = z] (mod m i)"
wenzelm@44872
   869
      apply clarify
nipkow@31952
   870
      apply (rule cong_trans_nat)
nipkow@31719
   871
      using cong apply (erule bspec)
nipkow@31952
   872
      apply (rule cong_sym_nat)
nipkow@31719
   873
      using zcong apply auto
nipkow@31719
   874
      done
nipkow@31719
   875
    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
wenzelm@44872
   876
      apply (intro coprime_cong_prod_nat)
wenzelm@44872
   877
      apply auto
wenzelm@44872
   878
      done
nipkow@31719
   879
    with zless less show "z = ?x"
nipkow@31952
   880
      apply (intro cong_less_modulus_unique_nat)
nipkow@31952
   881
      apply (auto, erule cong_sym_nat)
nipkow@31719
   882
      done
wenzelm@44872
   883
  qed
wenzelm@44872
   884
  from less cong unique show ?thesis by blast
nipkow@31719
   885
qed
nipkow@31719
   886
nipkow@31719
   887
end