src/HOL/NumberTheory/EvenOdd.thy
author wenzelm
Thu Dec 08 12:50:04 2005 +0100 (2005-12-08)
changeset 18369 694ea14ab4f2
parent 16663 13e9c402308b
child 19670 2e4a143c73c5
permissions -rw-r--r--
tuned sources and proofs
paulson@13871
     1
(*  Title:      HOL/Quadratic_Reciprocity/EvenOdd.thy
kleing@14981
     2
    ID:         $Id$
paulson@13871
     3
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
paulson@13871
     4
*)
paulson@13871
     5
paulson@13871
     6
header {*Parity: Even and Odd Integers*}
paulson@13871
     7
wenzelm@18369
     8
theory EvenOdd imports Int2 begin
paulson@13871
     9
paulson@13871
    10
text{*Note.  This theory is being revised.  See the web page
paulson@13871
    11
\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
paulson@13871
    12
paulson@13871
    13
constdefs
paulson@13871
    14
  zOdd    :: "int set"
wenzelm@18369
    15
  "zOdd == {x. \<exists>k. x = 2 * k + 1}"
paulson@13871
    16
  zEven   :: "int set"
paulson@13871
    17
  "zEven == {x. \<exists>k. x = 2 * k}"
paulson@13871
    18
paulson@13871
    19
(***********************************************************)
paulson@13871
    20
(*                                                         *)
paulson@13871
    21
(* Some useful properties about even and odd               *)
paulson@13871
    22
(*                                                         *)
paulson@13871
    23
(***********************************************************)
paulson@13871
    24
wenzelm@18369
    25
lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
wenzelm@18369
    26
  and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@18369
    27
  by (auto simp add: zOdd_def)
paulson@13871
    28
wenzelm@18369
    29
lemma zEvenI [intro?]: "x = 2 * k \<Longrightarrow> x \<in> zEven"
wenzelm@18369
    30
  and zEvenE [elim?]: "x \<in> zEven \<Longrightarrow> (!!k. x = 2 * k \<Longrightarrow> C) \<Longrightarrow> C"
wenzelm@18369
    31
  by (auto simp add: zEven_def)
wenzelm@18369
    32
wenzelm@18369
    33
lemma one_not_even: "~(1 \<in> zEven)"
wenzelm@18369
    34
proof
wenzelm@18369
    35
  assume "1 \<in> zEven"
wenzelm@18369
    36
  then obtain k :: int where "1 = 2 * k" ..
wenzelm@18369
    37
  then show False by arith
wenzelm@18369
    38
qed
paulson@13871
    39
wenzelm@18369
    40
lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)"
wenzelm@18369
    41
proof -
wenzelm@18369
    42
  {
wenzelm@18369
    43
    fix a b
wenzelm@18369
    44
    assume "2 * (a::int) = 2 * (b::int) + 1"
wenzelm@18369
    45
    then have "2 * (a::int) - 2 * (b :: int) = 1"
wenzelm@18369
    46
      by arith
wenzelm@18369
    47
    then have "2 * (a - b) = 1"
wenzelm@18369
    48
      by (auto simp add: zdiff_zmult_distrib)
wenzelm@18369
    49
    moreover have "(2 * (a - b)):zEven"
wenzelm@18369
    50
      by (auto simp only: zEven_def)
wenzelm@18369
    51
    ultimately have False
wenzelm@18369
    52
      by (auto simp add: one_not_even)
wenzelm@18369
    53
  }
wenzelm@18369
    54
  then show ?thesis
wenzelm@18369
    55
    by (auto simp add: zOdd_def zEven_def)
wenzelm@18369
    56
qed
paulson@13871
    57
wenzelm@18369
    58
lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)"
wenzelm@18369
    59
  by (simp add: zOdd_def zEven_def) arith
paulson@13871
    60
wenzelm@18369
    61
lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven"
wenzelm@18369
    62
  using even_odd_disj by auto
paulson@13871
    63
wenzelm@18369
    64
lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd"
wenzelm@18369
    65
proof (rule classical)
wenzelm@18369
    66
  assume "\<not> ?thesis"
wenzelm@18369
    67
  then have "x \<in> zEven" by (rule not_odd_impl_even)
wenzelm@18369
    68
  then obtain a where a: "x = 2 * a" ..
wenzelm@18369
    69
  assume "x * y : zOdd"
wenzelm@18369
    70
  then obtain b where "x * y = 2 * b + 1" ..
wenzelm@18369
    71
  with a have "2 * a * y = 2 * b + 1" by simp
wenzelm@18369
    72
  then have "2 * a * y - 2 * b = 1"
wenzelm@18369
    73
    by arith
wenzelm@18369
    74
  then have "2 * (a * y - b) = 1"
wenzelm@18369
    75
    by (auto simp add: zdiff_zmult_distrib)
wenzelm@18369
    76
  moreover have "(2 * (a * y - b)):zEven"
wenzelm@18369
    77
    by (auto simp only: zEven_def)
wenzelm@18369
    78
  ultimately have False
wenzelm@18369
    79
    by (auto simp add: one_not_even)
