equal
deleted
inserted
replaced
1 (* $Id$ *) |
|
2 |
1 |
3 header {* Slices of lists *} |
2 header {* Slices of lists *} |
4 |
3 |
5 theory Sublist |
4 theory Sublist |
6 imports Multiset |
5 imports Multiset |
7 begin |
6 begin |
8 |
|
9 |
7 |
10 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" |
8 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" |
11 apply (induct xs arbitrary: i j k) |
9 apply (induct xs arbitrary: i j k) |
12 apply simp |
10 apply simp |
13 apply (simp only: sublist_Cons) |
11 apply (simp only: sublist_Cons) |