src/HOL/Old_Number_Theory/EvenOdd.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44766 d4d33a4d7548
child 49962 a8cc904a6820
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/Old_Number_Theory/EvenOdd.thy
     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     3 *)
     4 
     5 header {*Parity: Even and Odd Integers*}
     6 
     7 theory EvenOdd
     8 imports Int2
     9 begin
    10 
    11 definition zOdd :: "int set"
    12   where "zOdd = {x. \<exists>k. x = 2 * k + 1}"
    13 
    14 definition zEven :: "int set"
    15   where "zEven = {x. \<exists>k. x = 2 * k}"
    16 
    17 subsection {* Some useful properties about even and odd *}
    18 
    19 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
    20   and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
    21   by (auto simp add: zOdd_def)
    22 
    23 lemma zEvenI [intro?]: "x = 2 * k \<Longrightarrow> x \<in> zEven"
    24   and zEvenE [elim?]: "x \<in> zEven \<Longrightarrow> (!!k. x = 2 * k \<Longrightarrow> C) \<Longrightarrow> C"
    25   by (auto simp add: zEven_def)
    26 
    27 lemma one_not_even: "~(1 \<in> zEven)"
    28 proof
    29   assume "1 \<in> zEven"
    30   then obtain k :: int where "1 = 2 * k" ..
    31   then show False by arith
    32 qed
    33 
    34 lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)"
    35 proof -
    36   {
    37     fix a b
    38     assume "2 * (a::int) = 2 * (b::int) + 1"
    39     then have "2 * (a::int) - 2 * (b :: int) = 1"
    40       by arith
    41     then have "2 * (a - b) = 1"
    42       by (auto simp add: left_diff_distrib)
    43     moreover have "(2 * (a - b)):zEven"
    44       by (auto simp only: zEven_def)
    45     ultimately have False
    46       by (auto simp add: one_not_even)
    47   }
    48   then show ?thesis
    49     by (auto simp add: zOdd_def zEven_def)
    50 qed
    51 
    52 lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)"
    53   by (simp add: zOdd_def zEven_def) arith
    54 
    55 lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven"
    56   using even_odd_disj by auto
    57 
    58 lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd"
    59 proof (rule classical)
    60   assume "\<not> ?thesis"
    61   then have "x \<in> zEven" by (rule not_odd_impl_even)
    62   then obtain a where a: "x = 2 * a" ..
    63   assume "x * y : zOdd"
    64   then obtain b where "x * y = 2 * b + 1" ..
    65   with a have "2 * a * y = 2 * b + 1" by simp
    66   then have "2 * a * y - 2 * b = 1"
    67     by arith
    68   then have "2 * (a * y - b) = 1"
    69     by (auto simp add: left_diff_distrib)
    70   moreover have "(2 * (a * y - b)):zEven"
    71     by (auto simp only: zEven_def)
    72   ultimately have False
    73     by (auto simp add: one_not_even)
    74   then show ?thesis ..
    75 qed
    76 
    77 lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven"
    78   by (auto simp add: zOdd_def zEven_def)
    79 
    80 lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0"
    81   by (auto simp add: zEven_def)
    82 
    83 lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x"
    84   by (auto simp add: zEven_def)
    85 
    86 lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
    87   apply (auto simp add: zEven_def)
    88   apply (auto simp only: right_distrib [symmetric])
    89   done
    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   apply (auto simp only: right_diff_distrib [symmetric])
    97   done
    98 
    99 lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"
   100   apply (auto simp add: zOdd_def zEven_def)
   101   apply (auto simp only: right_diff_distrib [symmetric])
   102   done
   103 
   104 lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"
   105   apply (auto simp add: zOdd_def zEven_def)
   106   apply (rule_tac x = "k - ka - 1" in exI)
   107   apply auto
   108   done
   109 
   110 lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"
   111   apply (auto simp add: zOdd_def zEven_def)
   112   apply (auto simp only: right_diff_distrib [symmetric])
   113   done
   114 
   115 lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd"
   116   apply (auto simp add: zOdd_def left_distrib right_distrib)
   117   apply (rule_tac x = "2 * ka * k + ka + k" in exI)
   118   apply (auto simp add: left_distrib)
   119   done
   120 
   121 lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
   122   using even_odd_conj even_odd_disj by auto
   123 
   124 lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"
   125   using odd_iff_not_even odd_times_odd by auto
   126 
   127 lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))"
   128 proof
   129   assume xy: "x - y \<in> zEven"
   130   {
   131     assume x: "x \<in> zEven"
   132     have "y \<in> zEven"
   133     proof (rule classical)
   134       assume "\<not> ?thesis"
   135       then have "y \<in> zOdd"
   136         by (simp add: odd_iff_not_even)
   137       with x have "x - y \<in> zOdd"
   138         by (simp add: even_minus_odd)
   139       with xy have False
   140         by (auto simp add: odd_iff_not_even)
   141       then show ?thesis ..
   142     qed
   143   } moreover {
   144     assume y: "y \<in> zEven"
   145     have "x \<in> zEven"
   146     proof (rule classical)
   147       assume "\<not> ?thesis"
   148       then have "x \<in> zOdd"
   149         by (auto simp add: odd_iff_not_even)
   150       with y have "x - y \<in> zOdd"
   151         by (simp add: odd_minus_even)
   152       with xy have False
   153         by (auto simp add: odd_iff_not_even)
   154       then show ?thesis ..
   155     qed
   156   }
   157   ultimately show "(x \<in> zEven) = (y \<in> zEven)"
   158     by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
   159       even_minus_odd odd_minus_even)
   160 next
   161   assume "(x \<in> zEven) = (y \<in> zEven)"
   162   then show "x - y \<in> zEven"
   163     by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
   164       even_minus_odd odd_minus_even)
   165 qed
   166 
   167 lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
   168 proof -
   169   assume "x \<in> zEven" and "0 \<le> x"
   170   from `x \<in> zEven` obtain a where "x = 2 * a" ..
   171   with `0 \<le> x` have "0 \<le> a" by simp
   172   from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)"
   173     by simp
   174   also from `x = 2 * a` have "nat (2 * a) = 2 * nat a"
   175     by (simp add: nat_mult_distrib)
   176   finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
   177     by simp
   178   also have "... = ((-1::int)^2)^ (nat a)"
   179     by (simp add: zpower_zpower [symmetric])
   180   also have "(-1::int)^2 = 1"
   181     by simp
   182   finally show ?thesis
   183     by simp
   184 qed
   185 
   186 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
   187 proof -
   188   assume "x \<in> zOdd" and "0 \<le> x"
   189   from `x \<in> zOdd` obtain a where "x = 2 * a + 1" ..
   190   with `0 \<le> x` have a: "0 \<le> a" by simp
   191   with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)"
   192     by simp
   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 simp
   197   also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
   198     by (auto simp add: power_mult power_add)
   199   also have "(-1::int)^2 = 1"
   200     by simp
   201   finally show ?thesis
   202     by simp
   203 qed
   204 
   205 lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==>
   206     (-1::int)^(nat x) = (-1::int)^(nat y)"
   207   using even_odd_disj [of x] even_odd_disj [of y]
   208   by (auto simp add: neg_one_even_power neg_one_odd_power)
   209 
   210 
   211 lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))"
   212   by (auto simp add: zcong_def zdvd_not_zless)
   213 
   214 lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"
   215 proof -
   216   assume "y \<in> zEven" and "x < y"
   217   from `y \<in> zEven` obtain k where k: "y = 2 * k" ..
   218   with `x < y` have "x < 2 * k" by simp
   219   then have "x div 2 < k" by (auto simp add: div_prop1)
   220   also have "k = (2 * k) div 2" by simp
   221   finally have "x div 2 < 2 * k div 2" by simp
   222   with k show ?thesis by simp
   223 qed
   224 
   225 lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"
   226   by (auto simp add: zEven_def)
   227 
   228 lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"
   229   by (auto simp add: zEven_def)
   230 
   231 (* An odd prime is greater than 2 *)
   232 
   233 lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)"
   234   apply (auto simp add: zOdd_def zprime_def)
   235   apply (drule_tac x = 2 in allE)
   236   using odd_iff_not_even [of p]
   237   apply (auto simp add: zOdd_def zEven_def)
   238   done
   239 
   240 (* Powers of -1 and parity *)
   241 
   242 lemma neg_one_special: "finite A ==>
   243     ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
   244   by (induct set: finite) auto
   245 
   246 lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
   247   by (induct n) auto
   248 
   249 lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
   250     ==> ((-1::int)^j = (-1::int)^k)"
   251   using neg_one_power [of j] and ListMem.insert neg_one_power [of k]
   252   by (auto simp add: one_not_neg_one_mod_m zcong_sym)
   253 
   254 end