section {* Slices of lists *}
theory List_Sublist
imports "~~/src/HOL/Library/Multiset"
begin
lemma sublist_split: "i ≤ j ∧ j ≤ k ⟹ sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}"
apply (induct xs arbitrary: i j k)
apply simp
apply (simp only: sublist_Cons)
apply simp
apply safe
apply simp
apply (erule_tac x="0" in meta_allE)
apply (erule_tac x="j - 1" in meta_allE)
apply (erule_tac x="k - 1" in meta_allE)
apply (subgoal_tac "0 ≤ j - 1 ∧ j - 1 ≤ k - 1")
apply simp
apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
apply (subgoal_tac "{ja. j ≤ Suc ja ∧ Suc ja < k} = {j - Suc 0..<k - Suc 0}")
apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
apply simp
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply (erule_tac x="i - 1" in meta_allE)
apply (erule_tac x="j - 1" in meta_allE)
apply (erule_tac x="k - 1" in meta_allE)
apply (subgoal_tac " {ja. i ≤ Suc ja ∧ Suc ja < j} = {i - 1 ..<j - 1}")
apply (subgoal_tac " {ja. j ≤ Suc ja ∧ Suc ja < k} = {j - 1..<k - 1}")
apply (subgoal_tac "{j. i ≤ Suc j ∧ Suc j < k} = {i - 1..<k - 1}")
apply (subgoal_tac " 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..<m} = take m xs"
apply (induct xs arbitrary: m)
apply simp
apply (case_tac m)
apply simp
apply (simp add: sublist_Cons sublist_take)
done
lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
apply (induct xs)
apply simp
apply (simp add: sublist_Cons)
done
lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
apply (induct xs)
apply simp
apply (simp add: sublist_Cons)
done
lemma sublist_single: "a < length xs ⟹ 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..<m}"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac n, case_tac m)
apply simp
apply simp
apply (simp add: sublist_take')
apply (case_tac m)
apply simp
apply (simp add: sublist_Cons sublist'_sublist)
done
subsection {* Showing equivalence to use of drop and take for definition *}
lemma "sublist' n m xs = take (m - n) (drop n xs)"
apply (induct xs arbitrary: n m)
apply simp
apply (case_tac m)
apply simp
apply (case_tac n)
apply simp
apply simp
done
subsection {* General lemma about sublist *}
lemma sublist'_Nil[simp]: "sublist' i j [] = []"
by simp
lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 ⇒ (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
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