Generalisations involving numerals; comparisons should now work for ennreal
authorpaulson <lp15@cam.ac.uk>
Wed May 15 12:47:15 2019 +0100 (5 days ago ago)
changeset 704544065e3b0e5bf
parent 70453 40b6bc5a4721
child 70455 f7630118814c
Generalisations involving numerals; comparisons should now work for ennreal
src/HOL/Num.thy
src/HOL/Real.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Num.thy	Tue May 14 20:35:09 2019 +0200
     1.2 +++ b/src/HOL/Num.thy	Wed May 15 12:47:15 2019 +0100
     1.3 @@ -606,11 +606,9 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsubsection \<open>Comparisons: class \<open>linordered_semidom\<close>\<close>
     1.8 +subsubsection \<open>Comparisons: class \<open>linordered_nonzero_semiring\<close>\<close>
     1.9  
    1.10 -text \<open>Could be perhaps more general than here.\<close>
    1.11 -
    1.12 -context linordered_semidom
    1.13 +context linordered_nonzero_semiring
    1.14  begin
    1.15  
    1.16  lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n"
    1.17 @@ -621,10 +619,10 @@
    1.18  qed
    1.19  
    1.20  lemma one_le_numeral: "1 \<le> numeral n"
    1.21 -  using numeral_le_iff [of One n] by (simp add: numeral_One)
    1.22 +  using numeral_le_iff [of num.One n] by (simp add: numeral_One)
    1.23  
    1.24 -lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One"
    1.25 -  using numeral_le_iff [of n One] by (simp add: numeral_One)
    1.26 +lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> num.One"
    1.27 +  using numeral_le_iff [of n num.One] by (simp add: numeral_One)
    1.28  
    1.29  lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n"
    1.30  proof -
    1.31 @@ -634,16 +632,16 @@
    1.32  qed
    1.33  
    1.34  lemma not_numeral_less_one: "\<not> numeral n < 1"
    1.35 -  using numeral_less_iff [of n One] by (simp add: numeral_One)
    1.36 +  using numeral_less_iff [of n num.One] by (simp add: numeral_One)
    1.37  
    1.38 -lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> One < n"
    1.39 -  using numeral_less_iff [of One n] by (simp add: numeral_One)
    1.40 +lemma one_less_numeral_iff: "1 < numeral n \<longleftrightarrow> num.One < n"
    1.41 +  using numeral_less_iff [of num.One n] by (simp add: numeral_One)
    1.42  
    1.43  lemma zero_le_numeral: "0 \<le> numeral n"
    1.44 -  by (induct n) (simp_all add: numeral.simps)
    1.45 +  using dual_order.trans one_le_numeral zero_le_one by blast
    1.46  
    1.47  lemma zero_less_numeral: "0 < numeral n"
    1.48 -  by (induct n) (simp_all add: numeral.simps add_pos_pos)
    1.49 +  using less_linear not_numeral_less_one order.strict_trans zero_less_one by blast
    1.50  
    1.51  lemma not_numeral_le_zero: "\<not> numeral n \<le> 0"
    1.52    by (simp add: not_le zero_less_numeral)
     2.1 --- a/src/HOL/Real.thy	Tue May 14 20:35:09 2019 +0200
     2.2 +++ b/src/HOL/Real.thy	Wed May 15 12:47:15 2019 +0100
     2.3 @@ -1261,7 +1261,7 @@
     2.4        @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
     2.5        @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
     2.6        @{thm of_int_mult}, @{thm of_int_of_nat_eq},
     2.7 -      @{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}]
     2.8 +      @{thm of_nat_numeral}, @{thm of_int_numeral}, @{thm of_int_neg_numeral}]
     2.9    #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> real\<close>)
    2.10    #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_int\<close>, \<^typ>\<open>int \<Rightarrow> real\<close>))
    2.11  \<close>
     3.1 --- a/src/HOL/Transcendental.thy	Tue May 14 20:35:09 2019 +0200
     3.2 +++ b/src/HOL/Transcendental.thy	Wed May 15 12:47:15 2019 +0100
     3.3 @@ -2771,8 +2771,8 @@
     3.4    using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
     3.5    by (auto simp: field_simps powr_minus)
     3.6  
     3.7 -lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
     3.8 -  by (metis of_nat_numeral powr_realpow)
     3.9 +lemma powr_numeral [simp]: "0 \<le> x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
    3.10 +  by (metis less_le power_zero_numeral powr_0 of_nat_numeral powr_realpow)
    3.11  
    3.12  lemma powr_int:
    3.13    assumes "x > 0"