# HG changeset patch
# User haftmann
# Date 1413480388 -7200
# Node ID 68f8d22a68676bd98010b374a1fc87f375eb2c44
# Parent  5c5c148447384525045938bfe5ab2ed16355cd83
tuned

diff -r 5c5c14844738 -r 68f8d22a6867 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Oct 16 19:26:27 2014 +0200
+++ b/src/HOL/Parity.thy	Thu Oct 16 19:26:28 2014 +0200
@@ -514,6 +514,14 @@
 
 subsubsection {* Miscellaneous *}
 
+lemma even_mult_two_ex:
+  "even(n) = (\<exists>m::nat. n = 2*m)"
+  by presburger
+
+lemma odd_Suc_mult_two_ex:
+  "odd(n) = (\<exists>m. n = Suc (2*m))"
+  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
@@ -546,21 +554,28 @@
   "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x"
   by presburger
 
-lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger
-lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>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"
+lemma lemma_odd_div2 [simp]:
+  "odd 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)"
+lemma even_num_iff:
+  "0 < n ==> even n = (odd (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 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
+lemma lemma_odd_mod_4_div_2:
+  "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
+  by presburger
 
-lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
+lemma lemma_even_mod_4_div_2:
+  "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
   by presburger
 
 end