src/HOL/NumberTheory/EvenOdd.thy
author paulson
Fri Jan 09 10:46:18 2004 +0100 (2004-01-09)
changeset 14348 744c868ee0b7
parent 13871 26e5f5e624f6
child 14434 5f14c1207499
permissions -rw-r--r--
Defining the type class "ringpower" and deleting superseded theorems for
types nat, int, real, hypreal
paulson@13871
     1
(*  Title:      HOL/Quadratic_Reciprocity/EvenOdd.thy
paulson@13871
     2
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
paulson@13871
     3
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
paulson@13871
     4
*)
paulson@13871
     5
paulson@13871
     6
header {*Parity: Even and Odd Integers*}
paulson@13871
     7
paulson@13871
     8
theory EvenOdd = Int2:;
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@13871
    46
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
    47
  proof -;
paulson@13871
    48
    assume "\<forall>k. x \<noteq> 2 * k";
paulson@13871
    49
    have "0 \<le> (x mod 2) & (x mod 2) < 2";
paulson@13871
    50
      by (auto intro: pos_mod_sign pos_mod_bound)
paulson@13871
    51
    then have "x mod 2 = 0 | x mod 2 = 1" by arith
paulson@13871
    52
    moreover from prems have "x mod 2 \<noteq> 0" by auto
paulson@13871
    53
    ultimately have "x mod 2 = 1" by auto
paulson@13871
    54
    thus "\<exists>k. x = 2 * k + 1";
paulson@13871
    55
      by (insert zmod_zdiv_equality [of "x" "2"], auto)
paulson@13871
    56
  qed;
paulson@13871
    57
paulson@13871
    58
lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven";
paulson@13871
    59
  by (insert even_odd_disj, auto)
paulson@13871
    60
paulson@13871
    61
lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd";
paulson@13871
    62
  apply (case_tac "x \<in> zOdd", auto)
paulson@13871
    63
  apply (drule not_odd_impl_even)
paulson@13871
    64
  apply (auto simp add: zEven_def zOdd_def)
paulson@13871
    65
  proof -;
paulson@13871
    66
    fix a b; 
paulson@13871
    67
    assume "2 * a * y = 2 * b + 1";
paulson@13871
    68
    then have "2 * a * y - 2 * b = 1";
paulson@13871
    69
      by arith
paulson@13871
    70
    then have "2 * (a * y - b) = 1";
paulson@13871
    71
      by (auto simp add: zdiff_zmult_distrib)
paulson@13871
    72
    moreover have "(2 * (a * y - b)):zEven";
paulson@13871
    73
       by (auto simp only: zEven_def)
paulson@13871
    74
    ultimately show "False";
paulson@13871
    75
       by (auto simp add: one_not_even)
paulson@13871
    76
  qed;
paulson@13871
    77
paulson@13871
    78
lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven";
paulson@13871
    79
  by (auto simp add: zOdd_def zEven_def)
paulson@13871
    80
paulson@13871
    81
lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0";
paulson@13871
    82
  by (auto simp add: zEven_def)
paulson@13871
    83
paulson@13871
    84
lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x";
paulson@13871
    85
  by (auto simp add: zEven_def)
paulson@13871
    86
paulson@13871
    87
lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven";
paulson@13871
    88
  apply (auto simp add: zEven_def)
paulson@13871
    89
  by (auto simp only: zadd_zmult_distrib2 [THEN sym])
paulson@13871
    90
paulson@13871
    91
lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven";
paulson@13871
    92
  by (auto simp add: zEven_def)
paulson@13871
    93
paulson@13871
    94
lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven";
paulson@13871
    95
  apply (auto simp add: zEven_def)
paulson@13871
    96
  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
paulson@13871
    97
paulson@13871
    98
lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven";
paulson@13871
    99
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
   100
  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
paulson@13871
   101
paulson@13871
   102
lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd";
paulson@13871
   103
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
   104
  apply (rule_tac x = "k - ka - 1" in exI)
paulson@13871
   105
  by auto
paulson@13871
   106
paulson@13871
   107
lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd";
paulson@13871
   108
  apply (auto simp add: zOdd_def zEven_def)