wenzelm@18369
    80
  then show ?thesis ..
wenzelm@18369
    81
qed
wenzelm@18369
    82
wenzelm@18369
    83
lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven"
paulson@13871
    84
  by (auto simp add: zOdd_def zEven_def)
paulson@13871
    85
wenzelm@18369
    86
lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0"
paulson@13871
    87
  by (auto simp add: zEven_def)
paulson@13871
    88
wenzelm@18369
    89
lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x"
paulson@13871
    90
  by (auto simp add: zEven_def)
paulson@13871
    91
wenzelm@18369
    92
lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
paulson@13871
    93
  apply (auto simp add: zEven_def)
wenzelm@18369
    94
  apply (auto simp only: zadd_zmult_distrib2 [symmetric])
wenzelm@18369
    95
  done
paulson@13871
    96
wenzelm@18369
    97
lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
paulson@13871
    98
  by (auto simp add: zEven_def)
paulson@13871
    99
wenzelm@18369
   100
lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven"
paulson@13871
   101
  apply (auto simp add: zEven_def)
wenzelm@18369
   102
  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
wenzelm@18369
   103
  done
paulson@13871
   104
wenzelm@18369
   105
lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"
paulson@13871
   106
  apply (auto simp add: zOdd_def zEven_def)
wenzelm@18369
   107
  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
wenzelm@18369
   108
  done
paulson@13871
   109
wenzelm@18369
   110
lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"
paulson@13871
   111
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
   112
  apply (rule_tac x = "k - ka - 1" in exI)
wenzelm@18369
   113
  apply auto
wenzelm@18369
   114
  done
paulson@13871
   115
wenzelm@18369
   116
lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"
paulson@13871
   117
  apply (auto simp add: zOdd_def zEven_def)
wenzelm@18369
   118
  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
wenzelm@18369
   119
  done
paulson@13871
   120
wenzelm@18369
   121
lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd"
paulson@13871
   122
  apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
paulson@13871
   123
  apply (rule_tac x = "2 * ka * k + ka + k" in exI)
wenzelm@18369
   124
  apply (auto simp add: zadd_zmult_distrib)
wenzelm@18369
   125
  done
paulson@13871
   126
wenzelm@18369
   127
lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
wenzelm@18369
   128
  using even_odd_conj even_odd_disj by auto
wenzelm@18369
   129
wenzelm@18369
   130
lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"
wenzelm@18369
   131
  using odd_iff_not_even odd_times_odd by auto
paulson@13871
   132
wenzelm@18369
   133
lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))"
wenzelm@18369
   134
proof
wenzelm@18369
   135
  assume xy: "x - y \<in> zEven"
wenzelm@18369
   136
  {
wenzelm@18369
   137
    assume x: "x \<in> zEven"
wenzelm@18369
   138
    have "y \<in> zEven"
wenzelm@18369
   139
    proof (rule classical)
wenzelm@18369
   140
      assume "\<not> ?thesis"
wenzelm@18369
   141
      then have "y \<in> zOdd"
wenzelm@18369
   142
        by (simp add: odd_iff_not_even)
wenzelm@18369
   143
      with x have "x - y \<in> zOdd"
wenzelm@18369
   144
        by (simp add: even_minus_odd)
wenzelm@18369
   145
      with xy have False
wenzelm@18369
   146
        by (auto simp add: odd_iff_not_even)
wenzelm@18369
   147
      then show ?thesis ..
wenzelm@18369
   148
    qed
wenzelm@18369
   149
  } moreover {
wenzelm@18369
   150
    assume y: "y \<in> zEven"
wenzelm@18369
   151
    have "x \<in> zEven"
wenzelm@18369
   152
    proof (rule classical)
wenzelm@18369
   153
      assume "\<not> ?thesis"
wenzelm@18369
   154
      then have "x \<in> zOdd"
wenzelm@18369
   155
        by (auto simp add: odd_iff_not_even)
wenzelm@18369
   156
      with y have "x - y \<in> zOdd"
wenzelm@18369
   157
        by (simp add: odd_minus_even)
wenzelm@18369
   158
      with xy have False
wenzelm@18369
   159
        by (auto simp add: odd_iff_not_even)
wenzelm@18369
   160
      then show ?thesis ..
wenzelm@18369
   161
    qed
wenzelm@18369
   162
  }
wenzelm@18369
   163
  ultimately show "(x \<in> zEven) = (y \<in> zEven)"
wenzelm@18369
   164
    by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
wenzelm@18369
   165
      even_minus_odd odd_minus_even)
wenzelm@18369
   166
next
wenzelm@18369
   167
  assume "(x \<in> zEven) = (y \<in> zEven)"
wenzelm@18369
   168
  then show "x - y \<in> zEven"
wenzelm@18369
   169
    by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
wenzelm@18369
   170
      even_minus_odd odd_minus_even)
wenzelm@18369
   171
qed
paulson@13871
   172
wenzelm@18369
   173
lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
wenzelm@18369
   174
proof -
wenzelm@18369
   175
  assume 1: "x \<in> zEven" and 2: "0 \<le> x"
