legacy cleanup
authorhaftmann
Tue Oct 14 08:23:23 2014 +0200 (2014-10-14)
changeset 58681a478a0742a8e
parent 58680 6b2fa479945f
child 58682 542fa5093ebf
legacy cleanup
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Parity.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Oct 14 08:23:23 2014 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Oct 14 08:23:23 2014 +0200
     1.3 @@ -3608,9 +3608,8 @@
     1.4      }
     1.5      moreover
     1.6      {
     1.7 -      assume on: "odd n"
     1.8 -      from on obtain m where m: "n = 2*m + 1"
     1.9 -        unfolding odd_nat_equiv_def2 by (auto simp add: mult_2)
    1.10 +      assume "odd n"
    1.11 +      then obtain m where m: "n = 2 * m + 1" ..
    1.12        have "?l $n = ?r$n"
    1.13          by (simp add: m fps_sin_def fps_cos_def power_mult_distrib
    1.14            power_mult power_minus [of "c ^ 2"])
     2.1 --- a/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     2.2 +++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     2.3 @@ -183,7 +183,7 @@
     2.4  where
     2.5    "odd a \<equiv> \<not> even a"
     2.6  
     2.7 -lemma odd_dvdE [elim?]:
     2.8 +lemma oddE [elim?]:
     2.9    assumes "odd a"
    2.10    obtains b where "a = 2 * b + 1"
    2.11  proof -
    2.12 @@ -291,26 +291,6 @@
    2.13  
    2.14  subsubsection {* Legacy cruft *}
    2.15  
    2.16 -lemma even_plus_even:
    2.17 -  "even (x::int) ==> even y ==> even (x + y)"
    2.18 -  by simp
    2.19 -
    2.20 -lemma odd_plus_odd:
    2.21 -  "odd (x::int) ==> odd y ==> even (x + y)"
    2.22 -  by simp
    2.23 -
    2.24 -lemma even_sum_nat:
    2.25 -  "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"
    2.26 -  by auto
    2.27 -
    2.28 -lemma odd_pow:
    2.29 -  "odd x ==> odd((x::int)^n)"
    2.30 -  by simp
    2.31 -
    2.32 -lemma even_equiv_def:
    2.33 -  "even (x::int) = (EX y. x = 2 * y)"
    2.34 -  by presburger
    2.35 -
    2.36  
    2.37  subsubsection {* Equivalent definitions *}
    2.38  
    2.39 @@ -361,9 +341,6 @@
    2.40  lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==>
    2.41      Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger
    2.42  
    2.43 -lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
    2.44 -  by presburger
    2.45 -
    2.46  
    2.47  subsubsection {* Parity and powers *}
    2.48  
    2.49 @@ -386,11 +363,9 @@
    2.50    apply (rule zero_le_square)
    2.51    done
    2.52  
    2.53 -lemma zero_le_odd_power: "odd n ==>
    2.54 -    (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
    2.55 -apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
    2.56 -apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
    2.57 -done
    2.58 +lemma zero_le_odd_power:
    2.59 +  "odd n \<Longrightarrow> 0 \<le> (x::'a::{linordered_idom}) ^ n \<longleftrightarrow> 0 \<le> x"
    2.60 +  by (erule oddE) (auto simp: power_add zero_le_mult_iff mult_2 order_antisym_conv)
    2.61  
    2.62  lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
    2.63      (even n | (odd n & 0 <= x))"
    2.64 @@ -525,8 +500,7 @@
    2.65    thus ?thesis by (simp add: zero_le_even_power even)
    2.66  next
    2.67    assume odd: "odd n"
    2.68 -  then obtain k where "n = Suc(2*k)"
    2.69 -    by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
    2.70 +  then obtain k where "n = 2 * k + 1" ..
    2.71    moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
    2.72      by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
    2.73    ultimately show ?thesis
     3.1 --- a/src/HOL/Word/Misc_Numeric.thy	Tue Oct 14 08:23:23 2014 +0200
     3.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Tue Oct 14 08:23:23 2014 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4  lemma emep1:
     3.5    fixes n d :: int
     3.6    shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
     3.7 -  by (auto simp add: pos_zmod_mult_2 add.commute even_equiv_def)
     3.8 +  by (auto simp add: pos_zmod_mult_2 add.commute even_def dvd_def)
     3.9  
    3.10  lemma int_mod_ge:
    3.11    "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
     4.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Tue Oct 14 08:23:23 2014 +0200
     4.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Tue Oct 14 08:23:23 2014 +0200
     4.3 @@ -142,16 +142,8 @@
     4.4  lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
     4.5  lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
     4.6  
     4.7 -lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1" by arith
     4.8 -
     4.9 -lemma emep1:
    4.10 -  "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
    4.11 -  apply (simp add: add.commute)
    4.12 -  apply (safe dest!: even_equiv_def [THEN iffD1])
    4.13 -  apply (subst pos_zmod_mult_2)
    4.14 -   apply arith
    4.15 -  apply (simp add: mod_mult_mult1)
    4.16 - done
    4.17 +lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
    4.18 +  by arith
    4.19  
    4.20  lemmas eme1p = emep1 [simplified add.commute]
    4.21  
    4.22 @@ -165,9 +157,6 @@
    4.23  lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]
    4.24  lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]
    4.25  
    4.26 -lemma z1pmod2:
    4.27 -  "(2 * b + 1) mod 2 = (1::int)" by arith
    4.28 -  
    4.29  lemma z1pdiv2:
    4.30    "(2 * b + 1) div 2 = (b::int)" by arith
    4.31  
    4.32 @@ -256,7 +245,7 @@
    4.33  lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
    4.34  
    4.35  lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
    4.36 -  by (fact zmod_le_nonneg_dividend) (* FIXME: delete *)
    4.37 +  by (fact Divides.semiring_numeral_div_class.mod_less_eq_dividend) (* FIXME: delete *)
    4.38  
    4.39  lemma mod_add_if_z:
    4.40    "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>