equal
deleted
inserted
replaced
3230 case (1 i j) |
3230 case (1 i j) |
3231 from this show ?case |
3231 from this show ?case |
3232 unfolding upto.simps[of i j] by auto |
3232 unfolding upto.simps[of i j] by auto |
3233 qed |
3233 qed |
3234 |
3234 |
3235 lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k" |
3235 lemma nth_upto[simp]: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k" |
3236 apply(induction i j arbitrary: k rule: upto.induct) |
3236 apply(induction i j arbitrary: k rule: upto.induct) |
3237 apply(subst upto_rec1) |
3237 apply(subst upto_rec1) |
3238 apply(auto simp add: nth_Cons') |
3238 apply(auto simp add: nth_Cons') |
3239 done |
3239 done |
3240 |
3240 |