paulson@13871
   109
  by (auto simp only: zdiff_zmult_distrib2 [THEN sym])
paulson@13871
   110
paulson@13871
   111
lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd";
paulson@13871
   112
  apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
paulson@13871
   113
  apply (rule_tac x = "2 * ka * k + ka + k" in exI)
paulson@13871
   114
  by (auto simp add: zadd_zmult_distrib)
paulson@13871
   115
paulson@13871
   116
lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))";
paulson@13871
   117
  by (insert even_odd_conj even_odd_disj, auto)
paulson@13871
   118
paulson@13871
   119
lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"; 
paulson@13871
   120
  by (insert odd_iff_not_even odd_times_odd, auto)
paulson@13871
   121
paulson@13871
   122
lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))";
paulson@13871
   123
  apply (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
paulson@13871
   124
     even_minus_odd odd_minus_even)
paulson@13871
   125
  proof -;
paulson@13871
   126
    assume "x - y \<in> zEven" and "x \<in> zEven";
paulson@13871
   127
    show "y \<in> zEven";
paulson@13871
   128
    proof (rule classical);
paulson@13871
   129
      assume "~(y \<in> zEven)"; 
paulson@13871
   130
      then have "y \<in> zOdd" 
paulson@13871
   131
        by (auto simp add: odd_iff_not_even)
paulson@13871
   132
      with prems have "x - y \<in> zOdd";
paulson@13871
   133
        by (simp add: even_minus_odd)
paulson@13871
   134
      with prems have "False"; 
paulson@13871
   135
        by (auto simp add: odd_iff_not_even)
paulson@13871
   136
      thus ?thesis;
paulson@13871
   137
        by auto
paulson@13871
   138
    qed;
paulson@13871
   139
    next assume "x - y \<in> zEven" and "y \<in> zEven"; 
paulson@13871
   140
    show "x \<in> zEven";
paulson@13871
   141
    proof (rule classical);
paulson@13871
   142
      assume "~(x \<in> zEven)"; 
paulson@13871
   143
      then have "x \<in> zOdd" 
paulson@13871
   144
        by (auto simp add: odd_iff_not_even)
paulson@13871
   145
      with prems have "x - y \<in> zOdd";
paulson@13871
   146
        by (simp add: odd_minus_even)
paulson@13871
   147
      with prems have "False"; 
paulson@13871
   148
        by (auto simp add: odd_iff_not_even)
paulson@13871
   149
      thus ?thesis;
paulson@13871
   150
        by auto
paulson@13871
   151
    qed;
paulson@13871
   152
  qed;
paulson@13871
   153
paulson@13871
   154
lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1";
paulson@13871
   155
proof -;
paulson@13871
   156
  assume "x \<in> zEven" and "0 \<le> x";
paulson@13871
   157
  then have "\<exists>k. x = 2 * k";
paulson@13871
   158
    by (auto simp only: zEven_def)
paulson@13871
   159
  then show ?thesis;
paulson@13871
   160
    proof;
paulson@13871
   161
      fix a;
paulson@13871
   162
      assume "x = 2 * a";
paulson@13871
   163
      from prems have a: "0 \<le> a";
paulson@13871
   164
        by arith
paulson@13871
   165
      from prems have "nat x = nat(2 * a)";
paulson@13871
   166
        by auto
paulson@13871
   167
      also from a have "nat (2 * a) = 2 * nat a";
paulson@13871
   168
        by (auto simp add: nat_mult_distrib)
paulson@13871
   169
      finally have "(-1::int)^nat x = (-1)^(2 * nat a)";
paulson@13871
   170
        by auto
paulson@13871
   171
      also have "... = ((-1::int)^2)^ (nat a)";
paulson@13871
   172
        by (auto simp add: zpower_zpower [THEN sym])
paulson@13871
   173
      also have "(-1::int)^2 = 1";
paulson@13871
   174
        by auto
paulson@13871
   175
      finally; show ?thesis;
paulson@14348
   176
        by auto
paulson@13871
   177
    qed;
paulson@13871
   178
qed;
paulson@13871
   179
paulson@13871
   180
lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1";
paulson@13871
   181
