more lemmas
authornipkow
Tue Nov 21 14:11:31 2017 +0100 (9 months ago)
changeset 670816a8c148db36f
parent 67080 2c0f24e927dd
child 67082 4e4bea76e559
more lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sun Nov 19 15:27:01 2017 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Nov 21 14:11:31 2017 +0100
     1.3 @@ -3245,6 +3245,18 @@
     1.4      unfolding upto.simps[of i j] by auto
     1.5  qed
     1.6  
     1.7 +lemma upto_split1: 
     1.8 +  "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j-1] @ [j..k]"
     1.9 +proof (induction j rule: int_ge_induct)
    1.10 +  case base thus ?case by (simp add: upto_rec1)
    1.11 +next
    1.12 +  case step thus ?case using upto_rec1 upto_rec2 by simp
    1.13 +qed
    1.14 +
    1.15 +lemma upto_split2: 
    1.16 +  "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j] @ [j+1..k]"
    1.17 +using upto_rec1 upto_rec2 upto_split1 by auto
    1.18 +
    1.19  text\<open>Tail recursive version for code generation:\<close>
    1.20  
    1.21  definition upto_aux :: "int \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where