src/HOL/NumberTheory/EvenOdd.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 14981 e73f8140af78
child 16663 13e9c402308b
permissions -rw-r--r--
migrated theory headers to new format
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
haftmann@16417
     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"
paulson@13871
    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
paulson@13871
    25
lemma one_not_even: "~(1 \<in> zEven)";
paulson@13871
    26
  apply (simp add: zEven_def)
paulson@13871
    27
  apply (rule allI, case_tac "k \<le> 0", auto)
paulson@13871
    28
done
paulson@13871
    29
paulson@13871
    30
lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)";
paulson@13871
    31
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
    32
  proof -;
paulson@13871
    33
    fix a b;
paulson@13871
    34
    assume "2 * (a::int) = 2 * (b::int) + 1"; 
paulson@13871
    35
    then have "2 * (a::int) - 2 * (b :: int) = 1";
paulson@13871
    36
       by arith
paulson@13871
    37
    then have "2 * (a - b) = 1";
paulson@13871
    38
       by (auto simp add: zdiff_zmult_distrib)
paulson@13871
    39
    moreover have "(2 * (a - b)):zEven";
paulson@13871
    40
       by (auto simp only: zEven_def)
paulson@13871
    41
    ultimately show "False";
paulson@13871
    42
       by (auto simp add: one_not_even)
paulson@13871
    43
  qed;
paulson@13871
    44
paulson@13871
    45
lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)";
paulson@14434
    46
  by (simp add: zOdd_def zEven_def, presburger)
paulson@13871
    47
paulson@13871
    48
lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
paulson@13871
    49
  by (insert even_odd_disj, auto)
paulson@13871
    50
paulson@13871
    51
lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd";
paulson@13871
    52
  apply (case_tac "x \<in> zOdd", auto)
paulson@13871
    53
  apply (drule not_odd_impl_even)
paulson@13871
    54
  apply (auto simp add: zEven_def zOdd_def)
paulson@13871
    55
  proof -;
paulson@13871
    56
    fix a b; 
paulson@13871
    57
    assume "2 * a * y = 2 * b + 1";
paulson@13871
    58
    then have "2 * a * y - 2 * b = 1";
paulson@13871
    59
      by arith
paulson@13871
    60
    then have "2 * (a * y - b) = 1";
paulson@13871
    61
      by (auto simp add: zdiff_zmult_distrib)
paulson@13871
    62
    moreover have "(2 * (a * y - b)):zEven";
paulson@13871
    63
       by (auto simp only: zEven_def)
paulson@13871
    64
    ultimately show "False";
paulson@13871
    65
       by (auto simp add: one_not_even)
paulson@13871
    66
  qed;
paulson@13871
    67
paulson@13871
    68
lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven";
paulson@13871
    69
  by (auto simp add: zOdd_def zEven_def)
paulson@13871
    70
paulson@13871
    71
lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0";
paulson@13871
    72
  by (auto simp add: zEven_def)
paulson@13871
    73
paulson@13871
    74
lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x";
paulson@13871
    75
  by (auto simp add: zEven_def)
paulson@13871
    76
paulson@13871
    77
lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven";
paulson@13871
    78
  apply (auto simp add: zEven_def)
paulson@13871
    79
  by (auto simp only: zadd_zmult_distrib2 [THEN sym])
paulson@13871
    80
paulson@13871
    81
lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven";
paulson@13871
    82
  by (auto simp add: zEven_def)
paulson@13871
    83
paulson@13871
    84
lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven";
paulson@13871
    85
  apply (auto simp add: zEven_def)
paulson@13871
    86
  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
paulson@13871
    87
paulson@13871
    88
lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven";
paulson@13871
    89
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
    90
  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
paulson@13871
    91
paulson@13871
    92
lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd";
paulson@13871
    93
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
    94
  apply (rule_tac x = "k - ka - 1" in exI)
paulson@13871
    95
  by auto
paulson@13871
    96
paulson@13871
    97
lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd";
paulson@13871
    98
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
    99
  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
paulson@13871
   100
paulson@13871
   101
lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd";
paulson@13871
   102
  apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
paulson@13871
   103
  apply (rule_tac x = "2 * ka * k + ka + k" in exI)
paulson@13871
   104
  by (auto simp add: zadd_zmult_distrib)
paulson@13871
   105
paulson@13871
   106
lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))";
paulson@13871
   107
  by (insert even_odd_conj even_odd_disj, auto)
paulson@13871
   108
paulson@13871
   109
lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"; 
paulson@13871
   110
  by (insert odd_iff_not_even odd_times_odd, auto)
paulson@13871
   111
paulson@13871
   112
lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))";
paulson@13871
   113
  apply (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
paulson@13871
   114
     even_minus_odd odd_minus_even)
paulson@13871
   115
  proof -;
paulson@13871
   116
    assume "x - y \<in> zEven" and "x \<in> zEven";
paulson@13871
   117
    show "y \<in> zEven";
paulson@13871
   118
    proof (rule classical);
paulson@13871
   119
      assume "~(y \<in> zEven)"; 
paulson@13871
   120
      then have "y \<in> zOdd" 
paulson@13871
   121
        by (auto simp add: odd_iff_not_even)
paulson@13871
   122
      with prems have "x - y \<in> zOdd";
paulson@13871
   123
        by (simp add: even_minus_odd)
paulson@13871
   124
      with prems have "False"; 
paulson@13871
   125
        by (auto simp add: odd_iff_not_even)
paulson@13871
   126
      thus ?thesis;
paulson@13871
   127
        by auto
paulson@13871
   128
    qed;
paulson@13871
   129
    next assume "x - y \<in> zEven" and "y \<in> zEven"; 
paulson@13871
   130
    show "x \<in> zEven";
paulson@13871
   131
    proof (rule classical);
paulson@13871
   132
      assume "~(x \<in> zEven)"; 
paulson@13871
   133
      then have "x \<in> zOdd" 
paulson@13871
   134
        by (auto simp add: odd_iff_not_even)
paulson@13871
   135
      with prems have "x - y \<in> zOdd";
paulson@13871
   136
        by (simp add: odd_minus_even)
paulson@13871
   137
      with prems have "False"; 
paulson@13871
   138
        by (auto simp add: odd_iff_not_even)
paulson@13871
   139
      thus ?thesis;
paulson@13871
   140
        by auto
paulson@13871
   141
    qed;
paulson@13871
   142
  qed;
paulson@13871
   143
paulson@13871
   144
lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1";
paulson@13871
   145
proof -;
paulson@13871
   146
  assume "x \<in> zEven" and "0 \<le> x";
paulson@13871
   147
  then have "\<exists>k. x = 2 * k";
paulson@13871
   148
    by (auto simp only: zEven_def)
paulson@13871
   149
  then show ?thesis;
paulson@13871
   150
    proof;
paulson@13871
   151
      fix a;
paulson@13871
   152
      assume "x = 2 * a";
paulson@13871
   153
      from prems have a: "0 \<le> a";
paulson@13871
   154
        by arith
paulson@13871
   155
      from prems have "nat x = nat(2 * a)";
paulson@13871
   156
        by auto
paulson@13871
   157
      also from a have "nat (2 * a) = 2 * nat a";
paulson@13871
   158
        by (auto simp add: nat_mult_distrib)
paulson@13871
   159
      finally have "(-1::int)^nat x = (-1)^(2 * nat a)";
paulson@13871
   160
        by auto
paulson@13871
   161
      also have "... = ((-1::int)^2)^ (nat a)";
paulson@13871
   162
        by (auto simp add: zpower_zpower [THEN sym])
paulson@13871
   163
      also have "(-1::int)^2 = 1";
paulson@13871
   164
        by auto
paulson@13871
   165
      finally; show ?thesis;
paulson@14348
   166
        by auto
paulson@13871
   167
    qed;
paulson@13871
   168
qed;
paulson@13871
   169
paulson@13871
   170
lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1";
paulson@13871
   171
proof -;
paulson@13871
   172
  assume "x \<in> zOdd" and "0 \<le> x";
