src/HOL/NumberTheory/EvenOdd.thy
 author haftmann Wed Sep 26 20:27:55 2007 +0200 (2007-09-26) changeset 24728 e2b3a1065676 parent 22274 ce1459004c8d child 26289 9d2c375e242b permissions -rw-r--r--
moved Finite_Set before Datatype
```     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" where
```
```    12   "zOdd = {x. \<exists>k. x = 2 * k + 1}"
```
```    13
```
```    14 definition
```
```    15   zEven   :: "int set" where
```
```    16   "zEven = {x. \<exists>k. x = 2 * k}"
```
```    17
```
```    18 subsection {* Some useful properties about even and odd *}
```
```    19
```
```    20 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
```
```    21   and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
```
```    22   by (auto simp add: zOdd_def)
```
```    23
```
```    24 lemma zEvenI [intro?]: "x = 2 * k \<Longrightarrow> x \<in> zEven"
```
```    25   and zEvenE [elim?]: "x \<in> zEven \<Longrightarrow> (!!k. x = 2 * k \<Longrightarrow> C) \<Longrightarrow> C"
```
```    26   by (auto simp add: zEven_def)
```
```    27
```
```    28 lemma one_not_even: "~(1 \<in> zEven)"
```
```    29 proof
```
```    30   assume "1 \<in> zEven"
```
```    31   then obtain k :: int where "1 = 2 * k" ..
```
```    32   then show False by arith
```
```    33 qed
```
```    34
```
```    35 lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)"
```
```    36 proof -
```
```    37   {
```
```    38     fix a b
```
```    39     assume "2 * (a::int) = 2 * (b::int) + 1"
```
```    40     then have "2 * (a::int) - 2 * (b :: int) = 1"
```
```    41       by arith
```
```    42     then have "2 * (a - b) = 1"
```
```    43       by (auto simp add: zdiff_zmult_distrib)
```
```    44     moreover have "(2 * (a - b)):zEven"
```
```    45       by (auto simp only: zEven_def)
```
```    46     ultimately have False
```
```    47       by (auto simp add: one_not_even)
```
```    48   }
```
```    49   then show ?thesis
```
```    50     by (auto simp add: zOdd_def zEven_def)
```
```    51 qed
```
```    52
```
```    53 lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)"
```
```    54   by (simp add: zOdd_def zEven_def) arith
```
```    55
```
```    56 lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven"
```
```    57   using even_odd_disj by auto
```
```    58
```
```    59 lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd"
```
```    60 proof (rule classical)
```
```    61   assume "\<not> ?thesis"
```
```    62   then have "x \<in> zEven" by (rule not_odd_impl_even)
```
```    63   then obtain a where a: "x = 2 * a" ..
```
```    64   assume "x * y : zOdd"
```
```    65   then obtain b where "x * y = 2 * b + 1" ..
```
```    66   with a have "2 * a * y = 2 * b + 1" by simp
```
```    67   then have "2 * a * y - 2 * b = 1"
```
```    68     by arith
```
```    69   then have "2 * (a * y - b) = 1"
```
```    70     by (auto simp add: zdiff_zmult_distrib)
```
```    71   moreover have "(2 * (a * y - b)):zEven"
```
```    72     by (auto simp only: zEven_def)
```
```    73   ultimately have False
```
```    74     by (auto simp add: one_not_even)
```
```    75   then show ?thesis ..
```
```    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   apply (auto simp only: zadd_zmult_distrib2 [symmetric])
```
```    90   done
```
```    91
```
```    92 lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
```
```    93   by (auto simp add: zEven_def)
```
```    94
```
```    95 lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven"
```
```    96   apply (auto simp add: zEven_def)
```
```    97   apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
```
```    98   done
```
```    99
```
```   100 lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"
```
```   101   apply (auto simp add: zOdd_def zEven_def)
```
```   102   apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
```
```   103   done
```
```   104
```
```   105 lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"
```
```   106   apply (auto simp add: zOdd_def zEven_def)
```
```   107   apply (rule_tac x = "k - ka - 1" in exI)
```
```   108   apply auto
```
```   109   done
```
```   110
```
```   111 lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"
```
```   112   apply (auto simp add: zOdd_def zEven_def)
```
```   113   apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
```
```   114   done
```
```   115
```
```   116 lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd"
```
```   117   apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
```
```   118   apply (rule_tac x = "2 * ka * k + ka + k" in exI)
```
```   119   apply (auto simp add: zadd_zmult_distrib)
```
```   120   done
```
```   121
```
```   122 lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
```
```   123   using even_odd_conj even_odd_disj by auto
```
```   124
```
```   125 lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"
```
```   126   using odd_iff_not_even odd_times_odd by auto
```
```   127
```
```   128 lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))"
```
```   129 proof
```
```   130   assume xy: "x - y \<in> zEven"
```
```   131   {
```
```   132     assume x: "x \<in> zEven"
```
```   133     have "y \<in> zEven"
```
```   134     proof (rule classical)
```
```   135       assume "\<not> ?thesis"
```
```   136       then have "y \<in> zOdd"
```
```   137         by (simp add: odd_iff_not_even)
```
```   138       with x have "x - y \<in> zOdd"
```
```   139         by (simp add: even_minus_odd)
```
```   140       with xy have False
```
```   141         by (auto simp add: odd_iff_not_even)
```
```   142       then show ?thesis ..
```
```   143     qed
```
```   144   } moreover {
```
```   145     assume y: "y \<in> zEven"
```
```   146     have "x \<in> zEven"
```
```   147     proof (rule classical)
```
```   148       assume "\<not> ?thesis"
```
```   149       then have "x \<in> zOdd"
```
```   150         by (auto simp add: odd_iff_not_even)
```
```   151       with y have "x - y \<in> zOdd"
```
```   152         by (simp add: odd_minus_even)
```
```   153       with xy have False
```
```   154         by (auto simp add: odd_iff_not_even)
```
```   155       then show ?thesis ..
```
```   156     qed
```
```   157   }
```
```   158   ultimately show "(x \<in> zEven) = (y \<in> zEven)"
```
```   159     by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd
```
```   160       even_minus_odd odd_minus_even)
```
```   161 next
```
```   162   assume "(x \<in> zEven) = (y \<in> zEven)"
```
```   163   then show "x - 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 qed
```
```   167
```
```   168 lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"
```
```   169 proof -
```
```   170   assume "x \<in> zEven" and "0 \<le> x"
```
```   171   from `x \<in> zEven` obtain a where "x = 2 * a" ..
```
```   172   with `0 \<le> x` have "0 \<le> a" by simp
```
```   173   from `0 \<le> x` and `x = 2 * a` have "nat x = nat (2 * a)"
```
```   174     by simp
```
```   175   also from `x = 2 * a` have "nat (2 * a) = 2 * nat a"
```
```   176     by (simp add: nat_mult_distrib)
```
```   177   finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
```
```   178     by simp
```
```   179   also have "... = ((-1::int)^2)^ (nat a)"
```
```   180     by (simp add: zpower_zpower [symmetric])
```
```   181   also have "(-1::int)^2 = 1"
```
```   182     by simp
```
```   183   finally show ?thesis
```
```   184     by simp
```
```   185 qed
```
```   186
```
```   187 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"
```
```   188 proof -
```
```   189   assume "x \<in> zOdd" and "0 \<le> x"
```
```   190   from `x \<in> zOdd` obtain a where "x = 2 * a + 1" ..
```
```   191   with `0 \<le> x` have a: "0 \<le> a" by simp
```
```   192   with `0 \<le> x` and `x = 2 * a + 1` have "nat x = nat (2 * a + 1)"
```
```   193     by simp
```
```   194   also from a have "nat (2 * a + 1) = 2 * nat a + 1"
```
```   195     by (auto simp add: nat_mult_distrib nat_add_distrib)
```
```   196   finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
```
```   197     by simp
```
```   198   also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
```
```   199     by (auto simp add: zpower_zpower [symmetric] zpower_zadd_distrib)
```
```   200   also have "(-1::int)^2 = 1"
```
```   201     by simp
```
```   202   finally show ?thesis
```
```   203     by simp
```
```   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   using even_odd_disj [of x] even_odd_disj [of y]
```
```   209   by (auto simp add: neg_one_even_power neg_one_odd_power)
```
```   210
```
```   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 proof -
```
```   217   assume "y \<in> zEven" and "x < y"
```
```   218   from `y \<in> zEven` obtain k where k: "y = 2 * k" ..
```
```   219   with `x < y` have "x < 2 * k" by simp
```
```   220   then have "x div 2 < k" by (auto simp add: div_prop1)
```
```   221   also have "k = (2 * k) div 2" by simp
```
```   222   finally have "x div 2 < 2 * k div 2" by simp
```
```   223   with k show ?thesis by simp
```
```   224 qed
```
```   225
```
```   226 lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"
```
```   227   by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq)
```
```   228
```
```   229 lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"
```
```   230   by (auto simp add: zEven_def)
```
```   231
```
```   232 (* An odd prime is greater than 2 *)
```
```   233
```
```   234 lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)"
```
```   235   apply (auto simp add: zOdd_def zprime_def)
```
```   236   apply (drule_tac x = 2 in allE)
```
```   237   using odd_iff_not_even [of p]
```
```   238   apply (auto simp add: zOdd_def zEven_def)
```
```   239   done
```
```   240
```
```   241 (* Powers of -1 and parity *)
```
```   242
```
```   243 lemma neg_one_special: "finite A ==>
```
```   244     ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
```
```   245   by (induct set: finite) auto
```
```   246
```
```   247 lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
```
```   248   by (induct n) auto
```
```   249
```
```   250 lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
```
```   251     ==> ((-1::int)^j = (-1::int)^k)"
```
```   252   using neg_one_power [of j] and insert neg_one_power [of k]
```
```   253   by (auto simp add: one_not_neg_one_mod_m zcong_sym)
```
```   254
```
```   255 end
```