# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1522101523 -7200
# Node ID 120c96286336dad9b0191f5cf462211a26381822
# Parent  4bb49ed64933bf87f6e2c571c60f5630db07629c# Parent  655aa11359dc49974c2337880c7f4c15117227e3
Merged

diff -r 655aa11359dc -r 120c96286336 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 26 16:14:16 2018 +0200
+++ b/src/HOL/List.thy	Mon Mar 26 23:58:43 2018 +0200
@@ -3235,6 +3235,9 @@
   from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) upto_rec1 show ?case by simp
 qed
 
+lemma length_upto[simp]: "length [i..j] = nat(j - i + 1)"
+by(induction i j rule: upto.induct) (auto simp: upto.simps)
+
 lemma set_upto[simp]: "set[i..j] = {i..j}"
 proof(induct i j rule:upto.induct)
   case (1 i j)
@@ -3242,6 +3245,12 @@
     unfolding upto.simps[of i j] by auto
 qed
 
+lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
+apply(induction i j arbitrary: k rule: upto.induct)
+apply(subst upto_rec1)
+apply(auto simp add: nth_Cons')
+done
+
 lemma upto_split1: 
   "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j-1] @ [j..k]"
 proof (induction j rule: int_ge_induct)