# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1738858852 0
# Node ID 25dd3726fd001d3528468f5d0f3858d74a0dbd63
# Parent  0aa2d1c132b2291a7a6d7a32036c07cd8737961d
Minor lemma tweaking

diff -r 0aa2d1c132b2 -r 25dd3726fd00 NEWS
--- a/NEWS	Wed Feb 05 16:34:56 2025 +0000
+++ b/NEWS	Thu Feb 06 16:20:52 2025 +0000
@@ -343,6 +343,8 @@
 * Theory "HOL-Library.Suc_Notation" provides compact notation for
 iterated Suc terms.
 
+* Theory "HOL.Nat": of_nat_diff is now a simprule, minor INCOMPATIBILITY.
+
 * Theory "HOL-Library.Adhoc_Overloading" has been moved to Pure. Minor
 INCOMPATIBILITY: need to adjust theory imports.
 
diff -r 0aa2d1c132b2 -r 25dd3726fd00 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Wed Feb 05 16:34:56 2025 +0000
+++ b/src/HOL/Groups_List.thy	Thu Feb 06 16:20:52 2025 +0000
@@ -203,15 +203,15 @@
 
 lemma sum_list_eq_0_iff [simp]:
   "sum_list ns = 0 \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
-by (simp add: sum_list_nonneg_eq_0_iff)
+  by (simp add: sum_list_nonneg_eq_0_iff)
 
 lemma member_le_sum_list:
   "x \<in> set xs \<Longrightarrow> x \<le> sum_list xs"
-by (induction xs) (auto simp: add_increasing add_increasing2)
+  by (induction xs) (auto simp: add_increasing add_increasing2)
 
 lemma elem_le_sum_list:
   "k < size ns \<Longrightarrow> ns ! k \<le> sum_list (ns)"
-by (rule member_le_sum_list) simp
+  by (simp add: member_le_sum_list)
 
 end
 
@@ -379,6 +379,7 @@
   thus ?case by simp
 qed
 
+(*Note that we also have this for class canonically_ordered_monoid_add*)
 lemma member_le_sum_list:
   fixes x :: "'a :: ordered_comm_monoid_add"
   assumes "x \<in> set xs" "\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0"
diff -r 0aa2d1c132b2 -r 25dd3726fd00 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 05 16:34:56 2025 +0000
+++ b/src/HOL/Nat.thy	Thu Feb 06 16:20:52 2025 +0000
@@ -1268,7 +1268,7 @@
 
 lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0"
   for m n :: nat
-  by (rule iffD2, rule diff_is_0_eq)
+  by simp
 
 lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n"
   for m n :: nat
@@ -1755,6 +1755,9 @@
     by simp
 qed
 
+lemma of_nat_diff_if: \<open>of_nat (m - n) = (if n\<le>m then of_nat m - of_nat n else 0)\<close>
+  by (simp add: not_le less_imp_le)
+
 end
 
 text \<open>Class for unital semirings with characteristic zero.