src/HOL/Number_Theory/Cong.thy
author wenzelm
Thu Jan 13 23:50:16 2011 +0100 (2011-01-13)
changeset 41541 1fa4725c4656
parent 37293 2c9ed7478e6e
child 41959 b460124855b8
permissions -rw-r--r--
eliminated global prems;
tuned proofs;
nipkow@31719
     1
(*  Title:      HOL/Library/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
nipkow@31719
    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
nipkow@31719
    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
nipkow@31719
    26
header {* Congruence *}
nipkow@31719
    27
nipkow@31719
    28
theory Cong
haftmann@37293
    29
imports Primes
nipkow@31719
    30
begin
nipkow@31719
    31
nipkow@31719
    32
subsection {* Turn off One_nat_def *}
nipkow@31719
    33
nipkow@31952
    34
lemma induct'_nat [case_names zero plus1, induct type: nat]: 
nipkow@31719
    35
    "\<lbrakk> P (0::nat); !!n. P n \<Longrightarrow> P (n + 1)\<rbrakk> \<Longrightarrow> P n"
nipkow@31719
    36
by (erule nat_induct) (simp add:One_nat_def)
nipkow@31719
    37
nipkow@31952
    38
lemma cases_nat [case_names zero plus1, cases type: nat]: 
nipkow@31719
    39
    "P (0::nat) \<Longrightarrow> (!!n. P (n + 1)) \<Longrightarrow> P n"
nipkow@31952
    40
by(metis induct'_nat)
nipkow@31719
    41
nipkow@31719
    42
lemma power_plus_one [simp]: "(x::'a::power)^(n + 1) = x * x^n"
nipkow@31719
    43
by (simp add: One_nat_def)
nipkow@31719
    44
nipkow@31952
    45
lemma power_eq_one_eq_nat [simp]: 
nipkow@31719
    46
  "((x::nat)^m = 1) = (m = 0 | x = 1)"
nipkow@31719
    47
by (induct m, auto)
nipkow@31719
    48
nipkow@31719
    49
lemma card_insert_if' [simp]: "finite A \<Longrightarrow>
nipkow@31719
    50
  card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
nipkow@31719
    51
by (auto simp add: insert_absorb)
nipkow@31719
    52
nipkow@31719
    53
lemma nat_1' [simp]: "nat 1 = 1"
nipkow@31719
    54
by simp
nipkow@31719
    55
nipkow@31792
    56
(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
nipkow@31719
    57
nipkow@31719
    58
declare nat_1 [simp del]
nipkow@31719
    59
declare add_2_eq_Suc [simp del] 
nipkow@31719
    60
declare add_2_eq_Suc' [simp del]
nipkow@31719
    61
nipkow@31719
    62
nipkow@31719
    63
declare mod_pos_pos_trivial [simp]
nipkow@31719
    64
nipkow@31719
    65
nipkow@31719
    66
subsection {* Main definitions *}
nipkow@31719
    67
nipkow@31719
    68
class cong =
nipkow@31719
    69
nipkow@31719
    70
fixes 
nipkow@31719
    71
  cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ = _] '(mod _'))")
nipkow@31719
    72
nipkow@31719
    73
begin
nipkow@31719
    74
nipkow@31719
    75
abbreviation
nipkow@31719
    76
  notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(1[_ \<noteq> _] '(mod _'))")
nipkow@31719
    77
where
nipkow@31719
    78
  "notcong x y m == (~cong x y m)" 
nipkow@31719
    79
nipkow@31719
    80
end
nipkow@31719
    81
nipkow@31719
    82
(* definitions for the natural numbers *)
nipkow@31719
    83
nipkow@31719
    84
instantiation nat :: cong
nipkow@31719
    85
nipkow@31719
    86
begin 
nipkow@31719
    87
nipkow@31719
    88
definition 
nipkow@31719
    89
  cong_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
nipkow@31719
    90
where 
nipkow@31719
    91
  "cong_nat x y m = ((x mod m) = (y mod m))"
nipkow@31719
    92
nipkow@31719
    93
instance proof qed
nipkow@31719
    94
nipkow@31719
    95
end
nipkow@31719
    96
nipkow@31719
    97
nipkow@31719
    98
(* definitions for the integers *)
nipkow@31719
    99
nipkow@31719
   100
instantiation int :: cong
nipkow@31719
   101
nipkow@31719
   102
begin 
nipkow@31719
   103
nipkow@31719
   104
definition 
nipkow@31719
   105
  cong_int :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool"
nipkow@31719
   106
where 
nipkow@31719
   107
  "cong_int x y m = ((x mod m) = (y mod m))"
nipkow@31719
   108
nipkow@31719
   109
instance proof qed
nipkow@31719
   110
nipkow@31719
   111
end
nipkow@31719
   112
nipkow@31719
   113
nipkow@31719
   114
subsection {* Set up Transfer *}
nipkow@31719
   115
nipkow@31719
   116
nipkow@31719
   117
lemma transfer_nat_int_cong:
nipkow@31719
   118
  "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> m >= 0 \<Longrightarrow> 
nipkow@31719
   119
    ([(nat x) = (nat y)] (mod (nat m))) = ([x = y] (mod m))"
nipkow@31719
   120
  unfolding cong_int_def cong_nat_def 
nipkow@31719
   121
  apply (auto simp add: nat_mod_distrib [symmetric])
nipkow@31719
   122
  apply (subst (asm) eq_nat_nat_iff)
nipkow@31719
   123
  apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
nipkow@31719
   124
  apply assumption
nipkow@31719
   125
done
nipkow@31719
   126
haftmann@35644
   127
declare transfer_morphism_nat_int[transfer add return: 
nipkow@31719
   128
    transfer_nat_int_cong]
nipkow@31719
   129
nipkow@31719
   130
lemma transfer_int_nat_cong:
nipkow@31719
   131
  "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
nipkow@31719
   132
  apply (auto simp add: cong_int_def cong_nat_def)
nipkow@31719
   133
  apply (auto simp add: zmod_int [symmetric])
nipkow@31719
   134
done
nipkow@31719
   135
haftmann@35644
   136
declare transfer_morphism_int_nat[transfer add return: 
nipkow@31719
   137
    transfer_int_nat_cong]
nipkow@31719
   138
nipkow@31719
   139
nipkow@31719
   140
subsection {* Congruence *}
nipkow@31719
   141
nipkow@31719
   142
(* was zcong_0, etc. *)
nipkow@31952
   143
lemma cong_0_nat [simp, presburger]: "([(a::nat) = b] (mod 0)) = (a = b)"
nipkow@31719
   144
  by (unfold cong_nat_def, auto)
nipkow@31719
   145
nipkow@31952
   146
lemma cong_0_int [simp, presburger]: "([(a::int) = b] (mod 0)) = (a = b)"
nipkow@31719
   147
  by (unfold cong_int_def, auto)
nipkow@31719
   148
nipkow@31952
   149
lemma cong_1_nat [simp, presburger]: "[(a::nat) = b] (mod 1)"
nipkow@31719
   150
  by (unfold cong_nat_def, auto)
nipkow@31719
   151
nipkow@31952
   152
lemma cong_Suc_0_nat [simp, presburger]: "[(a::nat) = b] (mod Suc 0)"
nipkow@31719
   153
  by (unfold cong_nat_def, auto simp add: One_nat_def)
nipkow@31719
   154
nipkow@31952
   155
lemma cong_1_int [simp, presburger]: "[(a::int) = b] (mod 1)"
nipkow@31719
   156
  by (unfold cong_int_def, auto)
nipkow@31719
   157
nipkow@31952
   158
lemma cong_refl_nat [simp]: "[(k::nat) = k] (mod m)"
nipkow@31719
   159
  by (unfold cong_nat_def, auto)
nipkow@31719
   160
nipkow@31952
   161
lemma cong_refl_int [simp]: "[(k::int) = k] (mod m)"
nipkow@31719
   162
  by (unfold cong_int_def, auto)
