moved lemmas out of Int.thy which have nothing to do with int
authorhaftmann
Thu Oct 02 11:33:06 2014 +0200 (2014-10-02)
changeset 58512dc4d76dfa8f0
parent 58511 97aec08d6f28
child 58513 0bf0cf1d3547
moved lemmas out of Int.thy which have nothing to do with int
NEWS
src/HOL/Fields.thy
src/HOL/Int.thy
src/HOL/Num.thy
src/HOL/Tools/numeral_simprocs.ML
     1.1 --- a/NEWS	Thu Oct 02 11:33:05 2014 +0200
     1.2 +++ b/NEWS	Thu Oct 02 11:33:06 2014 +0200
     1.3 @@ -32,6 +32,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
     1.8 +Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Bootstrap of listsum as special case of abstract product over lists.
    1.11  Fact rename:
    1.12      listsum_def ~> listsum.eq_foldr
     2.1 --- a/src/HOL/Fields.thy	Thu Oct 02 11:33:05 2014 +0200
     2.2 +++ b/src/HOL/Fields.thy	Thu Oct 02 11:33:06 2014 +0200
     2.3 @@ -375,6 +375,9 @@
     2.4    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
     2.5    by (simp add: field_simps)
     2.6  
     2.7 +lemma divide_minus1 [simp]: "x / - 1 = - x"
     2.8 +  using nonzero_minus_divide_right [of "1" x] by simp
     2.9 +  
    2.10  end
    2.11  
    2.12  class field_inverse_zero = field +
     3.1 --- a/src/HOL/Int.thy	Thu Oct 02 11:33:05 2014 +0200
     3.2 +++ b/src/HOL/Int.thy	Thu Oct 02 11:33:06 2014 +0200
     3.3 @@ -1217,21 +1217,6 @@
     3.4    divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
     3.5    le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
     3.6  
     3.7 -text{*Division By @{text "-1"}*}
     3.8 -
     3.9 -lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
    3.10 -  unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
    3.11 -  by simp
    3.12 -
    3.13 -lemma half_gt_zero_iff:
    3.14 -  "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
    3.15 -  by auto
    3.16 -
    3.17 -lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
    3.18 -
    3.19 -lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
    3.20 -  by (fact divide_numeral_1)
    3.21 -
    3.22  
    3.23  subsection {* The divides relation *}
    3.24  
     4.1 --- a/src/HOL/Num.thy	Thu Oct 02 11:33:05 2014 +0200
     4.2 +++ b/src/HOL/Num.thy	Thu Oct 02 11:33:06 2014 +0200
     4.3 @@ -1073,6 +1073,22 @@
     4.4  lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
     4.5  
     4.6  
     4.7 +subsection {* Particular lemmas concerning @{term 2} *}
     4.8 +
     4.9 +context linordered_field_inverse_zero
    4.10 +begin
    4.11 +
    4.12 +lemma half_gt_zero_iff:
    4.13 +  "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
    4.14 +  by (auto simp add: field_simps)
    4.15 +
    4.16 +lemma half_gt_zero [simp]:
    4.17 +  "0 < a \<Longrightarrow> 0 < a / 2"
    4.18 +  by (simp add: half_gt_zero_iff)
    4.19 +
    4.20 +end
    4.21 +
    4.22 +
    4.23  subsection {* Numeral equations as default simplification rules *}
    4.24  
    4.25  declare (in numeral) numeral_One [simp]
     5.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 02 11:33:05 2014 +0200
     5.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 02 11:33:06 2014 +0200
     5.3 @@ -710,7 +710,7 @@
     5.4               name = "ord_frac_simproc", proc = proc3, identifier = []}
     5.5  
     5.6  val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
     5.7 -           @{thm "divide_Numeral1"},
     5.8 +           @{thm "divide_numeral_1"},
     5.9             @{thm "divide_zero"}, @{thm divide_zero_left},
    5.10             @{thm "divide_divide_eq_left"}, 
    5.11             @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},