proof -;
paulson@13871
   182
  assume "x \<in> zOdd" and "0 \<le> x";
paulson@13871
   183
  then have "\<exists>k. x = 2 * k + 1";
paulson@13871
   184
    by (auto simp only: zOdd_def)
paulson@13871
   185
  then show ?thesis;
paulson@13871
   186
    proof;
paulson@13871
   187
      fix a;
paulson@13871
   188
      assume "x = 2 * a + 1";
paulson@13871
   189
      from prems have a: "0 \<le> a";
paulson@13871
   190
        by arith
paulson@13871
   191
      from prems have "nat x = nat(2 * a + 1)";
paulson@13871
   192
        by auto
paulson@13871
   193
      also from a have "nat (2 * a + 1) = 2 * nat a + 1";
paulson@13871
   194
        by (auto simp add: nat_mult_distrib nat_add_distrib)
paulson@13871
   195
      finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)";
paulson@13871
   196
        by auto
paulson@13871
   197
      also have "... = ((-1::int)^2)^ (nat a) * (-1)^1";
paulson@13871
   198
        by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib)
paulson@13871
   199
      also have "(-1::int)^2 = 1";
paulson@13871
   200
        by auto
paulson@13871
   201
      finally; show ?thesis;
paulson@14348
   202
        by auto
paulson@13871
   203
    qed;
paulson@13871
   204
qed;
paulson@13871
   205
paulson@13871
   206
lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> 
paulson@13871
   207
  (-1::int)^(nat x) = (-1::int)^(nat y)";
paulson@13871
   208
  apply (insert even_odd_disj [of x])
paulson@13871
   209
  apply (insert even_odd_disj [of y])
paulson@13871
   210
  by (auto simp add: neg_one_even_power neg_one_odd_power)
paulson@13871
   211
paulson@13871
   212
lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))";
paulson@13871
   213
  by (auto simp add: zcong_def zdvd_not_zless)
paulson@13871
   214
paulson@13871
   215
lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2";
paulson@13871
   216
  apply (auto simp only: zEven_def)
paulson@13871
   217
  proof -;
paulson@13871
   218
    fix k assume "x < 2 * k";
paulson@13871
   219
    then have "x div 2 < k" by (auto simp add: div_prop1)
paulson@13871
   220
    also have "k = (2 * k) div 2"; by auto
paulson@13871
   221
    finally show "x div 2 < 2 * k div 2" by auto
paulson@13871
   222
  qed;
paulson@13871
   223
paulson@13871
   224
lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2";
paulson@13871
   225
  by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
paulson@13871
   226
paulson@13871
   227
lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y";
paulson@13871
   228
  by (auto simp add: zEven_def)
paulson@13871
   229
paulson@13871
   230
(* An odd prime is greater than 2 *)
paulson@13871
   231
paulson@13871
   232
lemma zprime_zOdd_eq_grt_2: "p \<in> zprime ==> (p \<in> zOdd) = (2 < p)";
paulson@13871
   233
  apply (auto simp add: zOdd_def zprime_def)
paulson@13871
   234
  apply (drule_tac x = 2 in allE)
paulson@13871
   235
  apply (insert odd_iff_not_even [of p])  
paulson@13871
   236
by (auto simp add: zOdd_def zEven_def)
paulson@13871
   237
paulson@13871
   238
(* Powers of -1 and parity *)
paulson@13871
   239
paulson@13871
   240
lemma neg_one_special: "finite A ==> 
paulson@13871
   241
    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1";
paulson@13871
   242
  by (induct set: Finites, auto)
paulson@13871
   243
paulson@13871
   244
lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1";
paulson@13871
   245
  apply (induct_tac n)
paulson@13871
   246
  by auto
paulson@13871
   247
paulson@13871
   248
lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
paulson@13871
   249
  ==> ((-1::int)^j = (-1::int)^k)";
paulson@13871
   250
  apply (insert neg_one_power [of j])
paulson@13871
   251
  apply (insert neg_one_power [of k])
paulson@13871
   252
  by (auto simp add: one_not_neg_one_mod_m zcong_sym)
paulson@13871
   253
paulson@13871
   254
end;