# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1557920835 -3600
# Node ID 4065e3b0e5bfeb66a1af03f85ee64cc93e62564f
# Parent  40b6bc5a47214db1c0dae91b7f3d3a83aa0e920e
Generalisations involving numerals; comparisons should now work for ennreal

diff -r 40b6bc5a4721 -r 4065e3b0e5bf src/HOL/Num.thy
--- 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)
diff -r 40b6bc5a4721 -r 4065e3b0e5bf src/HOL/Real.thy
--- 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>
diff -r 40b6bc5a4721 -r 4065e3b0e5bf src/HOL/Transcendental.thy
--- 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"