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