paulson@13871
   173
  then have "\<exists>k. x = 2 * k + 1";
paulson@13871
   174
    by (auto simp only: zOdd_def)
paulson@13871
   175
  then show ?thesis;
paulson@13871
   176
    proof;
paulson@13871
   177
      fix a;
paulson@13871
   178
      assume "x = 2 * a + 1";
paulson@13871
   179
      from prems have a: "0 \<le> a";
paulson@13871
   180
        by arith
paulson@13871
   181
      from prems have "nat x = nat(2 * a + 1)";
paulson@13871
   182
        by auto
paulson@13871
   183
      also from a have "nat (2 * a + 1) = 2 * nat a + 1";
paulson@13871
   184
        by (auto simp add: nat_mult_distrib nat_add_distrib)
paulson@13871
   185
      finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)";
paulson@13871
   186
        by auto
paulson@13871
   187
      also have "... = ((-1::int)^2)^ (nat a) * (-1)^1";
paulson@13871
   188
        by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib)
paulson@13871
   189
      also have "(-1::int)^2 = 1";
paulson@13871
   190
        by auto
paulson@13871
   191
      finally; show ?thesis;
paulson@14348
   192
        by auto
paulson@13871
   193
    qed;
paulson@13871
   194
qed;
paulson@13871
   195
paulson@13871
   196
lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> 
paulson@13871
   197
  (-1::int)^(nat x) = (-1::int)^(nat y)";
paulson@13871
   198
  apply (insert even_odd_disj [of x])
paulson@13871
   199
  apply (insert even_odd_disj [of y])
paulson@13871
   200
  by (auto simp add: neg_one_even_power neg_one_odd_power)
paulson@13871
   201
paulson@13871
   202
lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))";
paulson@13871
   203
  by (auto simp add: zcong_def zdvd_not_zless)
paulson@13871
   204
paulson@13871
   205
lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2";
paulson@13871
   206
  apply (auto simp only: zEven_def)
paulson@13871
   207
  proof -;
paulson@13871
   208
    fix k assume "x < 2 * k";
paulson@13871
   209
    then have "x div 2 < k" by (auto simp add: div_prop1)
paulson@13871
   210
    also have "k = (2 * k) div 2"; by auto
paulson@13871
   211
    finally show "x div 2 < 2 * k div 2" by auto
paulson@13871
   212
  qed;
paulson@13871
   213
paulson@13871
   214
lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2";
paulson@13871
   215
  by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
paulson@13871
   216
paulson@13871
   217
lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y";
paulson@13871
   218
  by (auto simp add: zEven_def)
paulson@13871
   219
paulson@13871
   220
(* An odd prime is greater than 2 *)
paulson@13871
   221
paulson@13871
   222
lemma zprime_zOdd_eq_grt_2: "p \<in> zprime ==> (p \<in> zOdd) = (2 < p)";
paulson@13871
   223
  apply (auto simp add: zOdd_def zprime_def)
paulson@13871
   224
  apply (drule_tac x = 2 in allE)
paulson@13871
   225
  apply (insert odd_iff_not_even [of p])  
paulson@13871
   226
by (auto simp add: zOdd_def zEven_def)
paulson@13871
   227
paulson@13871
   228
(* Powers of -1 and parity *)
paulson@13871
   229
paulson@13871
   230
lemma neg_one_special: "finite A ==> 
paulson@13871
   231
    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1";
paulson@13871
   232
  by (induct set: Finites, auto)
paulson@13871
   233
paulson@13871
   234
lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1";
paulson@13871
   235
  apply (induct_tac n)
paulson@13871
   236
  by auto
paulson@13871
   237
paulson@13871
   238
lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
paulson@13871
   239
  ==> ((-1::int)^j = (-1::int)^k)";
paulson@13871
   240
  apply (insert neg_one_power [of j])
paulson@13871
   241
  apply (insert neg_one_power [of k])
paulson@13871
   242
  by (auto simp add: one_not_neg_one_mod_m zcong_sym)
paulson@13871
   243
paulson@13871
   244
end;