# HG changeset patch # User haftmann # Date 1413480373 -7200 # Node ID 5469874b0228a92e49bd818eadc932b32ab722d4 # Parent 15e5b44d5ed23d16b419625ea0b4077a3546a33e even more cleanup diff -r 15e5b44d5ed2 -r 5469874b0228 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu Oct 16 11:56:46 2014 +0200 +++ b/src/HOL/Parity.thy Thu Oct 16 19:26:13 2014 +0200 @@ -19,6 +19,20 @@ "2 dvd Suc n \ \ 2 dvd n" by (induct n) auto +lemma two_dvd_diff_nat_iff: + fixes m n :: nat + shows "2 dvd m - n \ m < n \ 2 dvd m + n" +proof (cases "n \ m") + case True + then have "m - n + n * 2 = m + n" by simp + moreover have "2 dvd m - n \ 2 dvd m - n + n * 2" by simp + ultimately have "2 dvd m - n \ 2 dvd m + n" by (simp only:) + then show ?thesis by auto +next + case False + then show ?thesis by simp +qed + lemma two_dvd_diff_iff: fixes k l :: int shows "2 dvd k - l \ 2 dvd k + l" @@ -267,79 +281,93 @@ end -subsubsection {* Particularities for @{typ nat}/@{typ int} *} +subsubsection {* Particularities for @{typ nat} and @{typ int} *} + +lemma even_Suc [simp, presburger, algebra]: + "even (Suc n) = odd n" + by (simp add: even_def two_dvd_Suc_iff) + +lemma even_diff_nat [simp]: + fixes m n :: nat + shows "even (m - n) \ m < n \ even (m + n)" + by (simp add: even_def two_dvd_diff_nat_iff) lemma even_int_iff: "even (int n) \ even n" by (simp add: even_def dvd_int_iff) +lemma even_nat_iff: + "0 \ k \ even (nat k) \ even k" + by (simp add: even_int_iff [symmetric]) + + +subsubsection {* Tools setup *} + declare transfer_morphism_int_nat [transfer add return: even_int_iff ] - -subsubsection {* Tools setup *} - lemma [presburger]: "even n \ even (int n)" using even_int_iff [of n] by simp -lemma [presburger]: +lemma (in semiring_parity) [presburger]: "even (a + b) \ even a \ even b \ odd a \ odd b" by auto +lemma [presburger, algebra]: + fixes m n :: nat + shows "even (m - n) \ m < n \ even m \ even n \ odd m \ odd n" + by auto + +lemma [presburger, algebra]: + fixes m n :: nat + shows "even (m ^ n) \ even m \ 0 < n" + by simp + +lemma [presburger]: + fixes k :: int + shows "(k + 1) div 2 = k div 2 \ even k" + by presburger + +lemma [presburger]: + fixes k :: int + shows "(k + 1) div 2 = k div 2 + 1 \ odd k" + by presburger + +lemma [presburger]: + "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \ even n" + by presburger + subsubsection {* Legacy cruft *} subsubsection {* Equivalent definitions *} -lemma two_times_even_div_two: - "even (x::int) ==> 2 * (x div 2) = x" +lemma even_nat_mod_two_eq_zero: + "even (x::nat) ==> x mod Suc (Suc 0) = 0" by presburger -lemma two_times_odd_div_two_plus_one: - "odd (x::int) ==> 2 * (x div 2) + 1 = x" - by presburger - - -subsubsection {* even and odd for nats *} - -lemma pos_int_even_equiv_nat_even: "0 \ x ==> even x = even (nat x)" -by (simp add: even_int_iff [symmetric]) - -lemma even_difference_nat [simp,presburger,algebra]: - "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))" +lemma odd_nat_mod_two_eq_one: + "odd (x::nat) ==> x mod Suc (Suc 0) = Suc 0" by presburger -lemma even_Suc [simp ,presburger, algebra]: - "even (Suc x) = odd x" +lemma even_nat_equiv_def: + "even (x::nat) = (x mod Suc (Suc 0) = 0)" by presburger -lemma even_power_nat[simp,presburger,algebra]: - "even ((x::nat)^y) = (even x & 0 < y)" - by simp - - -subsubsection {* Equivalent definitions *} - -lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" -by presburger +lemma odd_nat_equiv_def: + "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" + by presburger -lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" -by presburger - -lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" -by presburger +lemma even_nat_div_two_times_two: + "even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x" + by presburger -lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" -by presburger - -lemma even_nat_div_two_times_two: "even (x::nat) ==> - Suc (Suc 0) * (x div Suc (Suc 0)) = x" by presburger - -lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> - Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger +lemma odd_nat_div_two_times_two_plus_one: + "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x" + by presburger subsubsection {* Parity and powers *} @@ -452,12 +480,13 @@ lemma even_mult_two_ex: "even(n) = (\m::nat. n = 2*m)" by presburger lemma odd_Suc_mult_two_ex: "odd(n) = (\m. n = Suc (2*m))" by presburger -lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger +lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" + by presburger -lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)" -by presburger +lemma lemma_odd_div2 [simp]: "odd n ==> (n + 1) div 2 = Suc (n div 2)" + by presburger -lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))" by presburger +lemma even_num_iff: "0 < n ==> even n = (odd (n - 1 :: nat))" by presburger lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)" by presburger lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)" by presburger @@ -510,17 +539,13 @@ subsubsection {* Miscellaneous *} -lemma [presburger]:"(x + 1) div 2 = x div 2 \ even (x::int)" by presburger -lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \ odd (x::int)" by presburger -lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" by presburger -lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger +lemma even_nat_plus_one_div_two: + "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" + by presburger -lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \ even x" by presburger -lemma even_nat_plus_one_div_two: "even (x::nat) ==> - (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger - -lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> - (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger +lemma odd_nat_plus_one_div_two: + "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" + by presburger end