wenzelm@18369
   176
  from 1 obtain a where 3: "x = 2 * a" ..
wenzelm@18369
   177
  with 2 have "0 \<le> a" by simp
wenzelm@18369
   178
  from 2 3 have "nat x = nat (2 * a)"
wenzelm@18369
   179
    by simp
wenzelm@18369
   180
  also from 3 have "nat (2 * a) = 2 * nat a"
wenzelm@18369
   181
    by (simp add: nat_mult_distrib)
wenzelm@18369
   182
  finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
wenzelm@18369
   183
    by simp
wenzelm@18369
   184
  also have "... = ((-1::int)^2)^ (nat a)"
wenzelm@18369
   185
    by (simp add: zpower_zpower [symmetric])
wenzelm@18369
   186
  also have "(-1::int)^2 = 1"
wenzelm@18369
   187
    by simp
wenzelm@18369
   188
  finally show ?thesis
wenzelm@18369
   189
    by simp
wenzelm@18369
   190
qed
paulson@13871
   191
wenzelm@18369
   192
lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
wenzelm@18369
   193
proof -
wenzelm@18369
   194
  assume 1: "x \<in> zOdd" and 2: "0 \<le> x"
wenzelm@18369
   195
  from 1 obtain a where 3: "x = 2 * a + 1" ..
wenzelm@18369
   196
  with 2 have a: "0 \<le> a" by simp
wenzelm@18369
   197
  with 2 3 have "nat x = nat (2 * a + 1)"
wenzelm@18369
   198
    by simp
wenzelm@18369
   199
  also from a have "nat (2 * a + 1) = 2 * nat a + 1"
wenzelm@18369
   200
    by (auto simp add: nat_mult_distrib nat_add_distrib)
wenzelm@18369
   201
  finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
wenzelm@18369
   202
    by simp
wenzelm@18369
   203
  also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
wenzelm@18369
   204
    by (auto simp add: zpower_zpower [symmetric] zpower_zadd_distrib)
wenzelm@18369
   205
  also have "(-1::int)^2 = 1"
wenzelm@18369
   206
    by simp
wenzelm@18369
   207
  finally show ?thesis
wenzelm@18369
   208
    by simp
wenzelm@18369
   209
qed
wenzelm@18369
   210
wenzelm@18369
   211
lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==>
wenzelm@18369
   212
  (-1::int)^(nat x) = (-1::int)^(nat y)"
wenzelm@18369
   213
  using even_odd_disj [of x] even_odd_disj [of y]
paulson@13871
   214
  by (auto simp add: neg_one_even_power neg_one_odd_power)
paulson@13871
   215
wenzelm@18369
   216
wenzelm@18369
   217
lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))"
paulson@13871
   218
  by (auto simp add: zcong_def zdvd_not_zless)
paulson@13871
   219
wenzelm@18369
   220
lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
wenzelm@18369
   221
proof -
wenzelm@18369
   222
  assume 1: "y \<in> zEven" and 2: "x < y"
wenzelm@18369
   223
  from 1 obtain k where k: "y = 2 * k" ..
wenzelm@18369
   224
  with 2 have "x < 2 * k" by simp
wenzelm@18369
   225
  then have "x div 2 < k" by (auto simp add: div_prop1)
wenzelm@18369
   226
  also have "k = (2 * k) div 2" by simp
wenzelm@18369
   227
  finally have "x div 2 < 2 * k div 2" by simp
wenzelm@18369
   228
  with k show ?thesis by simp
wenzelm@18369
   229
qed
paulson@13871
   230
wenzelm@18369
   231
lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"
paulson@13871
   232
  by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
paulson@13871
   233
wenzelm@18369
   234
lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"
paulson@13871
   235
  by (auto simp add: zEven_def)
paulson@13871
   236
paulson@13871
   237
(* An odd prime is greater than 2 *)
paulson@13871
   238
wenzelm@18369
   239
lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)"
paulson@13871
   240
  apply (auto simp add: zOdd_def zprime_def)
paulson@13871
   241
  apply (drule_tac x = 2 in allE)
wenzelm@18369
   242
  using odd_iff_not_even [of p]
wenzelm@18369
   243
  apply (auto simp add: zOdd_def zEven_def)
wenzelm@18369
   244
  done
paulson@13871
   245
paulson@13871
   246
(* Powers of -1 and parity *)
paulson@13871
   247
wenzelm@18369
   248
lemma neg_one_special: "finite A ==>
wenzelm@18369
   249
    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
wenzelm@18369
   250
  by (induct set: Finites) auto
paulson@13871
   251
wenzelm@18369
   252
lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
wenzelm@18369
   253
  by (induct n) auto
paulson@13871
   254
paulson@13871
   255
lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
wenzelm@18369
   256
    ==> ((-1::int)^j = (-1::int)^k)"
wenzelm@18369
   257
  using neg_one_power [of j] and insert neg_one_power [of k]
paulson@13871
   258
  by (auto simp add: one_not_neg_one_mod_m zcong_sym)
paulson@13871
   259
wenzelm@18369
   260
end