--- a/src/HOL/List.thy Mon Dec 04 23:07:44 2017 +0100
+++ b/src/HOL/List.thy Mon Dec 04 23:10:52 2017 +0100
@@ -3226,6 +3226,9 @@
lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
by(simp add: upto.simps)
+lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i"
+by (simp add: upto.simps)
+
lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
by(simp add: upto.simps)
@@ -3257,6 +3260,9 @@
"i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j] @ [j+1..k]"
using upto_rec1 upto_rec2 upto_split1 by auto
+lemma upto_split3: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow> [i..k] = [i..j-1] @ j # [j+1..k]"
+using upto_rec1 upto_split1 by auto
+
text\<open>Tail recursive version for code generation:\<close>
definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where