# HG changeset patch
# User haftmann
# Date 1412242386 -7200
# Node ID dc4d76dfa8f0b6b5d8a8c3757136d0fd45c916d3
# Parent  97aec08d6f286b93ac99a4749d952263bd3c971a
moved lemmas out of Int.thy which have nothing to do with int

diff -r 97aec08d6f28 -r dc4d76dfa8f0 NEWS
--- a/NEWS	Thu Oct 02 11:33:05 2014 +0200
+++ b/NEWS	Thu Oct 02 11:33:06 2014 +0200
@@ -32,6 +32,9 @@
 
 *** HOL ***
 
+* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
+Minor INCOMPATIBILITY.
+
 * Bootstrap of listsum as special case of abstract product over lists.
 Fact rename:
     listsum_def ~> listsum.eq_foldr
diff -r 97aec08d6f28 -r dc4d76dfa8f0 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Oct 02 11:33:05 2014 +0200
+++ b/src/HOL/Fields.thy	Thu Oct 02 11:33:06 2014 +0200
@@ -375,6 +375,9 @@
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
   by (simp add: field_simps)
 
+lemma divide_minus1 [simp]: "x / - 1 = - x"
+  using nonzero_minus_divide_right [of "1" x] by simp
+  
 end
 
 class field_inverse_zero = field +
diff -r 97aec08d6f28 -r dc4d76dfa8f0 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 02 11:33:05 2014 +0200
+++ b/src/HOL/Int.thy	Thu Oct 02 11:33:06 2014 +0200
@@ -1217,21 +1217,6 @@
   divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
 
-text{*Division By @{text "-1"}*}
-
-lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
-  unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
-  by simp
-
-lemma half_gt_zero_iff:
-  "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
-  by auto
-
-lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
-
-lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
-  by (fact divide_numeral_1)
-
 
 subsection {* The divides relation *}
 
diff -r 97aec08d6f28 -r dc4d76dfa8f0 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Oct 02 11:33:05 2014 +0200
+++ b/src/HOL/Num.thy	Thu Oct 02 11:33:06 2014 +0200
@@ -1073,6 +1073,22 @@
 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
 
 
+subsection {* Particular lemmas concerning @{term 2} *}
+
+context linordered_field_inverse_zero
+begin
+
+lemma half_gt_zero_iff:
+  "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
+  by (auto simp add: field_simps)
+
+lemma half_gt_zero [simp]:
+  "0 < a \<Longrightarrow> 0 < a / 2"
+  by (simp add: half_gt_zero_iff)
+
+end
+
+
 subsection {* Numeral equations as default simplification rules *}
 
 declare (in numeral) numeral_One [simp]
diff -r 97aec08d6f28 -r dc4d76dfa8f0 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 02 11:33:05 2014 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 02 11:33:06 2014 +0200
@@ -710,7 +710,7 @@
              name = "ord_frac_simproc", proc = proc3, identifier = []}
 
 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
-           @{thm "divide_Numeral1"},
+           @{thm "divide_numeral_1"},
            @{thm "divide_zero"}, @{thm divide_zero_left},
            @{thm "divide_divide_eq_left"}, 
            @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},