# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1746199538 -3600
# Node ID c0587d661ea826b0eec053b6601c82f2e1adbd97
# Parent  0af7fe946bfd9543697a6736ce244f1b2e004060
Tweaking the ordered semiring type classes

diff -r 0af7fe946bfd -r c0587d661ea8 src/HOL/Nat.thy
--- 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)
 
diff -r 0af7fe946bfd -r c0587d661ea8 src/HOL/Power.thy
--- 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"
diff -r 0af7fe946bfd -r c0587d661ea8 src/HOL/Rings.thy
--- 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)
diff -r 0af7fe946bfd -r c0587d661ea8 src/HOL/Vector_Spaces.thy
--- 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"