more lemmas
authornipkow
Mon Dec 04 20:24:17 2017 +0100 (7 weeks ago)
changeset 67124335ed2834ebc
parent 67123 3fe40ff1b921
child 67134 66ce07e8dbf2
more lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sun Dec 03 22:28:19 2017 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Dec 04 20:24:17 2017 +0100
     1.3 @@ -3226,6 +3226,9 @@
     1.4  lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
     1.5  by(simp add: upto.simps)
     1.6  
     1.7 +lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i"
     1.8 +by (simp add: upto.simps)
     1.9 +
    1.10  lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]"
    1.11  by(simp add: upto.simps)
    1.12  
    1.13 @@ -3257,6 +3260,9 @@
    1.14    "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j] @ [j+1..k]"
    1.15  using upto_rec1 upto_rec2 upto_split1 by auto
    1.16  
    1.17 +lemma upto_split3: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow> [i..k] = [i..j-1] @ j # [j+1..k]"
    1.18 +using upto_rec1 upto_split1 by auto
    1.19 +
    1.20  text\<open>Tail recursive version for code generation:\<close>
    1.21  
    1.22  definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where