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