# HG changeset patch
# User nipkow
# Date 1512415457 -3600
# Node ID 335ed2834ebcdc77266a218f5abf6cf0ee88cf29
# Parent  3fe40ff1b921be65de4993ba4362ff7153dcaecc
more lemmas

diff -r 3fe40ff1b921 -r 335ed2834ebc src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Dec 03 22:28:19 2017 +0100
+++ b/src/HOL/List.thy	Mon Dec 04 20:24:17 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