(* Title: HOL/Imperative_HOL/ex/Sublist.thy Author: Lukas Bulwahn, TU Muenchen *) section {* Slices of lists *} theory Sublist imports "~~/src/HOL/Library/Multiset" begin lemma sublist_split: "i \ j \ j \ k \ sublist xs {i.. j - 1 \ j - 1 \ k - 1") apply simp apply (subgoal_tac "{ja. Suc ja < j} = {0.. Suc ja \ Suc ja < k} = {j - Suc 0.. Suc ja \ Suc ja < j} = {i - 1 .. Suc ja \ Suc ja < k} = {j - 1.. Suc j \ Suc j < k} = {i - 1.. j - 1 \ j - 1 \ k - 1") apply simp apply fastforce apply fastforce apply fastforce apply fastforce done lemma sublist_update1: "i \ inds \ sublist (xs[i := v]) inds = sublist xs inds" apply (induct xs arbitrary: i inds) apply simp apply (case_tac i) apply (simp add: sublist_Cons) apply (simp add: sublist_Cons) done lemma sublist_update2: "i \ inds \ sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \ inds. k < i}):= v]" proof (induct xs arbitrary: i inds) case Nil thus ?case by simp next case (Cons x xs) thus ?case proof (cases i) case 0 with Cons show ?thesis by (simp add: sublist_Cons) next case (Suc i') with Cons show ?thesis apply simp apply (simp add: sublist_Cons) apply auto apply (auto simp add: nat.split) apply (simp add: card_less_Suc[symmetric]) apply (simp add: card_less_Suc2) done qed qed lemma sublist_update: "sublist (xs[i := v]) inds = (if i \ inds then (sublist xs inds)[(card {k \ inds. k < i}) := v] else sublist xs inds)" by (simp add: sublist_update1 sublist_update2) lemma sublist_take: "sublist xs {j. j < m} = take m xs" apply (induct xs arbitrary: m) apply simp apply (case_tac m) apply simp apply (simp add: sublist_Cons) done lemma sublist_take': "sublist xs {0.. sublist xs {a} = [xs ! a]" apply (induct xs arbitrary: a) apply simp apply(case_tac aa) apply simp apply (simp add: sublist_Cons) apply simp apply (simp add: sublist_Cons) done lemma sublist_is_Nil: "\i \ inds. i \ length xs \ sublist xs inds = []" apply (induct xs arbitrary: inds) apply simp apply (simp add: sublist_Cons) apply auto apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) apply auto done lemma sublist_Nil': "sublist xs inds = [] \ \i \ inds. i \ length xs" apply (induct xs arbitrary: inds) apply simp apply (simp add: sublist_Cons) apply (auto split: if_splits) apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) apply (case_tac x, auto) done lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\i \ inds. i \ length xs)" apply (induct xs arbitrary: inds) apply simp apply (simp add: sublist_Cons) apply auto apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) apply (case_tac x, auto) done lemma sublist_eq_subseteq: " \ inds' \ inds; sublist xs inds = sublist ys inds \ \ sublist xs inds' = sublist ys inds'" apply (induct xs arbitrary: ys inds inds') apply simp apply (drule sym, rule sym) apply (simp add: sublist_Nil, fastforce) apply (case_tac ys) apply (simp add: sublist_Nil, fastforce) apply (auto simp add: sublist_Cons) apply (erule_tac x="list" in meta_allE) apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) apply fastforce apply (erule_tac x="list" in meta_allE) apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) apply (erule_tac x="{j. Suc j \ inds'}" in meta_allE) apply fastforce done lemma sublist_eq: "\ \i \ inds. ((i < length xs) \ (i < length ys)) \ ((i \ length xs ) \ (i \ length ys)); \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" apply (induct xs arbitrary: ys inds) apply simp apply (rule sym, simp add: sublist_Nil) apply (case_tac ys) apply (simp add: sublist_Nil) apply (auto simp add: sublist_Cons) apply (erule_tac x="list" in meta_allE) apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) apply fastforce apply (erule_tac x="list" in meta_allE) apply (erule_tac x="{j. Suc j \ inds}" in meta_allE) apply fastforce done lemma sublist_eq_samelength: "\ length xs = length ys; \i \ inds. xs ! i = ys ! i \ \ sublist xs inds = sublist ys inds" by (rule sublist_eq, auto) lemma sublist_eq_samelength_iff: "length xs = length ys \ (sublist xs inds = sublist ys inds) = (\i \ inds. xs ! i = ys ! i)" apply (induct xs arbitrary: ys inds) apply simp apply (rule sym, simp add: sublist_Nil) apply (case_tac ys) apply (simp add: sublist_Nil) apply (auto simp add: sublist_Cons) apply (case_tac i) apply auto apply (case_tac i) apply auto done section {* Another sublist function *} function sublist' :: "nat \ nat \ 'a list \ 'a list" where "sublist' n m [] = []" | "sublist' n 0 xs = []" | "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)" | "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs" by pat_completeness auto termination by lexicographic_order subsection {* Proving equivalence to the other sublist command *} lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \ j \ j < m}" apply (induct xs arbitrary: n m) apply simp apply (case_tac n) apply (case_tac m) apply simp apply (simp add: sublist_Cons) apply (case_tac m) apply simp apply (simp add: sublist_Cons) done lemma "sublist' n m xs = sublist xs {n.. (x # sublist' 0 j xs) | Suc i' \ sublist' i' j xs)" by (cases i) auto lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))" apply (cases j) apply auto apply (cases i) apply auto done lemma sublist_n_0: "sublist' n 0 xs = []" by (induct xs, auto) lemma sublist'_Nil': "n \ m \ sublist' n m xs = []" apply (induct xs arbitrary: n m) apply simp apply (case_tac m) apply simp apply (case_tac n) apply simp apply simp done lemma sublist'_Nil2: "n \ length xs \ sublist' n m xs = []" apply (induct xs arbitrary: n m) apply simp apply (case_tac m) apply simp apply (case_tac n) apply simp apply simp done lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \ m) \ (n \ length xs))" apply (induct xs arbitrary: n m) apply simp apply (case_tac m) apply simp apply (case_tac n) apply simp apply simp done lemma sublist'_notNil: "\ n < length xs; n < m \ \ sublist' n m xs \ []" apply (induct xs arbitrary: n m) apply simp apply (case_tac m) apply simp apply (case_tac n) apply simp apply simp done lemma sublist'_single: "n < length xs \ sublist' n (Suc n) xs = [xs ! n]" apply (induct xs arbitrary: n) apply simp apply simp apply (case_tac n) apply (simp add: sublist_n_0) apply simp done lemma sublist'_update1: "i \ m \ sublist' n m (xs[i:=v]) = sublist' n m xs" apply (induct xs arbitrary: n m i) apply simp apply simp apply (case_tac i) apply simp apply simp done lemma sublist'_update2: "i < n \ sublist' n m (xs[i:=v]) = sublist' n m xs" apply (induct xs arbitrary: n m i) apply simp apply simp apply (case_tac i) apply simp apply simp done lemma sublist'_update3: "\n \ i; i < m\ \ sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]" proof (induct xs arbitrary: n m i) case Nil thus ?case by auto next case (Cons x xs) thus ?case apply - apply auto apply (cases i) apply auto apply (cases i) apply auto done qed lemma "\ sublist' i j xs = sublist' i j ys; n \ i; m \ j \ \ sublist' n m xs = sublist' n m ys" proof (induct xs arbitrary: i j ys n m) case Nil thus ?case apply - apply (rule sym, drule sym) apply (simp add: sublist'_Nil) apply (simp add: sublist'_Nil3) apply arith done next case (Cons x xs i j ys n m) note c = this thus ?case proof (cases m) case 0 thus ?thesis by (simp add: sublist_n_0) next case (Suc m') note a = this thus ?thesis proof (cases n) case 0 note b = this show ?thesis proof (cases ys) case Nil with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3) next case (Cons y ys) show ?thesis proof (cases j) case 0 with a b Cons.prems show ?thesis by simp next case (Suc j') with a b Cons.prems Cons show ?thesis apply - apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto) done qed qed next case (Suc n') show ?thesis proof (cases ys) case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3) next case (Cons y ys) with Suc a Cons.prems show ?thesis apply - apply simp apply (cases j) apply simp apply (cases i) apply simp apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"]) apply simp apply simp apply simp apply simp apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"]) apply simp apply simp apply simp done qed qed qed qed lemma length_sublist': "j \ length xs \ length (sublist' i j xs) = j - i" by (induct xs arbitrary: i j, auto) lemma sublist'_front: "\ i < j; i < length xs \ \ sublist' i j xs = xs ! i # sublist' (Suc i) j xs" apply (induct xs arbitrary: i j) apply simp apply (case_tac j) apply simp apply (case_tac i) apply simp apply simp done lemma sublist'_back: "\ i < j; j \ length xs \ \ sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]" apply (induct xs arbitrary: i j) apply simp apply simp done (* suffices that j \ length xs and length ys *) lemma sublist'_eq_samelength_iff: "length xs = length ys \ (sublist' i j xs = sublist' i j ys) = (\i'. i \ i' \ i' < j \ xs ! i' = ys ! i')" proof (induct xs arbitrary: ys i j) case Nil thus ?case by simp next case (Cons x xs) thus ?case apply - apply (cases ys) apply simp apply simp apply auto apply (case_tac i', auto) apply (erule_tac x="Suc i'" in allE, auto) apply (erule_tac x="i' - 1" in allE, auto) apply (erule_tac x="Suc i'" in allE, auto) done qed lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs" by (induct xs, auto) lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" by (induct xs arbitrary: i j n m) (auto simp add: min_diff) lemma sublist'_append: "\ i \ j; j \ k \ \(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs" by (induct xs arbitrary: i j k) auto lemma nth_sublist': "\ k < j - i; j \ length xs \ \ (sublist' i j xs) ! k = xs ! (i + k)" apply (induct xs arbitrary: i j k) apply simp apply (case_tac k) apply auto done lemma set_sublist': "set (sublist' i j xs) = {x. \k. i \ k \ k < j \ k < List.length xs \ x = xs ! k}" apply (simp add: sublist'_sublist) apply (simp add: set_sublist) apply auto done lemma all_in_set_sublist'_conv: "(\j. j \ set (sublist' l r xs) \ P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" unfolding set_sublist' by blast lemma ball_in_set_sublist'_conv: "(\j \ set (sublist' l r xs). P j) = (\k. l \ k \ k < r \ k < List.length xs \ P (xs ! k))" unfolding set_sublist' by blast lemma mset_sublist: assumes l_r: "l \ r \ r \ List.length xs" assumes left: "\ i. i < l \ (xs::'a list) ! i = ys ! i" assumes right: "\ i. i \ r \ (xs::'a list) ! i = ys ! i" assumes multiset: "mset xs = mset ys" shows "mset (sublist' l r xs) = mset (sublist' l r ys)" proof - from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") by (simp add: sublist'_append) from multiset have length_eq: "List.length xs = List.length ys" by (rule mset_eq_length) with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") by (simp add: sublist'_append) from xs_def ys_def multiset have "mset ?xs_long = mset ?ys_long" by simp moreover from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys" by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) moreover from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys" by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) ultimately show ?thesis by (simp add: mset_append) qed end