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