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