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