src/HOL/Old_Number_Theory/EvenOdd.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 61649 268d88ec9087 child 64240 eabf80376aab permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/Old_Number_Theory/EvenOdd.thy
```
```     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
```
```     3 *)
```
```     4
```
```     5 section \<open>Parity: Even and Odd Integers\<close>
```
```     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 \<open>Some useful properties about even and odd\<close>
```
```    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: distrib_left [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 distrib_right distrib_left)
```
```   117   apply (rule_tac x = "2 * ka * k + ka + k" in exI)
```
```   118   apply (auto simp add: distrib_right)
```
```   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 \<open>x \<in> zEven\<close> obtain a where "x = 2 * a" ..
```
```   171   with \<open>0 \<le> x\<close> have "0 \<le> a" by simp
```
```   172   from \<open>0 \<le> x\<close> and \<open>x = 2 * a\<close> have "nat x = nat (2 * a)"
```
```   173     by simp
```
```   174   also from \<open>x = 2 * a\<close> 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)\<^sup>2 ^ nat a"
```
```   179     by (simp add: power_mult)
```
```   180   also have "(-1::int)\<^sup>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 \<open>x \<in> zOdd\<close> obtain a where "x = 2 * a + 1" ..
```
```   190   with \<open>0 \<le> x\<close> have a: "0 \<le> a" by simp
```
```   191   with \<open>0 \<le> x\<close> and \<open>x = 2 * a + 1\<close> 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)\<^sup>2) ^ nat a * (-1)^1"
```
```   198     by (auto simp add: power_mult power_add)
```
```   199   also have "(-1::int)\<^sup>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 \<open>y \<in> zEven\<close> obtain k where k: "y = 2 * k" ..
```
```   218   with \<open>x < y\<close> 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) ^ card A) * ((- 1) ^ card A) = (1 :: int)"
```
```   244   unfolding power_add [symmetric] by simp
```
```   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
```