# HG changeset patch
# User haftmann
# Date 1540460882 0
# Node ID 2424301cc73dc5cace55336b86f3a16f722c5b42
# Parent  effe7f8b2b1bc31e7dfdca8dede8343be8c1839c
more and generalized lemmas

diff -r effe7f8b2b1b -r 2424301cc73d src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Tue Oct 23 10:50:48 2018 +0200
+++ b/src/HOL/Factorial.thy	Thu Oct 25 09:48:02 2018 +0000
@@ -242,11 +242,21 @@
   shows "x > 0 \<Longrightarrow> pochhammer x n > 0"
   by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)
 
+context comm_semiring_1
+begin
+
 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
-  by (simp add: pochhammer_prod)
+  by (simp add: pochhammer_prod Factorial.pochhammer_prod)
+
+end
+
+context comm_ring_1
+begin
 
 lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
-  by (simp add: pochhammer_prod)
+  by (simp add: pochhammer_prod Factorial.pochhammer_prod)
+
+end
 
 lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
   by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps)
diff -r effe7f8b2b1b -r 2424301cc73d src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Oct 23 10:50:48 2018 +0200
+++ b/src/HOL/Int.thy	Thu Oct 25 09:48:02 2018 +0000
@@ -1039,17 +1039,41 @@
 
 subsection \<open>@{term sum} and @{term prod}\<close>
 
-lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))"
-  by (induct A rule: infinite_finite_induct) auto
+context semiring_1
+begin
+
+lemma of_nat_sum [simp]:
+  "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat (f x))"
+  by (induction A rule: infinite_finite_induct) auto
+
+end
 
-lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))"
-  by (induct A rule: infinite_finite_induct) auto
+context ring_1
+begin
+
+lemma of_int_sum [simp]:
+  "of_int (sum f A) = (\<Sum>x\<in>A. of_int (f x))"
+  by (induction A rule: infinite_finite_induct) auto
+
+end
 
-lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))"
-  by (induct A rule: infinite_finite_induct) auto
+context comm_semiring_1
+begin
+
+lemma of_nat_prod [simp]:
+  "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat (f x))"
+  by (induction A rule: infinite_finite_induct) auto
+
+end
 
-lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))"
-  by (induct A rule: infinite_finite_induct) auto
+context comm_ring_1
+begin
+
+lemma of_int_prod [simp]:
+  "of_int (prod f A) = (\<Prod>x\<in>A. of_int (f x))"
+  by (induction A rule: infinite_finite_induct) auto
+
+end
 
 
 subsection \<open>Setting up simplification procedures\<close>
diff -r effe7f8b2b1b -r 2424301cc73d src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Oct 23 10:50:48 2018 +0200
+++ b/src/HOL/Set_Interval.thy	Thu Oct 25 09:48:02 2018 +0000
@@ -2271,42 +2271,28 @@
 qed
 
 lemma Sum_Icc_nat:
-  "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2"
-  if "m \<le> n" for m n :: nat
-proof -
-  have *: "m * (m - 1) \<le> n * (n + 1)"
-    using that by (meson diff_le_self order_trans le_add1 mult_le_mono)
+  "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2" for m n :: nat
+proof (cases "m \<le> n")
+  case True
+  then have *: "m * (m - 1) \<le> n * (n + 1)"
+    by (meson diff_le_self order_trans le_add1 mult_le_mono)
   have "int (\<Sum>{m..n}) = (\<Sum>{int m..int n})"
     by (simp add: sum.atLeast_int_atMost_int_shift)
   also have "\<dots> = (int n * (int n + 1) - int m * (int m - 1)) div 2"
-    using that by (simp add: Sum_Icc_int)
+    using \<open>m \<le> n\<close> by (simp add: Sum_Icc_int)
   also have "\<dots> = int ((n * (n + 1) - m * (m - 1)) div 2)"
     using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff)
   finally show ?thesis
     by (simp only: of_nat_eq_iff)
+next
+  case False
+  then show ?thesis
+    by (auto dest: less_imp_Suc_add simp add: not_le algebra_simps)
 qed
 
 lemma Sum_Ico_nat: 
-  "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2"
-  if "m \<le> n" for m n :: nat
-proof -
-  from that consider "m < n" | "m = n"
-    by (auto simp add: less_le)
-  then show ?thesis proof cases
-    case 1
-    then have "{m..<n} = {m..n - 1}"
-      by auto
-    then have "\<Sum>{m..<n} = \<Sum>{m..n - 1}"
-      by simp
-    also have "\<dots> = (n * (n - 1) - m * (m - 1)) div 2"
-      using \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute)
-    finally show ?thesis .
-  next
-    case 2
-    then show ?thesis
-      by simp
-  qed
-qed
+  "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2" for m n :: nat
+  by (cases n) (simp_all add: atLeastLessThanSuc_atLeastAtMost Sum_Icc_nat)
 
 
 subsubsection \<open>Division remainder\<close>