equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Slices of lists\<close> |
5 section \<open>Slices of lists\<close> |
6 |
6 |
7 theory List_Sublist |
7 theory List_Sublist |
8 imports "~~/src/HOL/Library/Multiset" |
8 imports "HOL-Library.Multiset" |
9 begin |
9 begin |
10 |
10 |
11 lemma nths_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> nths xs {i..<j} @ nths xs {j..<k} = nths xs {i..<k}" |
11 lemma nths_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> nths xs {i..<j} @ nths xs {j..<k} = nths xs {i..<k}" |
12 apply (induct xs arbitrary: i j k) |
12 apply (induct xs arbitrary: i j k) |
13 apply simp |
13 apply simp |