diff -r 6d96ee03b62e -r 4df0628e8545 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Set_Interval.thy	Wed Jul 17 14:02:42 2019 +0100
@@ -1995,6 +1995,20 @@
   finally show ?thesis .
 qed
 
+lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}"
+proof (induction n)
+  case 0
+  show ?case
+    by (cases "m=0") auto
+next
+  case (Suc n)
+  then show ?case
+    by (auto simp: assoc split: if_split_asm)
+qed
+
+lemma in_pairs_0: "F g {..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}"
+  using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost)
+
 end
 
 lemma sum_natinterval_diff: