# HG changeset patch
# User haftmann
# Date 1413267803 -7200
# Node ID a478a0742a8e671fb03e2f254b279ada5906ac80
# Parent  6b2fa479945fa4cf1e743fa6b124be52171bc379
legacy cleanup

diff -r 6b2fa479945f -r a478a0742a8e src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Oct 14 08:23:23 2014 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Oct 14 08:23:23 2014 +0200
@@ -3608,9 +3608,8 @@
     }
     moreover
     {
-      assume on: "odd n"
-      from on obtain m where m: "n = 2*m + 1"
-        unfolding odd_nat_equiv_def2 by (auto simp add: mult_2)
+      assume "odd n"
+      then obtain m where m: "n = 2 * m + 1" ..
       have "?l $n = ?r$n"
         by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
           power_mult power_minus [of "c ^ 2"])
diff -r 6b2fa479945f -r a478a0742a8e src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
+++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
@@ -183,7 +183,7 @@
 where
   "odd a \<equiv> \<not> even a"
 
-lemma odd_dvdE [elim?]:
+lemma oddE [elim?]:
   assumes "odd a"
   obtains b where "a = 2 * b + 1"
 proof -
@@ -291,26 +291,6 @@
 
 subsubsection {* Legacy cruft *}
 
-lemma even_plus_even:
-  "even (x::int) ==> even y ==> even (x + y)"
-  by simp
-
-lemma odd_plus_odd:
-  "odd (x::int) ==> odd y ==> even (x + y)"
-  by simp
-
-lemma even_sum_nat:
-  "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"
-  by auto
-
-lemma odd_pow:
-  "odd x ==> odd((x::int)^n)"
-  by simp
-
-lemma even_equiv_def:
-  "even (x::int) = (EX y. x = 2 * y)"
-  by presburger
-
 
 subsubsection {* Equivalent definitions *}
 
@@ -361,9 +341,6 @@
 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_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
-  by presburger
-
 
 subsubsection {* Parity and powers *}
 
@@ -386,11 +363,9 @@
   apply (rule zero_le_square)
   done
 
-lemma zero_le_odd_power: "odd n ==>
-    (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
-apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
-apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
-done
+lemma zero_le_odd_power:
+  "odd n \<Longrightarrow> 0 \<le> (x::'a::{linordered_idom}) ^ n \<longleftrightarrow> 0 \<le> x"
+  by (erule oddE) (auto simp: power_add zero_le_mult_iff mult_2 order_antisym_conv)
 
 lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
     (even n | (odd n & 0 <= x))"
@@ -525,8 +500,7 @@
   thus ?thesis by (simp add: zero_le_even_power even)
 next
   assume odd: "odd n"
-  then obtain k where "n = Suc(2*k)"
-    by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
+  then obtain k where "n = 2 * k + 1" ..
   moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
     by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   ultimately show ?thesis
diff -r 6b2fa479945f -r a478a0742a8e src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Oct 14 08:23:23 2014 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Oct 14 08:23:23 2014 +0200
@@ -25,7 +25,7 @@
 lemma emep1:
   fixes n d :: int
   shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
-  by (auto simp add: pos_zmod_mult_2 add.commute even_equiv_def)
+  by (auto simp add: pos_zmod_mult_2 add.commute even_def dvd_def)
 
 lemma int_mod_ge:
   "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
diff -r 6b2fa479945f -r a478a0742a8e src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Tue Oct 14 08:23:23 2014 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Tue Oct 14 08:23:23 2014 +0200
@@ -142,16 +142,8 @@
 lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
 lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
 
-lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith
-
-lemma emep1:
-  "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
-  apply (simp add: add.commute)
-  apply (safe dest!: even_equiv_def [THEN iffD1])
-  apply (subst pos_zmod_mult_2)
-   apply arith
-  apply (simp add: mod_mult_mult1)
- done
+lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
+  by arith
 
 lemmas eme1p = emep1 [simplified add.commute]
 
@@ -165,9 +157,6 @@
 lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]
 lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]
 
-lemma z1pmod2:
-  "(2 * b + 1) mod 2 = (1::int)" by arith
-  
 lemma z1pdiv2:
   "(2 * b + 1) div 2 = (b::int)" by arith
 
@@ -256,7 +245,7 @@
 lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
 
 lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
-  by (fact zmod_le_nonneg_dividend) (* FIXME: delete *)
+  by (fact Divides.semiring_numeral_div_class.mod_less_eq_dividend) (* FIXME: delete *)
 
 lemma mod_add_if_z:
   "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>