--- a/src/HOL/Num.thy Tue May 14 20:35:09 2019 +0200
+++ b/src/HOL/Num.thy Wed May 15 12:47:15 2019 +0100
@@ -606,11 +606,9 @@
end
-subsubsection \<open>Comparisons: class \<open>linordered_semidom\<close>\<close>
+subsubsection \<open>Comparisons: class \<open>linordered_nonzero_semiring\<close>\<close>
-text \<open>Could be perhaps more general than here.\<close>
-
-context linordered_semidom
+context linordered_nonzero_semiring
begin
lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n"
@@ -621,10 +619,10 @@
qed
lemma one_le_numeral: "1 \<le> numeral n"
- using numeral_le_iff [of One n] by (simp add: numeral_One)
+ using numeral_le_iff [of num.One n] by (simp add: numeral_One)
-lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One"
- using numeral_le_iff [of n One] by (simp add: numeral_One)
+lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> num.One"
+ using numeral_le_iff [of n num.One] by (simp add: numeral_One)
lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n"
proof -
@@ -634,16 +632,16 @@
qed
lemma not_numeral_less_one: "\<not> numeral n < 1"
- using numeral_less_iff [of n One] by (simp add: numeral_One)
+ using numeral_less_iff [of n num.One] by (simp add: numeral_One)
-lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n"
- using numeral_less_iff [of One n] by (simp add: numeral_One)
+lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> num.One < n"
+ using numeral_less_iff [of num.One n] by (simp add: numeral_One)
lemma zero_le_numeral: "0 \<le> numeral n"
- by (induct n) (simp_all add: numeral.simps)
+ using dual_order.trans one_le_numeral zero_le_one by blast
lemma zero_less_numeral: "0 < numeral n"
- by (induct n) (simp_all add: numeral.simps add_pos_pos)
+ using less_linear not_numeral_less_one order.strict_trans zero_less_one by blast
lemma not_numeral_le_zero: "\<not> numeral n \<le> 0"
by (simp add: not_le zero_less_numeral)
--- a/src/HOL/Real.thy Tue May 14 20:35:09 2019 +0200
+++ b/src/HOL/Real.thy Wed May 15 12:47:15 2019 +0100
@@ -1261,7 +1261,7 @@
@{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
@{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
@{thm of_int_mult}, @{thm of_int_of_nat_eq},
- @{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}]
+ @{thm of_nat_numeral}, @{thm of_int_numeral}, @{thm of_int_neg_numeral}]
#> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
#> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> real\<close>))
\<close>
--- a/src/HOL/Transcendental.thy Tue May 14 20:35:09 2019 +0200
+++ b/src/HOL/Transcendental.thy Wed May 15 12:47:15 2019 +0100
@@ -2771,8 +2771,8 @@
using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
by (auto simp: field_simps powr_minus)
-lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
- by (metis of_nat_numeral powr_realpow)
+lemma powr_numeral [simp]: "0 \<le> x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
+ by (metis less_le power_zero_numeral powr_0 of_nat_numeral powr_realpow)
lemma powr_int:
assumes "x > 0"