src/HOL/Parity.thy
changeset 54227 63b441f49645
parent 47225 650318981557
child 54228 229282d53781
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -11,11 +11,14 @@
     1.4  
     1.5  class even_odd = 
     1.6    fixes even :: "'a \<Rightarrow> bool"
     1.7 +begin
     1.8  
     1.9 -abbreviation
    1.10 -  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
    1.11 +abbreviation odd :: "'a \<Rightarrow> bool"
    1.12 +where
    1.13    "odd x \<equiv> \<not> even x"
    1.14  
    1.15 +end
    1.16 +
    1.17  instantiation nat and int  :: even_odd
    1.18  begin
    1.19  
    1.20 @@ -52,7 +55,7 @@
    1.21    unfolding even_def by simp
    1.22  
    1.23  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
    1.24 -declare even_def[of "neg_numeral v", simp] for v
    1.25 +declare even_def [of "neg_numeral v", simp] for v
    1.26  
    1.27  lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
    1.28    unfolding even_nat_def by simp
    1.29 @@ -62,13 +65,6 @@
    1.30  
    1.31  subsection {* Even and odd are mutually exclusive *}
    1.32  
    1.33 -lemma int_pos_lt_two_imp_zero_or_one:
    1.34 -    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
    1.35 -  by presburger
    1.36 -
    1.37 -lemma neq_one_mod_two [simp, presburger]: 
    1.38 -  "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger
    1.39 -
    1.40  
    1.41  subsection {* Behavior under integer arithmetic operations *}
    1.42  declare dvd_def[algebra]
    1.43 @@ -158,10 +154,6 @@
    1.44  
    1.45  subsection {* Equivalent definitions *}
    1.46  
    1.47 -lemma nat_lt_two_imp_zero_or_one:
    1.48 -  "(x::nat) < Suc (Suc 0) ==> x = 0 | x = Suc 0"
    1.49 -by presburger
    1.50 -
    1.51  lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
    1.52  by presburger
    1.53  
    1.54 @@ -244,7 +236,7 @@
    1.55  apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
    1.56  done
    1.57  
    1.58 -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
    1.59 +lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
    1.60      (even n | (odd n & 0 <= x))"
    1.61    apply auto
    1.62    apply (subst zero_le_odd_power [symmetric])
    1.63 @@ -277,9 +269,6 @@
    1.64    apply (simp add: zero_le_even_power)
    1.65    done
    1.66  
    1.67 -lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
    1.68 -  by (induct n) auto
    1.69 -
    1.70  lemma power_minus_even [simp]: "even n ==>
    1.71      (- x)^n = (x^n::'a::{comm_ring_1})"
    1.72    apply (subst power_minus)
    1.73 @@ -336,13 +325,6 @@
    1.74  
    1.75  lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger
    1.76  
    1.77 -lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +
    1.78 -    (a mod c + Suc 0 mod c) div c" 
    1.79 -  apply (subgoal_tac "Suc a = a + Suc 0")
    1.80 -  apply (erule ssubst)
    1.81 -  apply (rule div_add1_eq, simp)
    1.82 -  done
    1.83 -
    1.84  lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
    1.85  
    1.86  lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
    1.87 @@ -359,31 +341,29 @@
    1.88  text {* Simplify, when the exponent is a numeral *}
    1.89  
    1.90  lemmas zero_le_power_eq_numeral [simp] =
    1.91 -    zero_le_power_eq [of _ "numeral w"] for w
    1.92 +  zero_le_power_eq [of _ "numeral w"] for w
    1.93  
    1.94  lemmas zero_less_power_eq_numeral [simp] =
    1.95 -    zero_less_power_eq [of _ "numeral w"] for w
    1.96 +  zero_less_power_eq [of _ "numeral w"] for w
    1.97  
    1.98  lemmas power_le_zero_eq_numeral [simp] =
    1.99 -    power_le_zero_eq [of _ "numeral w"] for w
   1.100 +  power_le_zero_eq [of _ "numeral w"] for w
   1.101  
   1.102  lemmas power_less_zero_eq_numeral [simp] =
   1.103 -    power_less_zero_eq [of _ "numeral w"] for w
   1.104 +  power_less_zero_eq [of _ "numeral w"] for w
   1.105  
   1.106  lemmas zero_less_power_nat_eq_numeral [simp] =
   1.107 -    zero_less_power_nat_eq [of _ "numeral w"] for w
   1.108 +  nat_zero_less_power_iff [of _ "numeral w"] for w
   1.109  
   1.110 -lemmas power_eq_0_iff_numeral [simp] = power_eq_0_iff [of _ "numeral w"] for w
   1.111 +lemmas power_eq_0_iff_numeral [simp] =
   1.112 +  power_eq_0_iff [of _ "numeral w"] for w
   1.113  
   1.114 -lemmas power_even_abs_numeral [simp] = power_even_abs [of "numeral w" _] for w
   1.115 +lemmas power_even_abs_numeral [simp] =
   1.116 +  power_even_abs [of "numeral w" _] for w
   1.117  
   1.118  
   1.119  subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
   1.120  
   1.121 -lemma even_power_le_0_imp_0:
   1.122 -    "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
   1.123 -  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   1.124 -
   1.125  lemma zero_le_power_iff[presburger]:
   1.126    "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
   1.127  proof cases
   1.128 @@ -395,9 +375,10 @@
   1.129    assume odd: "odd n"
   1.130    then obtain k where "n = Suc(2*k)"
   1.131      by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
   1.132 -  thus ?thesis
   1.133 -    by (auto simp add: zero_le_mult_iff zero_le_even_power
   1.134 -             dest!: even_power_le_0_imp_0)
   1.135 +  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
   1.136 +    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   1.137 +  ultimately show ?thesis
   1.138 +    by (auto simp add: zero_le_mult_iff zero_le_even_power)
   1.139  qed
   1.140  
   1.141  
   1.142 @@ -409,7 +390,6 @@
   1.143  lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger
   1.144  
   1.145  lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
   1.146 -lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
   1.147  lemma even_nat_plus_one_div_two: "even (x::nat) ==>
   1.148      (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger
   1.149  
   1.150 @@ -417,3 +397,4 @@
   1.151      (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger
   1.152  
   1.153  end
   1.154 +