src/HOL/Parity.thy
changeset 58710 7216a10d69ba
parent 58709 efdc6c533bd3
child 58711 3f7886cd75b9
     1.1 --- a/src/HOL/Parity.thy	Sun Oct 19 18:05:26 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Mon Oct 20 07:45:58 2014 +0200
     1.3 @@ -279,13 +279,45 @@
     1.4  
     1.5  end
     1.6  
     1.7 +
     1.8 +subsubsection {* Parity and division *}
     1.9 +
    1.10  context semiring_div_parity
    1.11  begin
    1.12  
    1.13 +lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
    1.14 +  "1 div 2 = 0"
    1.15 +proof (cases "2 = 0")
    1.16 +  case True then show ?thesis by simp
    1.17 +next
    1.18 +  case False
    1.19 +  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
    1.20 +  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
    1.21 +  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
    1.22 +  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
    1.23 +  with False show ?thesis by auto
    1.24 +qed
    1.25 +
    1.26  lemma even_iff_mod_2_eq_zero [presburger]:
    1.27    "even a \<longleftrightarrow> a mod 2 = 0"
    1.28    by (simp add: even_def dvd_eq_mod_eq_0)
    1.29  
    1.30 +lemma even_succ_div_two [simp]:
    1.31 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    1.32 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
    1.33 +
    1.34 +lemma odd_succ_div_two [simp]:
    1.35 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
    1.36 +  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    1.37 +
    1.38 +lemma even_two_times_div_two:
    1.39 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
    1.40 +  by (rule dvd_mult_div_cancel) (simp add: even_def)
    1.41 +
    1.42 +lemma odd_two_times_div_two_succ:
    1.43 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
    1.44 +  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
    1.45 +  
    1.46  end
    1.47  
    1.48  
    1.49 @@ -312,8 +344,37 @@
    1.50    "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
    1.51    by (simp add: even_int_iff [symmetric])
    1.52  
    1.53 +lemma even_num_iff:
    1.54 +  "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
    1.55 +  by simp
    1.56  
    1.57 -subsubsection {* Parity and powers *}
    1.58 +lemma even_Suc_div_two [simp]:
    1.59 +  "even n \<Longrightarrow> Suc n div 2 = n div 2"
    1.60 +  using even_succ_div_two [of n] by simp
    1.61 +  
    1.62 +lemma odd_Suc_div_two [simp]:
    1.63 +  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
    1.64 +  using odd_succ_div_two [of n] by simp
    1.65 +
    1.66 +lemma odd_two_times_div_two_Suc:
    1.67 +  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
    1.68 +  using odd_two_times_div_two_succ [of n] by simp
    1.69 +  
    1.70 +text {* Nice facts about division by @{term 4} *}  
    1.71 +
    1.72 +lemma even_even_mod_4_iff:
    1.73 +  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
    1.74 +  by presburger
    1.75 +
    1.76 +lemma odd_mod_4_div_2:
    1.77 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
    1.78 +  by presburger
    1.79 +
    1.80 +lemma even_mod_4_div_2:
    1.81 +  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    1.82 +  by presburger
    1.83 +  
    1.84 +text {* Parity and powers *}
    1.85  
    1.86  context comm_ring_1
    1.87  begin
    1.88 @@ -370,7 +431,7 @@
    1.89    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
    1.90    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
    1.91  
    1.92 -lemma zero_le_power_iff [presburger]:
    1.93 +lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. zero_le_power_eq\<close>
    1.94    "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
    1.95  proof (cases "even n")
    1.96    case True
    1.97 @@ -385,7 +446,7 @@
    1.98      by (auto simp add: zero_le_mult_iff zero_le_even_power)
    1.99  qed
   1.100  
   1.101 -lemma zero_le_power_eq [presburger]: -- \<open>FIXME weaker version of @{text zero_le_power_iff}\<close>
   1.102 +lemma zero_le_power_eq [presburger]:
   1.103    "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   1.104    using zero_le_power_iff [of a n] by auto
   1.105  
   1.106 @@ -395,7 +456,7 @@
   1.107    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
   1.108      unfolding power_eq_0_iff' [of a n, symmetric] by blast
   1.109    show ?thesis
   1.110 -  unfolding less_le zero_le_power_iff by auto
   1.111 +  unfolding less_le zero_le_power_eq by auto
   1.112  qed
   1.113  
   1.114  lemma power_less_zero_eq [presburger]:
   1.115 @@ -511,64 +572,5 @@
   1.116    "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
   1.117    by presburger
   1.118  
   1.119 -
   1.120 -subsubsection {* Miscellaneous *}
   1.121 -
   1.122 -lemma even_nat_plus_one_div_two:
   1.123 -  "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
   1.124 -  by presburger
   1.125 -
   1.126 -lemma odd_nat_plus_one_div_two:
   1.127 -  "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
   1.128 -  by presburger
   1.129 -
   1.130 -lemma even_nat_mod_two_eq_zero:
   1.131 -  "even (x::nat) ==> x mod Suc (Suc 0) = 0"
   1.132 -  by presburger
   1.133 -
   1.134 -lemma odd_nat_mod_two_eq_one:
   1.135 -  "odd (x::nat) ==> x mod Suc (Suc 0) = Suc 0"
   1.136 -  by presburger
   1.137 -
   1.138 -lemma even_nat_equiv_def:
   1.139 -  "even (x::nat) = (x mod Suc (Suc 0) = 0)"
   1.140 -  by presburger
   1.141 -
   1.142 -lemma odd_nat_equiv_def:
   1.143 -  "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
   1.144 -  by presburger
   1.145 -
   1.146 -lemma even_nat_div_two_times_two:
   1.147 -  "even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x"
   1.148 -  by presburger
   1.149 -
   1.150 -lemma odd_nat_div_two_times_two_plus_one:
   1.151 -  "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x"
   1.152 -  by presburger
   1.153 -
   1.154 -lemma lemma_even_div2 [simp]:
   1.155 -  "even (n::nat) ==> (n + 1) div 2 = n div 2"
   1.156 -  by presburger
   1.157 -
   1.158 -lemma lemma_odd_div2 [simp]:
   1.159 -  "odd n ==> (n + 1) div 2 = Suc (n div 2)"
   1.160 -  by presburger
   1.161 -
   1.162 -lemma even_num_iff:
   1.163 -  "0 < n ==> even n = (odd (n - 1 :: nat))"
   1.164 -  by presburger
   1.165 -
   1.166 -lemma even_even_mod_4_iff:
   1.167 -  "even (n::nat) = even (n mod 4)"
   1.168 -  by presburger
   1.169 -
   1.170 -lemma lemma_odd_mod_4_div_2:
   1.171 -  "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
   1.172 -  by presburger
   1.173 -
   1.174 -lemma lemma_even_mod_4_div_2:
   1.175 -  "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
   1.176 -  by presburger
   1.177 -
   1.178  end
   1.179