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