--- 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
--- 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 +
--- 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 *}
--- 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]
--- 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"},