nipkow@31719
   163
nipkow@31952
   164
lemma cong_sym_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
nipkow@31719
   165
  by (unfold cong_nat_def, auto)
nipkow@31719
   166
nipkow@31952
   167
lemma cong_sym_int: "[(a::int) = b] (mod m) \<Longrightarrow> [b = a] (mod m)"
nipkow@31719
   168
  by (unfold cong_int_def, auto)
nipkow@31719
   169
nipkow@31952
   170
lemma cong_sym_eq_nat: "[(a::nat) = b] (mod m) = [b = a] (mod m)"
nipkow@31719
   171
  by (unfold cong_nat_def, auto)
nipkow@31719
   172
nipkow@31952
   173
lemma cong_sym_eq_int: "[(a::int) = b] (mod m) = [b = a] (mod m)"
nipkow@31719
   174
  by (unfold cong_int_def, auto)
nipkow@31719
   175
nipkow@31952
   176
lemma cong_trans_nat [trans]:
nipkow@31719
   177
    "[(a::nat) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
nipkow@31719
   178
  by (unfold cong_nat_def, auto)
nipkow@31719
   179
nipkow@31952
   180
lemma cong_trans_int [trans]:
nipkow@31719
   181
    "[(a::int) = b] (mod m) \<Longrightarrow> [b = c] (mod m) \<Longrightarrow> [a = c] (mod m)"
nipkow@31719
   182
  by (unfold cong_int_def, auto)
nipkow@31719
   183
nipkow@31952
   184
lemma cong_add_nat:
nipkow@31719
   185
    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
nipkow@31719
   186
  apply (unfold cong_nat_def)
nipkow@31719
   187
  apply (subst (1 2) mod_add_eq)
nipkow@31719
   188
  apply simp
nipkow@31719
   189
done
nipkow@31719
   190
nipkow@31952
   191
lemma cong_add_int:
nipkow@31719
   192
    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a + c = b + d] (mod m)"
nipkow@31719
   193
  apply (unfold cong_int_def)
nipkow@31719
   194
  apply (subst (1 2) mod_add_left_eq)
nipkow@31719
   195
  apply (subst (1 2) mod_add_right_eq)
nipkow@31719
   196
  apply simp
nipkow@31719
   197
done
nipkow@31719
   198
nipkow@31952
   199
lemma cong_diff_int:
nipkow@31719
   200
    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a - c = b - d] (mod m)"
nipkow@31719
   201
  apply (unfold cong_int_def)
nipkow@31719
   202
  apply (subst (1 2) mod_diff_eq)
nipkow@31719
   203
  apply simp
nipkow@31719
   204
done
nipkow@31719
   205
nipkow@31952
   206
lemma cong_diff_aux_int:
nipkow@31719
   207
  "(a::int) >= c \<Longrightarrow> b >= d \<Longrightarrow> [(a::int) = b] (mod m) \<Longrightarrow> 
nipkow@31719
   208
      [c = d] (mod m) \<Longrightarrow> [tsub a c = tsub b d] (mod m)"
nipkow@31719
   209
  apply (subst (1 2) tsub_eq)
nipkow@31952
   210
  apply (auto intro: cong_diff_int)
nipkow@31719
   211
done;
nipkow@31719
   212
nipkow@31952
   213
lemma cong_diff_nat:
nipkow@31719
   214
  assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
nipkow@31719
   215
    "[c = d] (mod m)"
nipkow@31719
   216
  shows "[a - c = b - d] (mod m)"
wenzelm@41541
   217
  using assms by (rule cong_diff_aux_int [transferred]);
nipkow@31719
   218
nipkow@31952
   219
lemma cong_mult_nat:
nipkow@31719
   220
    "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
nipkow@31719
   221
  apply (unfold cong_nat_def)
nipkow@31719
   222
  apply (subst (1 2) mod_mult_eq)
nipkow@31719
   223
  apply simp
nipkow@31719
   224
done
nipkow@31719
   225
nipkow@31952
   226
lemma cong_mult_int:
nipkow@31719
   227
    "[(a::int) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
nipkow@31719
   228
  apply (unfold cong_int_def)
nipkow@31719
   229
  apply (subst (1 2) zmod_zmult1_eq)
nipkow@31719
   230
  apply (subst (1 2) mult_commute)
nipkow@31719
   231
  apply (subst (1 2) zmod_zmult1_eq)
nipkow@31719
   232
  apply simp
nipkow@31719
   233
done
nipkow@31719
   234
nipkow@31952
   235
lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
nipkow@31719
   236
  apply (induct k)
wenzelm@41541
   237
  apply (auto simp add: cong_mult_nat)
wenzelm@41541
   238
  done
nipkow@31719
   239
nipkow@31952
   240
lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
nipkow@31719
   241
  apply (induct k)
wenzelm@41541
   242
  apply (auto simp add: cong_mult_int)
wenzelm@41541
   243
  done
nipkow@31719
   244
nipkow@31952
   245
lemma cong_setsum_nat [rule_format]: 
nipkow@31719
   246
    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
nipkow@31719
   247
      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
nipkow@31719
   248
  apply (case_tac "finite A")
nipkow@31719
   249
  apply (induct set: finite)
nipkow@31952
   250
  apply (auto intro: cong_add_nat)
nipkow@31719
   251
done
nipkow@31719
   252
nipkow@31952
   253
lemma cong_setsum_int [rule_format]:
nipkow@31719
   254
    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
nipkow@31719
   255
      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
nipkow@31719
   256
  apply (case_tac "finite A")
nipkow@31719
   257
  apply (induct set: finite)
nipkow@31952
   258
  apply (auto intro: cong_add_int)
nipkow@31719
   259
done
nipkow@31719
   260
nipkow@31952
   261
lemma cong_setprod_nat [rule_format]: 
nipkow@31719
   262
    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow> 
nipkow@31719
   263
      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
nipkow@31719
   264
  apply (case_tac "finite A")
nipkow@31719
   265
  apply (induct set: finite)
nipkow@31952
   266
  apply (auto intro: cong_mult_nat)
nipkow@31719
   267
done
nipkow@31719
   268
nipkow@31952
   269
lemma cong_setprod_int [rule_format]: 
nipkow@31719
   270
    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow> 
nipkow@31719
   271
      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
nipkow@31719
   272
  apply (case_tac "finite A")
nipkow@31719
   273
  apply (induct set: finite)
nipkow@31952
   274
  apply (auto intro: cong_mult_int)
nipkow@31719
   275
done
nipkow@31719
   276
nipkow@31952
   277
lemma cong_scalar_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
nipkow@31952
   278
  by (rule cong_mult_nat, simp_all)
nipkow@31719
   279
nipkow@31952
   280
lemma cong_scalar_int: "[(a::int)= b] (mod m) \<Longrightarrow> [a * k = b * k] (mod m)"
nipkow@31952
   281
  by (rule cong_mult_int, simp_all)
nipkow@31719
   282
nipkow@31952
   283
lemma cong_scalar2_nat: "[(a::nat)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
nipkow@31952
   284
  by (rule cong_mult_nat, simp_all)
nipkow@31719
   285
nipkow@31952
   286
lemma cong_scalar2_int: "[(a::int)= b] (mod m) \<Longrightarrow> [k * a = k * b] (mod m)"
nipkow@31952
   287
  by (rule cong_mult_int, simp_all)
nipkow@31719
   288
nipkow@31952
   289
lemma cong_mult_self_nat: "[(a::nat) * m = 0] (mod m)"
nipkow@31719
   290
  by (unfold cong_nat_def, auto)
nipkow@31719
   291
nipkow@31952
   292
lemma cong_mult_self_int: "[(a::int) * m = 0] (mod m)"
nipkow@31719
   293
  by (unfold cong_int_def, auto)
nipkow@31719
   294
nipkow@31952
   295
