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