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