added lemmas
authornipkow
Mon Mar 26 19:13:45 2018 +0200 (13 months ago)
changeset 679494bb49ed64933
parent 67948 83902fff6243
child 67952 120c96286336
added lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sat Mar 24 22:45:06 2018 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Mar 26 19:13:45 2018 +0200
     1.3 @@ -3235,6 +3235,9 @@
     1.4    from this(2) Suc.hyps(1)[OF this(1)] Suc(2,3) upto_rec1 show ?case by simp
     1.5  qed
     1.6  
     1.7 +lemma length_upto[simp]: "length [i..j] = nat(j - i + 1)"
     1.8 +by(induction i j rule: upto.induct) (auto simp: upto.simps)
     1.9 +
    1.10  lemma set_upto[simp]: "set[i..j] = {i..j}"
    1.11  proof(induct i j rule:upto.induct)
    1.12    case (1 i j)
    1.13 @@ -3242,6 +3245,12 @@
    1.14      unfolding upto.simps[of i j] by auto
    1.15  qed
    1.16  
    1.17 +lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
    1.18 +apply(induction i j arbitrary: k rule: upto.induct)
    1.19 +apply(subst upto_rec1)
    1.20 +apply(auto simp add: nth_Cons')
    1.21 +done
    1.22 +
    1.23  lemma upto_split1: 
    1.24    "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j-1] @ [j..k]"
    1.25  proof (induction j rule: int_ge_induct)