lemma cong_eq_diff_cong_0_int: "[(a::int) = b] (mod m) = [a - b = 0] (mod m)"
nipkow@31719
   296
  apply (rule iffI)
nipkow@31952
   297
  apply (erule cong_diff_int [of a b m b b, simplified])
nipkow@31952
   298
  apply (erule cong_add_int [of "a - b" 0 m b b, simplified])
nipkow@31719
   299
done
nipkow@31719
   300
nipkow@31952
   301
lemma cong_eq_diff_cong_0_aux_int: "a >= b \<Longrightarrow>
nipkow@31719
   302
    [(a::int) = b] (mod m) = [tsub a b = 0] (mod m)"
nipkow@31952
   303
  by (subst tsub_eq, assumption, rule cong_eq_diff_cong_0_int)
nipkow@31719
   304
nipkow@31952
   305
lemma cong_eq_diff_cong_0_nat:
nipkow@31719
   306
  assumes "(a::nat) >= b"
nipkow@31719
   307
  shows "[a = b] (mod m) = [a - b = 0] (mod m)"
wenzelm@41541
   308
  using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
nipkow@31719
   309
nipkow@31952
   310
lemma cong_diff_cong_0'_nat: 
nipkow@31719
   311
  "[(x::nat) = y] (mod n) \<longleftrightarrow> 
nipkow@31719
   312
    (if x <= y then [y - x = 0] (mod n) else [x - y = 0] (mod n))"
nipkow@31719
   313
  apply (case_tac "y <= x")
nipkow@31952
   314
  apply (frule cong_eq_diff_cong_0_nat [where m = n])
nipkow@31719
   315
  apply auto [1]
nipkow@31719
   316
  apply (subgoal_tac "x <= y")
nipkow@31952
   317
  apply (frule cong_eq_diff_cong_0_nat [where m = n])
nipkow@31952
   318
  apply (subst cong_sym_eq_nat)
nipkow@31719
   319
  apply auto
nipkow@31719
   320
done
nipkow@31719
   321
nipkow@31952
   322
lemma cong_altdef_nat: "(a::nat) >= b \<Longrightarrow> [a = b] (mod m) = (m dvd (a - b))"
nipkow@31952
   323
  apply (subst cong_eq_diff_cong_0_nat, assumption)
nipkow@31719
   324
  apply (unfold cong_nat_def)
nipkow@31719
   325
  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
nipkow@31719
   326
done
nipkow@31719
   327
nipkow@31952
   328
lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
nipkow@31952
   329
  apply (subst cong_eq_diff_cong_0_int)
nipkow@31719
   330
  apply (unfold cong_int_def)
nipkow@31719
   331
  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
nipkow@31719
   332
done
nipkow@31719
   333
nipkow@31952
   334
lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
nipkow@31952
   335
  by (simp add: cong_altdef_int)
nipkow@31719
   336
nipkow@31952
   337
lemma cong_square_int:
nipkow@31719
   338
   "\<lbrakk> prime (p::int); 0 < a; [a * a = 1] (mod p) \<rbrakk>
nipkow@31719
   339
    \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
nipkow@31952
   340
  apply (simp only: cong_altdef_int)
nipkow@31952
   341
  apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
nipkow@31719
   342
  (* any way around this? *)
nipkow@31719
   343
  apply (subgoal_tac "a * a - 1 = (a - 1) * (a - -1)")
haftmann@36350
   344
  apply (auto simp add: field_simps)
nipkow@31719
   345
done
nipkow@31719
   346
nipkow@31952
   347
lemma cong_mult_rcancel_int:
nipkow@31719
   348
  "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
nipkow@31952
   349
  apply (subst (1 2) cong_altdef_int)
nipkow@31719
   350
  apply (subst left_diff_distrib [symmetric])
nipkow@31952
   351
  apply (rule coprime_dvd_mult_iff_int)
nipkow@31952
   352
  apply (subst gcd_commute_int, assumption)
nipkow@31719
   353
done
nipkow@31719
   354
nipkow@31952
   355
lemma cong_mult_rcancel_nat:
nipkow@31719
   356
  assumes  "coprime k (m::nat)"
nipkow@31719
   357
  shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
nipkow@31952
   358
  apply (rule cong_mult_rcancel_int [transferred])
wenzelm@41541
   359
  using assms apply auto
nipkow@31719
   360
done
nipkow@31719
   361
nipkow@31952
   362
lemma cong_mult_lcancel_nat:
nipkow@31719
   363
  "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
nipkow@31952
   364
  by (simp add: mult_commute cong_mult_rcancel_nat)
nipkow@31719
   365
nipkow@31952
   366
lemma cong_mult_lcancel_int:
nipkow@31719
   367
  "coprime k (m::int) \<Longrightarrow> [k * a = k * b] (mod m) = [a = b] (mod m)"
nipkow@31952
   368
  by (simp add: mult_commute cong_mult_rcancel_int)
nipkow@31719
   369
nipkow@31719
   370
(* was zcong_zgcd_zmult_zmod *)
nipkow@31952
   371
lemma coprime_cong_mult_int:
nipkow@31719
   372
  "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
nipkow@31719
   373
    \<Longrightarrow> [a = b] (mod m * n)"
nipkow@31952
   374
  apply (simp only: cong_altdef_int)
nipkow@31952
   375
  apply (erule (2) divides_mult_int)
wenzelm@41541
   376
  done
nipkow@31719
   377
nipkow@31952
   378
lemma coprime_cong_mult_nat:
nipkow@31719
   379
  assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
nipkow@31719
   380
  shows "[a = b] (mod m * n)"
nipkow@31952
   381
  apply (rule coprime_cong_mult_int [transferred])
wenzelm@41541
   382
  using assms apply auto
wenzelm@41541
   383
  done
nipkow@31719
   384
nipkow@31952
   385
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
nipkow@31719
   386
    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
wenzelm@41541
   387
  by (auto simp add: cong_nat_def)
nipkow@31719
   388
nipkow@31952
   389
lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
nipkow@31719
   390
    a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
wenzelm@41541
   391
  by (auto simp add: cong_int_def)
nipkow@31719
   392
nipkow@31952
   393
lemma cong_less_unique_nat:
nipkow@31719
   394
    "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
nipkow@31719
   395
  apply auto
nipkow@31719
   396
  apply (rule_tac x = "a mod m" in exI)
nipkow@31719
   397
  apply (unfold cong_nat_def, auto)
nipkow@31719
   398
done
nipkow@31719
   399
nipkow@31952
   400
lemma cong_less_unique_int:
nipkow@31719
   401
    "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
nipkow@31719
   402
  apply auto
nipkow@31719
   403
  apply (rule_tac x = "a mod m" in exI)
wenzelm@41541
   404
  apply (unfold cong_int_def, auto)
wenzelm@41541
   405
  done
nipkow@31719
   406
nipkow@31952
   407
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
haftmann@36350
   408
  apply (auto simp add: cong_altdef_int dvd_def field_simps)
nipkow@31719
   409
  apply (rule_tac [!] x = "-k" in exI, auto)
nipkow@31719
   410
done
nipkow@31719
   411
nipkow@31952
   412
lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) = 
nipkow@31719
   413
    (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
nipkow@31719
   414
  apply (rule iffI)
nipkow@31719
   415
  apply (case_tac "b <= a")
nipkow@31952
   416
  apply (subst (asm) cong_altdef_nat, assumption)
nipkow@31719
   417
  apply (unfold dvd_def, auto)
nipkow@31719
   418
  apply (rule_tac x = k in exI)
nipkow@31719
   419
  apply (rule_tac x = 0 in exI)
haftmann@36350
   420
  apply (auto simp add: field_simps)
nipkow@31952
   421
  apply (subst (asm) cong_sym_eq_nat)
nipkow@31952
   422
  apply (subst (asm) cong_altdef_nat)
nipkow@31719
   423
  apply force
nipkow@31719
   424
  apply (unfold dvd_def, auto)
nipkow@31719
   425
  apply (rule_tac x = 0 in exI)
nipkow@31719
   426
  apply (rule_tac x = k in exI)
haftmann@36350
   427
  apply (auto simp add: field_simps)
nipkow@31719
   428
  apply (unfold cong_nat_def)
nipkow@31719
   429
  apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
nipkow@31719
   430
  apply (erule ssubst)back
nipkow@31719
   431
  apply (erule subst)
nipkow@31719
   432
  apply auto
nipkow@31719
   433
done
nipkow@31719
   434
nipkow@31952
   435
lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
nipkow@31952
   436
  apply (subst (asm) cong_iff_lin_int, auto)
nipkow@31719
   437
  apply (subst add_commute) 
nipkow@31952
   438
  apply (subst (2) gcd_commute_int)
nipkow@31719
   439
  apply (subst mult_commute)
nipkow@31952
   440
  apply (subst gcd_add_mult_int)
nipkow@31952
   441
  apply (rule gcd_commute_int)
wenzelm@41541
   442
  done
nipkow@31719
   443
nipkow@31952
   444
lemma cong_gcd_eq_nat: 
nipkow@31719
   445
  assumes "[(a::nat) = b] (mod m)"
nipkow@31719
   446
  shows "gcd a m = gcd b m"
nipkow@31952
   447
  apply (rule cong_gcd_eq_int [transferred])
wenzelm@41541
   448
  using assms apply auto
wenzelm@41541
   449
  done
nipkow@31719
   450
nipkow@31952
   451
lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
nipkow@31719
   452
    coprime b m"
nipkow@31952
   453
  by (auto simp add: cong_gcd_eq_nat)
nipkow@31719
   454
nipkow@31952
   455
lemma cong_imp_coprime_int: "[(a::int) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> 
nipkow@31719
   456
    coprime b m"
nipkow@31952
   457
  by (auto simp add: cong_gcd_eq_int)
nipkow@31719
   458
nipkow@31952
   459
lemma cong_cong_mod_nat: "[(a::nat) = b] (mod m) = 
nipkow@31719
   460
    [a mod m = b mod m] (mod m)"
nipkow@31719
   461
  by (auto simp add: cong_nat_def)
nipkow@31719
   462
nipkow@31952
   463
lemma cong_cong_mod_int: "[(a::int) = b] (mod m) = 
nipkow@31719
   464
    [a mod m = b mod m] (mod m)"
nipkow@31719
   465
  by (auto simp add: cong_int_def)
nipkow@31719
   466
nipkow@31952
   467
lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
nipkow@31952
   468
  by (subst (1 2) cong_altdef_int, auto)
nipkow@31719
   469
wenzelm@41541
   470
lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
wenzelm@41541
   471
  by auto
nipkow@31719
   472
wenzelm@41541
   473
lemma cong_zero_int: "[(a::int) = b] (mod 0) = (a = b)"
wenzelm@41541
   474
  by auto
nipkow@31719
   475
nipkow@31719
   476
(*
nipkow@31952
   477
lemma mod_dvd_mod_int:
nipkow@31719
   478
    "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
nipkow@31719
   479
  apply (unfold dvd_def, auto)
nipkow@31719
   480
  apply (rule mod_mod_cancel)
nipkow@31719
   481
  apply auto
nipkow@31719
   482
done
nipkow@31719
   483
nipkow@31719
   484
lemma mod_dvd_mod:
nipkow@31719
   485
  assumes "0 < (m::nat)" and "m dvd b"
nipkow@31719
   486
  shows "(a mod b mod m) = (a mod m)"
nipkow@31719
   487
nipkow@31952
   488
  apply (rule mod_dvd_mod_int [transferred])
wenzelm@41541
   489
  using assms apply auto
wenzelm@41541
   490
  done
nipkow@31719
   491
*)
nipkow@31719
   492
nipkow@31952
   493
lemma cong_add_lcancel_nat: 
nipkow@31719
   494
    "[(a::nat) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
nipkow@31952
   495
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   496
nipkow@31952
   497
lemma cong_add_lcancel_int: 
nipkow@31719
   498
    "[(a::int) + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)" 
nipkow@31952
   499
  by (simp add: cong_iff_lin_int)
nipkow@31719
   500
nipkow@31952
   501
lemma cong_add_rcancel_nat: "[(x::nat) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
nipkow@31952
   502
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   503
nipkow@31952
   504
lemma cong_add_rcancel_int: "[(x::int) + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
nipkow@31952
   505
  by (simp add: cong_iff_lin_int)
nipkow@31719
   506
nipkow@31952
   507
lemma cong_add_lcancel_0_nat: "[(a::nat) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
nipkow@31952
   508
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   509
nipkow@31952
   510
lemma cong_add_lcancel_0_int: "[(a::int) + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
nipkow@31952
   511
  by (simp add: cong_iff_lin_int)
nipkow@31719
   512
nipkow@31952
   513
lemma cong_add_rcancel_0_nat: "[x + (a::nat) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
nipkow@31952
   514
  by (simp add: cong_iff_lin_nat)
nipkow@31719
   515
nipkow@31952
   516
lemma cong_add_rcancel_0_int: "[x + (a::int) = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)" 
nipkow@31952
   517
  by (simp add: cong_iff_lin_int)
nipkow@31719
   518
nipkow@31952
   519
lemma cong_dvd_modulus_nat: "[(x::nat) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
nipkow@31719
   520
    [x = y] (mod n)"
nipkow@31952
   521
  apply (auto simp add: cong_iff_lin_nat dvd_def)
nipkow@31719
   522
  apply (rule_tac x="k1 * k" in exI)
nipkow@31719
   523
  apply (rule_tac x="k2 * k" in exI)
haftmann@36350
   524
  apply (simp add: field_simps)
nipkow@31719
   525
done
nipkow@31719
   526
nipkow@31952
   527
lemma cong_dvd_modulus_int: "[(x::int) = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> 
nipkow@31719
   528
    [x = y] (mod n)"
nipkow@31952
   529
  by (auto simp add: cong_altdef_int dvd_def)
nipkow@31719
   530
nipkow@31952
   531
lemma cong_dvd_eq_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
nipkow@31719
   532
  by (unfold cong_nat_def, auto simp add: dvd_eq_mod_eq_0)
nipkow@31719
   533
nipkow@31952
   534
lemma cong_dvd_eq_int: "[(x::int) = y] (mod n) \<Longrightarrow> n dvd x \<longleftrightarrow> n dvd y"
nipkow@31719
   535
  by (unfold cong_int_def, auto simp add: dvd_eq_mod_eq_0)
nipkow@31719
   536
nipkow@31952
   537
lemma cong_mod_nat: "(n::nat) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
nipkow@31719
   538
  by (simp add: cong_nat_def)
nipkow@31719
   539
nipkow@31952
   540
lemma cong_mod_int: "(n::int) ~= 0 \<Longrightarrow> [a mod n = a] (mod n)" 
nipkow@31719
   541
  by (simp add: cong_int_def)
nipkow@31719
   542
nipkow@31952
   543
lemma mod_mult_cong_nat: "(a::nat) ~= 0 \<Longrightarrow> b ~= 0 
nipkow@31719
   544
    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
nipkow@31719
   545
  by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
nipkow@31719
   546
nipkow@31952
   547
lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
nipkow@31952
   548
  apply (simp add: cong_altdef_int)
nipkow@31719
   549
  apply (subst dvd_minus_iff [symmetric])
haftmann@36350
   550
  apply (simp add: field_simps)
nipkow@31719
   551
done
nipkow@31719
   552
nipkow@31952
   553
lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
nipkow@31952
   554
  by (auto simp add: cong_altdef_int)
nipkow@31719
   555
nipkow@31952
   556
lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0 
nipkow@31719
   557
    \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
nipkow@31719
   558
  apply (case_tac "b > 0")
nipkow@31719
   559
  apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
nipkow@31952
   560
  apply (subst (1 2) cong_modulus_neg_int)
nipkow@31719
   561
  apply (unfold cong_int_def)
nipkow@31719
   562
  apply (subgoal_tac "a * b = (-a * -b)")
nipkow@31719
   563
  apply (erule ssubst)
nipkow@31719
   564
  apply (subst zmod_zmult2_eq)
nipkow@31719
   565
  apply (auto simp add: mod_add_left_eq) 
nipkow@31719
   566
done
nipkow@31719
   567
nipkow@31952
   568
lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
nipkow@31719
   569
  apply (case_tac "a = 0")
nipkow@31719
   570
  apply force
nipkow@31952
   571
  apply (subst (asm) cong_altdef_nat)
nipkow@31719
   572
  apply auto
nipkow@31719
   573
done
nipkow@31719
   574
nipkow@31952
   575
lemma cong_0_1_nat: "[(0::nat) = 1] (mod n) = (n = 1)"
nipkow@31719
   576
  by (unfold cong_nat_def, auto)
nipkow@31719
   577
nipkow@31952
   578
lemma cong_0_1_int: "[(0::int) = 1] (mod n) = ((n = 1) | (n = -1))"
nipkow@31719
   579
  by (unfold cong_int_def, auto simp add: zmult_eq_1_iff)
nipkow@31719
   580
nipkow@31952
   581
lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow> 
nipkow@31719
   582
    a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
nipkow@31719
   583
  apply (case_tac "n = 1")
nipkow@31719
   584
  apply auto [1]
nipkow@31719
   585
  apply (drule_tac x = "a - 1" in spec)
nipkow@31719
   586
  apply force
nipkow@31719
   587
  apply (case_tac "a = 0")
nipkow@31952
   588
  apply (auto simp add: cong_0_1_nat) [1]
nipkow@31719
   589
  apply (rule iffI)
nipkow@31952
   590
  apply (drule cong_to_1_nat)
nipkow@31719
   591
  apply (unfold dvd_def)
nipkow@31719
   592
  apply auto [1]
nipkow@31719
   593
  apply (rule_tac x = k in exI)
haftmann@36350
   594
  apply (auto simp add: field_simps) [1]
nipkow@31952
   595
  apply (subst cong_altdef_nat)
nipkow@31719
   596
  apply (auto simp add: dvd_def)
nipkow@31719
   597
done
nipkow@31719
   598
nipkow@31952
   599
lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
nipkow@31952
   600
  apply (subst cong_altdef_nat)
nipkow@31719
   601
  apply assumption
haftmann@36350
   602
  apply (unfold dvd_def, auto simp add: field_simps)
nipkow@31719
   603
  apply (rule_tac x = k in exI)
nipkow@31719
   604
  apply auto
nipkow@31719
   605
done
nipkow@31719
   606
nipkow@31952
   607
lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
nipkow@31719
   608
  apply (case_tac "n = 0")
nipkow@31719
   609
  apply force
nipkow@31952
   610
  apply (frule bezout_nat [of a n], auto)
nipkow@31719
   611
  apply (rule exI, erule ssubst)
nipkow@31952
   612
  apply (rule cong_trans_nat)
nipkow@31952
   613
  apply (rule cong_add_nat)
nipkow@31719
   614
  apply (subst mult_commute)
nipkow@31952
   615
  apply (rule cong_mult_self_nat)
nipkow@31719
   616
  prefer 2
nipkow@31719
   617
  apply simp
nipkow@31952
   618
  apply (rule cong_refl_nat)
nipkow@31952
   619
  apply (rule cong_refl_nat)
nipkow@31719
   620
done
nipkow@31719
   621
nipkow@31952
   622
lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
nipkow@31719
   623
  apply (case_tac "n = 0")
nipkow@31719
   624
  apply (case_tac "a \<ge> 0")
nipkow@31719
   625
  apply auto
nipkow@31719
   626
  apply (rule_tac x = "-1" in exI)
nipkow@31719
   627
  apply auto
nipkow@31952
   628
  apply (insert bezout_int [of a n], auto)
nipkow@31719
   629
  apply (rule exI)
nipkow@31719
   630
  apply (erule subst)
nipkow@31952
   631
  apply (rule cong_trans_int)
nipkow@31719
   632
  prefer 2
nipkow@31952
   633
  apply (rule cong_add_int)
nipkow@31952
   634
  apply (rule cong_refl_int)
nipkow@31952
   635
  apply (rule cong_sym_int)
nipkow@31952
   636
  apply (rule cong_mult_self_int)
nipkow@31719
   637
  apply simp
nipkow@31719
   638
  apply (subst mult_commute)
nipkow@31952
   639
  apply (rule cong_refl_int)
nipkow@31719
   640
done
nipkow@31719
   641
  
nipkow@31952
   642
lemma cong_solve_dvd_nat: 
nipkow@31719
   643
  assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
nipkow@31719
   644
  shows "EX x. [a * x = d] (mod n)"
nipkow@31719
   645
proof -
nipkow@31952
   646
  from cong_solve_nat [OF a] obtain x where 
nipkow@31719
   647
      "[a * x = gcd a n](mod n)"
nipkow@31719
   648
    by auto
nipkow@31719
   649
  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
nipkow@31952
   650
    by (elim cong_scalar2_nat)
nipkow@31719
   651
  also from b have "(d div gcd a n) * gcd a n = d"
nipkow@31719
   652
    by (rule dvd_div_mult_self)
nipkow@31719
   653
  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
nipkow@31719
   654
    by auto
nipkow@31719
   655
  finally show ?thesis
nipkow@31719
   656
    by auto
nipkow@31719
   657
qed
nipkow@31719
   658
nipkow@31952
   659
lemma cong_solve_dvd_int: 
nipkow@31719
   660
  assumes a: "(a::int) \<noteq> 0" and b: "gcd a n dvd d"
nipkow@31719
   661
  shows "EX x. [a * x = d] (mod n)"
nipkow@31719
   662
proof -
nipkow@31952
   663
  from cong_solve_int [OF a] obtain x where 
nipkow@31719
   664
      "[a * x = gcd a n](mod n)"
nipkow@31719
   665
    by auto
nipkow@31719
   666
  hence "[(d div gcd a n) * (a * x) = (d div gcd a n) * gcd a n] (mod n)" 
nipkow@31952
   667
    by (elim cong_scalar2_int)
nipkow@31719
   668
  also from b have "(d div gcd a n) * gcd a n = d"
nipkow@31719
   669
    by (rule dvd_div_mult_self)
nipkow@31719
   670
  also have "(d div gcd a n) * (a * x) = a * (d div gcd a n * x)"
nipkow@31719
   671
    by auto
nipkow@31719
   672
  finally show ?thesis
nipkow@31719
   673
    by auto
nipkow@31719
   674
qed
nipkow@31719
   675
nipkow@31952
   676
lemma cong_solve_coprime_nat: "coprime (a::nat) n \<Longrightarrow> 
nipkow@31719
   677
    EX x. [a * x = 1] (mod n)"
nipkow@31719
   678
  apply (case_tac "a = 0")
nipkow@31719
   679
  apply force
nipkow@31952
   680
  apply (frule cong_solve_nat [of a n])
nipkow@31719
   681
  apply auto
nipkow@31719
   682
done
nipkow@31719
   683
nipkow@31952
   684
lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> 
nipkow@31719
   685
    EX x. [a * x = 1] (mod n)"
nipkow@31719
   686
  apply (case_tac "a = 0")
nipkow@31719
   687
  apply auto
nipkow@31719
   688
  apply (case_tac "n \<ge> 0")
nipkow@31719
   689
  apply auto
nipkow@31719
   690
  apply (subst cong_int_def, auto)
nipkow@31952
   691
  apply (frule cong_solve_int [of a n])
nipkow@31719
   692
  apply auto
nipkow@31719
   693
done
nipkow@31719
   694
nipkow@31952
   695
lemma coprime_iff_invertible_nat: "m > (1::nat) \<Longrightarrow> coprime a m = 
nipkow@31719
   696
    (EX x. [a * x = 1] (mod m))"
nipkow@31952
   697
  apply (auto intro: cong_solve_coprime_nat)
nipkow@31952
   698
  apply (unfold cong_nat_def, auto intro: invertible_coprime_nat)
nipkow@31719
   699
done
nipkow@31719
   700
nipkow@31952
   701
lemma coprime_iff_invertible_int: "m > (1::int) \<Longrightarrow> coprime a m = 
nipkow@31719
   702
    (EX x. [a * x = 1] (mod m))"
nipkow@31952
   703
  apply (auto intro: cong_solve_coprime_int)
nipkow@31719
   704
  apply (unfold cong_int_def)
nipkow@31952
   705
  apply (auto intro: invertible_coprime_int)
nipkow@31719
   706
done
nipkow@31719
   707
nipkow@31952
   708
lemma coprime_iff_invertible'_int: "m > (1::int) \<Longrightarrow> coprime a m = 
nipkow@31719
   709
    (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
nipkow@31952
   710
  apply (subst coprime_iff_invertible_int)
nipkow@31719
   711
  apply auto
nipkow@31719
   712
  apply (auto simp add: cong_int_def)
nipkow@31719
   713
  apply (rule_tac x = "x mod m" in exI)
nipkow@31719
   714
  apply (auto simp add: mod_mult_right_eq [symmetric])
nipkow@31719
   715
done
nipkow@31719
   716
nipkow@31719
   717
nipkow@31952
   718
lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
nipkow@31719
   719
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
nipkow@31719
   720
  apply (case_tac "y \<le> x")
nipkow@31952
   721
  apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
nipkow@31952
   722
  apply (rule cong_sym_nat)
nipkow@31952
   723
  apply (subst (asm) (1 2) cong_sym_eq_nat)
nipkow@31952
   724
  apply (auto simp add: cong_altdef_nat lcm_least_nat)
nipkow@31719
   725
done
nipkow@31719
   726
nipkow@31952
   727
lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
nipkow@31719
   728
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
nipkow@31952
   729
  by (auto simp add: cong_altdef_int lcm_least_int) [1]
nipkow@31719
   730
nipkow@31952
   731
lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
nipkow@31719
   732
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
nipkow@31952
   733
  apply (frule (1) cong_cong_lcm_nat)back
nipkow@31719
   734
  apply (simp add: lcm_nat_def)
nipkow@31719
   735
done
nipkow@31719
   736
nipkow@31952
   737
lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
nipkow@31719
   738
    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
nipkow@31952
   739
  apply (frule (1) cong_cong_lcm_int)back
nipkow@31952
   740
  apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
nipkow@31719
   741
done
nipkow@31719
   742
nipkow@31952
   743
lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   744
    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   745
    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
nipkow@31719
   746
      [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   747
  apply (induct set: finite)
nipkow@31719
   748
  apply auto
nipkow@31952
   749
  apply (rule cong_cong_coprime_nat)
nipkow@31952
   750
  apply (subst gcd_commute_nat)
nipkow@31952
   751
  apply (rule setprod_coprime_nat)
nipkow@31719
   752
  apply auto
nipkow@31719
   753
done
nipkow@31719
   754
nipkow@31952
   755
lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
nipkow@31719
   756
    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
   757
    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
nipkow@31719
   758
      [x = y] (mod (PROD i:A. m i))"
nipkow@31719
   759
  apply (induct set: finite)
nipkow@31719
   760
  apply auto
nipkow@31952
   761
  apply (rule cong_cong_coprime_int)
nipkow@31952
   762
  apply (subst gcd_commute_int)
nipkow@31952
   763
  apply (rule setprod_coprime_int)
nipkow@31719
   764
  apply auto
nipkow@31719
   765
done
nipkow@31719
   766
nipkow@31952
   767
lemma binary_chinese_remainder_aux_nat: 
nipkow@31719
   768
  assumes a: "coprime (m1::nat) m2"
nipkow@31719
   769
  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
nipkow@31719
   770
    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
nipkow@31719
   771
proof -
nipkow@31952
   772
  from cong_solve_coprime_nat [OF a]
nipkow@31719
   773
      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
nipkow@31719
   774
    by auto
nipkow@31719
   775
  from a have b: "coprime m2 m1" 
nipkow@31952
   776
    by (subst gcd_commute_nat)
nipkow@31952
   777
  from cong_solve_coprime_nat [OF b]
nipkow@31719
   778
      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
nipkow@31719
   779
    by auto
nipkow@31719
   780
  have "[m1 * x1 = 0] (mod m1)"
nipkow@31952
   781
    by (subst mult_commute, rule cong_mult_self_nat)
nipkow@31719
   782
  moreover have "[m2 * x2 = 0] (mod m2)"
nipkow@31952
   783
    by (subst mult_commute, rule cong_mult_self_nat)
nipkow@31719
   784
  moreover note one two
nipkow@31719
   785
  ultimately show ?thesis by blast
nipkow@31719
   786
qed
nipkow@31719
   787
nipkow@31952
   788
lemma binary_chinese_remainder_aux_int: 
nipkow@31719
   789
  assumes a: "coprime (m1::int) m2"
nipkow@31719
   790
  shows "EX b1 b2. [b1 = 1] (mod m1) \<and> [b1 = 0] (mod m2) \<and>
nipkow@31719
   791
    [b2 = 0] (mod m1) \<and> [b2 = 1] (mod m2)"
nipkow@31719
   792
proof -
nipkow@31952
   793
  from cong_solve_coprime_int [OF a]
nipkow@31719
   794
      obtain x1 where one: "[m1 * x1 = 1] (mod m2)"
nipkow@31719
   795
    by auto
nipkow@31719
   796
  from a have b: "coprime m2 m1" 
nipkow@31952
   797
    by (subst gcd_commute_int)
nipkow@31952
   798
  from cong_solve_coprime_int [OF b]
nipkow@31719
   799
      obtain x2 where two: "[m2 * x2 = 1] (mod m1)"
nipkow@31719
   800
    by auto
nipkow@31719
   801
  have "[m1 * x1 = 0] (mod m1)"
nipkow@31952
   802
    by (subst mult_commute, rule cong_mult_self_int)
nipkow@31719
   803
  moreover have "[m2 * x2 = 0] (mod m2)"
nipkow@31952
   804
    by (subst mult_commute, rule cong_mult_self_int)
nipkow@31719
   805
  moreover note one two
nipkow@31719
   806
  ultimately show ?thesis by blast
nipkow@31719
   807
qed
nipkow@31719
   808
nipkow@31952
   809
lemma binary_chinese_remainder_nat:
nipkow@31719
   810
  assumes a: "coprime (m1::nat) m2"
nipkow@31719
   811
  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   812
proof -
nipkow@31952
   813
  from binary_chinese_remainder_aux_nat [OF a] obtain b1 b2
nipkow@31719
   814
    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
nipkow@31719
   815
          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
nipkow@31719
   816
    by blast
nipkow@31719
   817
  let ?x = "u1 * b1 + u2 * b2"
nipkow@31719
   818
  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
nipkow@31952
   819
    apply (rule cong_add_nat)
nipkow@31952
   820
    apply (rule cong_scalar2_nat)
nipkow@31719
   821
    apply (rule `[b1 = 1] (mod m1)`)
nipkow@31952
   822
    apply (rule cong_scalar2_nat)
nipkow@31719
   823
    apply (rule `[b2 = 0] (mod m1)`)
nipkow@31719
   824
    done
nipkow@31719
   825
  hence "[?x = u1] (mod m1)" by simp
nipkow@31719
   826
  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
nipkow@31952
   827
    apply (rule cong_add_nat)
nipkow@31952
   828
    apply (rule cong_scalar2_nat)
nipkow@31719
   829
    apply (rule `[b1 = 0] (mod m2)`)
nipkow@31952
   830
    apply (rule cong_scalar2_nat)
nipkow@31719
   831
    apply (rule `[b2 = 1] (mod m2)`)
nipkow@31719
   832
    done
nipkow@31719
   833
  hence "[?x = u2] (mod m2)" by simp
nipkow@31719
   834
  with `[?x = u1] (mod m1)` show ?thesis by blast
nipkow@31719
   835
qed
nipkow@31719
   836
nipkow@31952
   837
lemma binary_chinese_remainder_int:
nipkow@31719
   838
  assumes a: "coprime (m1::int) m2"
nipkow@31719
   839
  shows "EX x. [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   840
proof -
nipkow@31952
   841
  from binary_chinese_remainder_aux_int [OF a] obtain b1 b2
nipkow@31719
   842
    where "[b1 = 1] (mod m1)" and "[b1 = 0] (mod m2)" and
nipkow@31719
   843
          "[b2 = 0] (mod m1)" and "[b2 = 1] (mod m2)"
nipkow@31719
   844
    by blast
nipkow@31719
   845
  let ?x = "u1 * b1 + u2 * b2"
nipkow@31719
   846
  have "[?x = u1 * 1 + u2 * 0] (mod m1)"
nipkow@31952
   847
    apply (rule cong_add_int)
nipkow@31952
   848
    apply (rule cong_scalar2_int)
nipkow@31719
   849
    apply (rule `[b1 = 1] (mod m1)`)
nipkow@31952
   850
    apply (rule cong_scalar2_int)
nipkow@31719
   851
    apply (rule `[b2 = 0] (mod m1)`)
nipkow@31719
   852
    done
nipkow@31719
   853
  hence "[?x = u1] (mod m1)" by simp
nipkow@31719
   854
  have "[?x = u1 * 0 + u2 * 1] (mod m2)"
nipkow@31952
   855
    apply (rule cong_add_int)
nipkow@31952
   856
    apply (rule cong_scalar2_int)
nipkow@31719
   857
    apply (rule `[b1 = 0] (mod m2)`)
nipkow@31952
   858
    apply (rule cong_scalar2_int)
nipkow@31719
   859
    apply (rule `[b2 = 1] (mod m2)`)
nipkow@31719
   860
    done
nipkow@31719
   861
  hence "[?x = u2] (mod m2)" by simp
nipkow@31719
   862
  with `[?x = u1] (mod m1)` show ?thesis by blast
nipkow@31719
   863
qed
nipkow@31719
   864
nipkow@31952
   865
lemma cong_modulus_mult_nat: "[(x::nat) = y] (mod m * n) \<Longrightarrow> 
nipkow@31719
   866
    [x = y] (mod m)"
nipkow@31719
   867
  apply (case_tac "y \<le> x")
nipkow@31952
   868
  apply (simp add: cong_altdef_nat)
nipkow@31719
   869
  apply (erule dvd_mult_left)
nipkow@31952
   870
  apply (rule cong_sym_nat)
nipkow@31952
   871
  apply (subst (asm) cong_sym_eq_nat)
nipkow@31952
   872
  apply (simp add: cong_altdef_nat) 
nipkow@31719
   873
  apply (erule dvd_mult_left)
nipkow@31719
   874
done
nipkow@31719
   875
nipkow@31952
   876
lemma cong_modulus_mult_int: "[(x::int) = y] (mod m * n) \<Longrightarrow> 
nipkow@31719
   877
    [x = y] (mod m)"
nipkow@31952
   878
  apply (simp add: cong_altdef_int) 
nipkow@31719
   879
  apply (erule dvd_mult_left)
nipkow@31719
   880
done
nipkow@31719
   881
nipkow@31952
   882
lemma cong_less_modulus_unique_nat: 
nipkow@31719
   883
    "[(x::nat) = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
nipkow@31719
   884
  by (simp add: cong_nat_def)
nipkow@31719
   885
nipkow@31952
   886
lemma binary_chinese_remainder_unique_nat:
nipkow@31719
   887
  assumes a: "coprime (m1::nat) m2" and
nipkow@31719
   888
         nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
nipkow@31719
   889
  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
nipkow@31719
   890
proof -
nipkow@31952
   891
  from binary_chinese_remainder_nat [OF a] obtain y where 
nipkow@31719
   892
      "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
nipkow@31719
   893
    by blast
nipkow@31719
   894
  let ?x = "y mod (m1 * m2)"
nipkow@31719
   895
  from nz have less: "?x < m1 * m2"
nipkow@31719
   896
    by auto   
nipkow@31719
   897
  have one: "[?x = u1] (mod m1)"
nipkow@31952
   898
    apply (rule cong_trans_nat)
nipkow@31719
   899
    prefer 2
nipkow@31719
   900
    apply (rule `[y = u1] (mod m1)`)
nipkow@31952
   901
    apply (rule cong_modulus_mult_nat)
nipkow@31952
   902
    apply (rule cong_mod_nat)
nipkow@31719
   903
    using nz apply auto
nipkow@31719
   904
    done
nipkow@31719
   905
  have two: "[?x = u2] (mod m2)"
nipkow@31952
   906
    apply (rule cong_trans_nat)
nipkow@31719
   907
    prefer 2
nipkow@31719
   908
    apply (rule `[y = u2] (mod m2)`)
nipkow@31719
   909
    apply (subst mult_commute)
nipkow@31952
   910
    apply (rule cong_modulus_mult_nat)
nipkow@31952
   911
    apply (rule cong_mod_nat)
nipkow@31719
   912
    using nz apply auto
nipkow@31719
   913
    done
nipkow@31719
   914
  have "ALL z. z < m1 * m2 \<and> [z = u1] (mod m1) \<and> [z = u2] (mod m2) \<longrightarrow>
nipkow@31719
   915
      z = ?x"
nipkow@31719
   916
  proof (clarify)
nipkow@31719
   917
    fix z
nipkow@31719
   918
    assume "z < m1 * m2"
nipkow@31719
   919
    assume "[z = u1] (mod m1)" and  "[z = u2] (mod m2)"
nipkow@31719
   920
    have "[?x = z] (mod m1)"
nipkow@31952
   921
      apply (rule cong_trans_nat)
nipkow@31719
   922
      apply (rule `[?x = u1] (mod m1)`)
nipkow@31952
   923
      apply (rule cong_sym_nat)
nipkow@31719
   924
      apply (rule `[z = u1] (mod m1)`)
nipkow@31719
   925
      done
nipkow@31719
   926
    moreover have "[?x = z] (mod m2)"
nipkow@31952
   927
      apply (rule cong_trans_nat)
nipkow@31719
   928
      apply (rule `[?x = u2] (mod m2)`)
nipkow@31952
   929
      apply (rule cong_sym_nat)
nipkow@31719
   930
      apply (rule `[z = u2] (mod m2)`)
nipkow@31719
   931
      done
nipkow@31719
   932
    ultimately have "[?x = z] (mod m1 * m2)"
nipkow@31952
   933
      by (auto intro: coprime_cong_mult_nat a)
nipkow@31719
   934
    with `z < m1 * m2` `?x < m1 * m2` show "z = ?x"
nipkow@31952
   935
      apply (intro cong_less_modulus_unique_nat)
nipkow@31952
   936
      apply (auto, erule cong_sym_nat)
nipkow@31719
   937
      done
nipkow@31719
   938
  qed  
nipkow@31719
   939
  with less one two show ?thesis
nipkow@31719
   940
    by auto
nipkow@31719
   941
 qed
nipkow@31719
   942
nipkow@31952
   943
lemma chinese_remainder_aux_nat:
nipkow@31719
   944
  fixes A :: "'a set" and
nipkow@31719
   945
        m :: "'a \<Rightarrow> nat"
nipkow@31719
   946
  assumes fin: "finite A" and
nipkow@31719
   947
          cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
nipkow@31719
   948
  shows "EX b. (ALL i : A. 
nipkow@31719
   949
      [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
nipkow@31719
   950
proof (rule finite_set_choice, rule fin, rule ballI)
nipkow@31719
   951
  fix i
nipkow@31719
   952
  assume "i : A"
nipkow@31719
   953
  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
nipkow@31952
   954
    by (intro setprod_coprime_nat, auto)
nipkow@31719
   955
  hence "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
nipkow@31952
   956
    by (elim cong_solve_coprime_nat)
nipkow@31719
   957
  then obtain x where "[(PROD j : A - {i}. m j) * x = 1] (mod m i)"
nipkow@31719
   958
    by auto
nipkow@31719
   959
  moreover have "[(PROD j : A - {i}. m j) * x = 0] 
nipkow@31719
   960
    (mod (PROD j : A - {i}. m j))"
nipkow@31952
   961
    by (subst mult_commute, rule cong_mult_self_nat)
nipkow@31719
   962
  ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0] 
nipkow@31719
   963
      (mod setprod m (A - {i}))"
nipkow@31719
   964
    by blast
nipkow@31719
   965
qed
nipkow@31719
   966
nipkow@31952
   967
lemma chinese_remainder_nat:
nipkow@31719
   968
  fixes A :: "'a set" and
nipkow@31719
   969
        m :: "'a \<Rightarrow> nat" and
nipkow@31719
   970
        u :: "'a \<Rightarrow> nat"
nipkow@31719
   971
  assumes 
nipkow@31719
   972
        fin: "finite A" and
nipkow@31719
   973
        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
nipkow@31719
   974
  shows "EX x. (ALL i:A. [x = u i] (mod m i))"
nipkow@31719
   975
proof -
nipkow@31952
   976
  from chinese_remainder_aux_nat [OF fin cop] obtain b where
nipkow@31719
   977
    bprop: "ALL i:A. [b i = 1] (mod m i) \<and> 
nipkow@31719
   978
      [b i = 0] (mod (PROD j : A - {i}. m j))"
nipkow@31719
   979
    by blast
nipkow@31719
   980
  let ?x = "SUM i:A. (u i) * (b i)"
nipkow@31719
   981
  show "?thesis"
nipkow@31719
   982
  proof (rule exI, clarify)
nipkow@31719
   983
    fix i
nipkow@31719
   984
    assume a: "i : A"
nipkow@31719
   985
    show "[?x = u i] (mod m i)" 
nipkow@31719
   986
    proof -
nipkow@31719
   987
      from fin a have "?x = (SUM j:{i}. u j * b j) + 
nipkow@31719
   988
          (SUM j:A-{i}. u j * b j)"
nipkow@31719
   989
        by (subst setsum_Un_disjoint [symmetric], auto intro: setsum_cong)
nipkow@31719
   990
      hence "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
nipkow@31719
   991
        by auto
nipkow@31719
   992
      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
nipkow@31719
   993
                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
nipkow@31952
   994
        apply (rule cong_add_nat)
nipkow@31952
   995
        apply (rule cong_scalar2_nat)
nipkow@31719
   996
        using bprop a apply blast
nipkow@31952
   997
        apply (rule cong_setsum_nat)
nipkow@31952
   998
        apply (rule cong_scalar2_nat)
nipkow@31719
   999
        using bprop apply auto
nipkow@31952
  1000
        apply (rule cong_dvd_modulus_nat)
nipkow@31719
  1001
        apply (drule (1) bspec)
nipkow@31719
  1002
        apply (erule conjE)
nipkow@31719
  1003
        apply assumption
nipkow@31719
  1004
        apply (rule dvd_setprod)
nipkow@31719
  1005
        using fin a apply auto
nipkow@31719
  1006
        done
nipkow@31719
  1007
      finally show ?thesis
nipkow@31719
  1008
        by simp
nipkow@31719
  1009
    qed
nipkow@31719
  1010
  qed
nipkow@31719
  1011
qed
nipkow@31719
  1012
nipkow@31952
  1013
lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow> 
nipkow@31719
  1014
    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
nipkow@31719
  1015
      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
nipkow@31719
  1016
         [x = y] (mod (PROD i:A. m i))" 
nipkow@31719
  1017
  apply (induct set: finite)
nipkow@31719
  1018
  apply auto
nipkow@31952
  1019
  apply (erule (1) coprime_cong_mult_nat)
nipkow@31952
  1020
  apply (subst gcd_commute_nat)
nipkow@31952
  1021
  apply (rule setprod_coprime_nat)
nipkow@31719
  1022
  apply auto
nipkow@31719
  1023
done
nipkow@31719
  1024
nipkow@31952
  1025
lemma chinese_remainder_unique_nat:
nipkow@31719
  1026
  fixes A :: "'a set" and
nipkow@31719
  1027
        m :: "'a \<Rightarrow> nat" and
nipkow@31719
  1028
        u :: "'a \<Rightarrow> nat"
nipkow@31719
  1029
  assumes 
nipkow@31719
  1030
        fin: "finite A" and
nipkow@31719
  1031
         nz: "ALL i:A. m i \<noteq> 0" and
nipkow@31719
  1032
        cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
nipkow@31719
  1033
  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
nipkow@31719
  1034
proof -
nipkow@31952
  1035
  from chinese_remainder_nat [OF fin cop] obtain y where
nipkow@31719
  1036
      one: "(ALL i:A. [y = u i] (mod m i))" 
nipkow@31719
  1037
    by blast
nipkow@31719
  1038
  let ?x = "y mod (PROD i:A. m i)"
nipkow@31719
  1039
  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
nipkow@31719
  1040
    by auto
nipkow@31719
  1041
  hence less: "?x < (PROD i:A. m i)"
nipkow@31719
  1042
    by auto
nipkow@31719
  1043
  have cong: "ALL i:A. [?x = u i] (mod m i)"
nipkow@31719
  1044
    apply auto
nipkow@31952
  1045
    apply (rule cong_trans_nat)
nipkow@31719
  1046
    prefer 2
nipkow@31719
  1047
    using one apply auto
nipkow@31952
  1048
    apply (rule cong_dvd_modulus_nat)
nipkow@31952
  1049
    apply (rule cong_mod_nat)
nipkow@31719
  1050
    using prodnz apply auto
nipkow@31719
  1051
    apply (rule dvd_setprod)
nipkow@31719
  1052
    apply (rule fin)
nipkow@31719
  1053
    apply assumption
nipkow@31719
  1054
    done
nipkow@31719
  1055
  have unique: "ALL z. z < (PROD i:A. m i) \<and> 
nipkow@31719
  1056
      (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
nipkow@31719
  1057
  proof (clarify)
nipkow@31719
  1058
    fix z
nipkow@31719
  1059
    assume zless: "z < (PROD i:A. m i)"
nipkow@31719
  1060
    assume zcong: "(ALL i:A. [z = u i] (mod m i))"
nipkow@31719
  1061
    have "ALL i:A. [?x = z] (mod m i)"
nipkow@31719
  1062
      apply clarify     
nipkow@31952
  1063
      apply (rule cong_trans_nat)
nipkow@31719
  1064
      using cong apply (erule bspec)
nipkow@31952
  1065
      apply (rule cong_sym_nat)
nipkow@31719
  1066
      using zcong apply auto
nipkow@31719
  1067
      done
nipkow@31719
  1068
    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
nipkow@31952
  1069
      by (intro coprime_cong_prod_nat, auto)
nipkow@31719
  1070
    with zless less show "z = ?x"
nipkow@31952
  1071
      apply (intro cong_less_modulus_unique_nat)
nipkow@31952
  1072
      apply (auto, erule cong_sym_nat)
nipkow@31719
  1073
      done
nipkow@31719
  1074
  qed 
nipkow@31719
  1075
  from less cong unique show ?thesis
nipkow@31719
  1076
    by blast  
nipkow@31719
  1077
qed
nipkow@31719
  1078
nipkow@31719
  1079
end