# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1738773296 0
# Node ID 0aa2d1c132b2291a7a6d7a32036c07cd8737961d
# Parent  2028082805f00f094779e359be48d5427a5dc54a
A couple of theorems proved by Manuel Eberl from his AFP entry Sum_Of_Squares_Count

diff -r 2028082805f0 -r 0aa2d1c132b2 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Tue Feb 04 22:21:36 2025 +0100
+++ b/src/HOL/Groups_List.thy	Wed Feb 05 16:34:56 2025 +0000
@@ -141,6 +141,12 @@
     .
 qed
 
+lemma sum_list_of_nat: "sum_list (map of_nat xs) = of_nat (sum_list xs)"
+  by (induction xs) auto
+
+lemma sum_list_of_int: "sum_list (map of_int xs) = of_int (sum_list xs)"
+  by (induction xs) auto
+
 lemma (in comm_monoid_add) sum_list_map_remove1:
   "x \<in> set xs \<Longrightarrow> sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
   by (induct xs) (auto simp add: ac_simps)
@@ -171,7 +177,7 @@
 
 lemma (in comm_monoid_add) distinct_sum_list_conv_Sum:
   "distinct xs \<Longrightarrow> sum_list xs = Sum (set xs)"
-  by (induct xs) simp_all
+  by (metis local.sum.set_conv_list local.sum_list_def map_ident remdups_id_iff_distinct)
 
 lemma sum_list_upt[simp]:
   "m \<le> n \<Longrightarrow> sum_list [m..<n] = \<Sum> {m..<n}"
@@ -181,14 +187,14 @@
 begin
 
 lemma sum_list_nonneg: "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> 0 \<le> sum_list xs"
-by (induction xs) auto
+  by (induction xs) auto
 
 lemma sum_list_nonpos: "(\<And>x. x \<in> set xs \<Longrightarrow> x \<le> 0) \<Longrightarrow> sum_list xs \<le> 0"
-by (induction xs) (auto simp: add_nonpos_nonpos)
+  by (induction xs) (auto simp: add_nonpos_nonpos)
 
 lemma sum_list_nonneg_eq_0_iff:
   "(\<And>x. x \<in> set xs \<Longrightarrow> 0 \<le> x) \<Longrightarrow> sum_list xs = 0 \<longleftrightarrow> (\<forall>x\<in> set xs. x = 0)"
-by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg)
+  by (induction xs) (simp_all add: add_nonneg_eq_0_iff sum_list_nonneg)
 
 end
 
@@ -211,10 +217,15 @@
 
 lemma (in ordered_cancel_comm_monoid_diff) sum_list_update:
   "k < size xs \<Longrightarrow> sum_list (xs[k := x]) = sum_list xs + x - xs ! k"
-apply(induction xs arbitrary:k)
- apply (auto simp: add_ac split: nat.split)
-apply(drule elem_le_sum_list)
-by (simp add: local.add_diff_assoc local.add_increasing)
+proof (induction xs arbitrary:k)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs)
+  then show ?case
+    apply (simp add: add_ac split: nat.split)
+    using add_increasing diff_add_assoc elem_le_sum_list zero_le by force
+qed
 
 lemma (in monoid_add) sum_list_triv:
   "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
@@ -276,8 +287,7 @@
 lemma sum_list_mono2: fixes xs :: "'a ::ordered_comm_monoid_add list"
 shows "\<lbrakk> length xs = length ys; \<And>i. i < length xs \<longrightarrow> xs!i \<le> ys!i \<rbrakk>
   \<Longrightarrow> sum_list xs \<le> sum_list ys"
-apply(induction xs ys rule: list_induct2)
-by(auto simp: nth_Cons' less_Suc_eq_0_disj imp_ex add_mono)
+  by (induction xs ys rule: list_induct2) (auto simp: nth_Cons' less_Suc_eq_0_disj imp_ex add_mono)
 
 lemma (in monoid_add) sum_list_distinct_conv_sum_set:
   "distinct xs \<Longrightarrow> sum_list (map f xs) = sum f (set xs)"
@@ -369,6 +379,28 @@
   thus ?case by simp
 qed
 
+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"
+  shows   "x \<le> sum_list xs"
+  using assms
+proof (induction xs)
+  case (Cons y xs)
+  show ?case
+  proof (cases "y = x")
+    case True
+    have "x + 0 \<le> x + sum_list xs"
+      by (intro add_mono order.refl sum_list_nonneg) (use Cons in auto)
+    thus ?thesis
+      using True by auto
+  next
+    case False
+    have "0 + x \<le> y + sum_list xs"
+      by (intro add_mono Cons.IH Cons.prems) (use Cons.prems False in auto)
+    thus ?thesis
+      by auto
+  qed
+qed auto
 
 subsection \<open>Horner sums\<close>
 
diff -r 2028082805f0 -r 0aa2d1c132b2 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Tue Feb 04 22:21:36 2025 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 05 16:34:56 2025 +0000
@@ -774,4 +774,35 @@
   finally show ?thesis .
 qed
 
+text \<open>Thanks to Manuel Eberl\<close>
+lemma prime_cong_4_nat_cases [consumes 1, case_names 2 cong_1 cong_3]:
+  assumes "prime (p :: nat)"
+  obtains "p = 2" | "[p = 1] (mod 4)" | "[p = 3] (mod 4)"
+proof -
+  have "[p = 2] (mod 4) \<longleftrightarrow> p = 2"
+  proof
+    assume "[p = 2] (mod 4)"
+    hence "p mod 4 = 2"
+      by (auto simp: cong_def)
+    hence "even p"
+      by (simp add: even_even_mod_4_iff)
+    with assms show "p = 2"
+      unfolding prime_nat_iff by force
+  qed auto
+  moreover have "[p \<noteq> 0] (mod 4)"
+  proof
+    assume "[p = 0] (mod 4)"
+    hence "4 dvd p"
+      by (auto simp: cong_0_iff)
+    with assms have "p = 4"
+      by (subst (asm) prime_nat_iff) auto
+    thus False
+      using assms by simp
+  qed
+  ultimately consider "[p = 3] (mod 4)" | "[p = 1] (mod 4)" | "p = 2"
+    by (fastforce simp: cong_def)
+  thus ?thesis
+    using that by metis
+qed
+
 end
diff -r 2028082805f0 -r 0aa2d1c132b2 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Feb 04 22:21:36 2025 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Feb 05 16:34:56 2025 +0000
@@ -287,6 +287,9 @@
 lemma of_real_prod[simp]: "of_real (prod f s) = (\<Prod>x\<in>s. of_real (f x))"
   by (induct s rule: infinite_finite_induct) auto
 
+lemma sum_list_of_real: "sum_list (map of_real xs) = of_real (sum_list xs)"
+  by (induction xs) auto
+
 lemma nonzero_of_real_inverse:
   "x \<noteq> 0 \<Longrightarrow> of_real (inverse x) = inverse (of_real x :: 'a::real_div_algebra)"
   by (simp add: of_real_def nonzero_inverse_scaleR_distrib)