--- a/src/HOL/Nat.thy Sun Apr 27 11:21:04 2025 +0100
+++ b/src/HOL/Nat.thy Fri May 02 16:25:38 2025 +0100
@@ -1793,12 +1793,12 @@
class ring_char_0 = ring_1 + semiring_char_0
+lemma (in ordered_semiring_1) of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
+ by (induct n) simp_all
+
context linordered_nonzero_semiring
begin
-lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
- by (induct n) simp_all
-
lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
by (simp add: not_less)
--- a/src/HOL/Power.thy Sun Apr 27 11:21:04 2025 +0100
+++ b/src/HOL/Power.thy Fri May 02 16:25:38 2025 +0100
@@ -426,12 +426,9 @@
subsection \<open>Exponentiation on ordered types\<close>
-context linordered_semidom
+context ordered_semiring_1
begin
-lemma zero_less_power [simp]: "0 < a \<Longrightarrow> 0 < a ^ n"
- by (induct n) simp_all
-
lemma zero_le_power [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
by (induct n) simp_all
@@ -462,6 +459,42 @@
lemma one_less_power [simp]: "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
by (cases n) (simp_all add: power_gt1_lemma)
+text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
+lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
+proof (induct N)
+ case 0
+ then show ?case by simp
+next
+ case (Suc N)
+ then show ?case
+ using mult_mono[of 1 a "a ^ n" "a ^ N"]
+ by (auto simp add: le_Suc_eq order_trans [OF zero_le_one])
+qed
+
+text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
+lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
+proof (induction N)
+ case 0
+ then show ?case by simp
+next
+ case (Suc N)
+ then show ?case
+ using mult_mono[of a 1 "a^N" "a ^ n"]
+ by (auto simp add: le_Suc_eq)
+qed
+
+lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
+ using power_decreasing [of 1 "Suc n" a] by simp
+
+end
+
+
+context linordered_semidom
+begin
+
+lemma zero_less_power [simp]: "0 < a \<Longrightarrow> 0 < a ^ n"
+ by (induct n) simp_all
+
lemma power_le_imp_le_exp:
assumes gt1: "1 < a"
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n"
@@ -485,18 +518,6 @@
lemma of_nat_zero_less_power_iff [simp]: "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
by (induct n) auto
-
-text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
-lemma power_inject_exp [simp]:
- \<open>a ^ m = a ^ n \<longleftrightarrow> m = n\<close> if \<open>1 < a\<close>
- using that by (force simp add: order_class.order.antisym power_le_imp_le_exp)
-
-text \<open>
- Can relax the first premise to \<^term>\<open>0<a\<close> in the case of the
- natural numbers.
-\<close>
-lemma power_less_imp_less_exp: "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
- by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp)
lemma power_strict_mono: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a ^ n < b ^ n"
proof (induct n)
@@ -527,18 +548,6 @@
by (auto simp add: power_Suc_less less_Suc_eq)
qed
-text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
-lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
-proof (induction N)
- case 0
- then show ?case by simp
-next
- case (Suc N)
- then show ?case
- using mult_mono[of a 1 "a^N" "a ^ n"]
- by (auto simp add: le_Suc_eq)
-qed
-
lemma power_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m \<le> b ^ n \<longleftrightarrow> n \<le> m"
using power_strict_decreasing [of m n b]
by (auto intro: power_decreasing ccontr)
@@ -550,18 +559,6 @@
lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
using power_strict_decreasing [of 0 "Suc n" a] by simp
-text \<open>Proof again resembles that of \<open>power_strict_decreasing\<close>.\<close>
-lemma power_increasing: "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
-proof (induct N)
- case 0
- then show ?case by simp
-next
- case (Suc N)
- then show ?case
- using mult_mono[of 1 a "a ^ n" "a ^ N"]
- by (auto simp add: le_Suc_eq order_trans [OF zero_le_one])
-qed
-
text \<open>Lemma for \<open>power_strict_increasing\<close>.\<close>
lemma power_less_power_Suc: "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
by (induct n) (auto simp: mult_strict_left_mono less_trans [OF zero_less_one])
@@ -577,6 +574,23 @@
by (auto simp add: power_less_power_Suc less_Suc_eq less_trans [OF zero_less_one] less_imp_le)
qed
+text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
+lemma power_inject_exp [simp]:
+ \<open>a ^ m = a ^ n \<longleftrightarrow> m = n\<close> if \<open>1 < a\<close>
+ using that by (force simp add: order_class.order.antisym power_le_imp_le_exp)
+
+lemma power_inject_exp':
+ \<open>a ^ m = a ^ n \<longleftrightarrow> m = n\<close> if \<open>a\<noteq>1\<close> \<open>a>0\<close>
+ using that
+ by (metis linorder_neqE_nat not_less_iff_gr_or_eq power_inject_exp power_strict_decreasing)
+
+text \<open>
+ Can relax the first premise to \<^term>\<open>0<a\<close> in the case of the
+ natural numbers.
+\<close>
+lemma power_less_imp_less_exp: "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
+ by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp)
+
lemma power_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y"
by (blast intro: power_le_imp_le_exp power_increasing less_imp_le)
@@ -625,9 +639,6 @@
lemma power2_eq_imp_eq: "x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y"
unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp
-lemma power_Suc_le_self: "0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ Suc n \<le> a"
- using power_decreasing [of 1 "Suc n" a] by simp
-
lemma power2_eq_iff_nonneg [simp]:
assumes "0 \<le> x" "0 \<le> y"
shows "(x ^ 2 = y ^ 2) \<longleftrightarrow> x = y"
--- a/src/HOL/Rings.thy Sun Apr 27 11:21:04 2025 +0100
+++ b/src/HOL/Rings.thy Fri May 02 16:25:38 2025 +0100
@@ -1953,7 +1953,19 @@
end
-class ordered_semiring_1 = ordered_semiring + semiring_1 + zero_neq_one
+class zero_less_one = order + zero + one +
+ assumes zero_less_one [simp]: "0 < 1"
+begin
+
+subclass zero_neq_one
+ by standard (simp add: less_imp_neq)
+
+lemma zero_le_one [simp]:
+ \<open>0 \<le> 1\<close> by (rule less_imp_le) simp
+
+end
+
+class ordered_semiring_1 = ordered_semiring_0 + semiring_1 + zero_less_one
begin
lemma convex_bound_le:
@@ -1994,18 +2006,6 @@
end
-class zero_less_one = order + zero + one +
- assumes zero_less_one [simp]: "0 < 1"
-begin
-
-subclass zero_neq_one
- by standard (simp add: less_imp_neq)
-
-lemma zero_le_one [simp]:
- \<open>0 \<le> 1\<close> by (rule less_imp_le) simp
-
-end
-
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
@@ -2157,7 +2157,7 @@
end
-class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
+class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1 + zero_less_one
\<comment> \<open>analogous to \<^class>\<open>linordered_semiring_1_strict\<close> not requiring a total order\<close>
begin
@@ -2500,14 +2500,12 @@
assumes add_mono1: "a < b \<Longrightarrow> a + 1 < b + 1"
begin
-subclass zero_neq_one
- by standard
+subclass zero_neq_one ..
subclass comm_semiring_1
by standard (rule mult_1_left)
-lemma zero_le_one [simp]: "0 \<le> 1"
- by (rule zero_less_one [THEN less_imp_le])
+subclass ordered_semiring_1 ..
lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
by (simp add: not_le)
--- a/src/HOL/Vector_Spaces.thy Sun Apr 27 11:21:04 2025 +0100
+++ b/src/HOL/Vector_Spaces.thy Fri May 02 16:25:38 2025 +0100
@@ -717,7 +717,7 @@
vs1.representation (vs1.extend_basis B) v b *b (if b \<in> B then g b else 0))"
lemma construct_cong: "(\<And>b. b \<in> B \<Longrightarrow> f b = g b) \<Longrightarrow> construct B f = construct B g"
- unfolding construct_def by (rule ext, auto intro!: sum.cong)
+ unfolding construct_def by (auto intro!: sum.cong)
lemma linear_construct:
assumes B[simp]: "vs1.independent B"