# Theory More_List

```(* Author: Simon Wimmer *)
theory More_List
imports
Main
Instantiate_Existentials
begin

section ‹First and Last Elements of Lists›

lemma (in -) hd_butlast_last_id:
"hd xs # tl (butlast xs) @ [last xs] = xs" if "length xs > 1"
using that by (cases xs) auto

section ‹@{term list_all}›

lemma (in -) list_all_map:
assumes inv: "⋀ x. P x ⟹ ∃ y. f y = x"
and all: "list_all P as"
shows "∃ as'. map f as' = as"
using all
apply (induction as)
apply (auto dest!: inv)
subgoal for as' a
by (inst_existentials "a # as'") simp
done

section ‹@{term list_all2}›

lemma list_all2_op_map_iff:
"list_all2 (λ a b. b = f a) xs ys ⟷ map f xs = ys"
unfolding list_all2_iff
proof (induction xs arbitrary: ys)
case Nil
then show ?case by auto
next
case (Cons a xs ys)
then show ?case by (cases ys) auto
qed

lemma list_all2_last:
"R (last xs) (last ys)" if "list_all2 R xs ys" "xs ≠ []"
using that
unfolding list_all2_iff
proof (induction xs arbitrary: ys)
case Nil
then show ?case by simp
next
case (Cons a xs ys)
then show ?case by (cases ys) auto
qed

lemma list_all2_set1:
"∀x∈set xs. ∃xa∈set as. P x xa" if "list_all2 P xs as"
using that
proof (induction xs arbitrary: as)
case Nil
then show ?case by auto
next
case (Cons a xs as)
then show ?case by (cases as) auto
qed

lemma list_all2_swap:
"list_all2 P xs ys ⟷ list_all2 (λ x y. P y x) ys xs"
unfolding list_all2_iff by (fastforce simp: in_set_zip)+

lemma list_all2_set2:
"∀x∈set as. ∃xa∈set xs. P xa x" if "list_all2 P xs as"
using that by - (rule list_all2_set1, subst (asm) list_all2_swap)

section ‹Distinct lists›

(* XXX Duplication with Floyd_Warshall.thy *)
lemma distinct_length_le:"finite s ⟹ set xs ⊆ s ⟹ distinct xs ⟹ length xs ≤ card s"
by (metis card_mono distinct_card)

section ‹@{term filter}›

lemma filter_eq_appendD:
"∃ xs' ys'. filter P xs' = xs ∧ filter P ys' = ys ∧ as = xs' @ ys'" if "filter P as = xs @ ys"
using that
proof (induction xs arbitrary: as)
case Nil
then show ?case
by (inst_existentials "[] :: 'a list" as) auto
next
case (Cons a xs)
from filter_eq_ConsD[OF Cons.prems[simplified]] obtain us vs where
"as = us @ a # vs" "∀u∈set us. ¬ P u" "P a" "filter P vs = xs @ ys"
by auto
moreover from Cons.IH[OF ‹_ = xs @ ys›] obtain xs' ys where
"filter P xs' = xs" "vs = xs' @ ys"
by auto
ultimately show ?case
by (inst_existentials "us @ [a] @ xs'" ys) auto
qed

lemma list_all2_elem_filter:
assumes "list_all2 P xs us" "x ∈ set xs"
shows "length (filter (P x) us) ≥ 1"
using assms by (induction xs arbitrary: us) (auto simp: list_all2_Cons1)

lemma list_all2_replicate_elem_filter:
assumes "list_all2 P (concat (replicate n xs)) ys" "x ∈ set xs"
shows "length (filter (P x) ys) ≥ n"
using assms
by (induction n arbitrary: ys; fastforce dest: list_all2_elem_filter simp: list_all2_append1)

section ‹Sublists›

lemma nths_split:
"nths xs (A ∪ B) = nths xs A @ nths xs B" if "∀ i ∈ A. ∀ j ∈ B. i < j"
using that
proof (induction xs arbitrary: A B)
case Nil
then show ?case by simp
next
case (Cons a xs)
let ?A = "{j. Suc j ∈ A}" and ?B = "{j. Suc j ∈ B}"
from Cons.prems have *: "∀i∈?A. ∀a∈?B. i < a"
by auto
have [simp]: "{j. Suc j ∈ A ∨ Suc j ∈ B} = ?A ∪ ?B"
by auto
show ?case
unfolding nths_Cons
proof (clarsimp, safe, goal_cases)
case 2
with Cons.prems have "A = {}"
by auto
with Cons.IH[OF *] show ?case by auto
qed (use Cons.prems Cons.IH[OF *] in auto)
qed

lemma nths_nth:
"nths xs {i} = [xs ! i]" if "i < length xs"
using that
proof (induction xs arbitrary: i)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case
by (cases i) (auto simp: nths_Cons)
qed

lemma nths_shift:
"nths (xs @ ys) S = nths ys {x - length xs | x. x ∈ S}" if
"∀ i ∈ S. length xs ≤ i"
using that
proof (induction xs arbitrary: S)
case Nil
then show ?case by auto
next
case (Cons a xs)
have [simp]: "{x - length xs |x. Suc x ∈ S} = {x - Suc (length xs) |x. x ∈ S}" if "0 ∉ S"
using that apply safe
apply force
subgoal for x x'
by (cases x') auto
done
from Cons.prems show ?case
by (simp, subst nths_Cons, subst Cons.IH; auto)
qed

lemma nths_eq_ConsD:
assumes "nths xs I = x # as"
shows
"∃ ys zs.
xs = ys @ x # zs ∧ length ys ∈ I ∧ (∀ i ∈ I. i ≥ length ys)
∧ nths zs ({i - length ys - 1 | i. i ∈ I ∧ i > length ys}) = as"
using assms
proof (induction xs arbitrary: I x as)
case Nil
then show ?case by simp
next
case (Cons a xs)
from Cons.prems show ?case
unfolding nths_Cons
apply (auto split: if_split_asm)
subgoal
by (inst_existentials "[] :: 'a list" xs; force intro: arg_cong2[of xs xs _ _ nths])
subgoal
apply (drule Cons.IH)
apply safe
subgoal for ys zs
apply (inst_existentials "a # ys" zs)
apply simp+
apply standard
subgoal for i
by (cases i; auto)
apply (rule arg_cong2[of zs zs _ _ nths])
apply simp
apply safe
subgoal for _ i
by (cases i; auto)
by force
done
done
qed

lemma nths_out_of_bounds:
"nths xs I = []" if "∀i ∈ I. i ≥ length xs"
(* Found by sledgehammer, then modified *)
proof -
have
"∀N as.
(∃n. n ∈ N ∧ ¬ length (as::'a list) ≤ n)
∨ (∀asa. nths (as @ asa) N = nths asa {n - length as |n. n ∈ N})"
using nths_shift by blast
then have
"⋀as. nths as {n - length xs |n. n ∈ I} = nths (xs @ as) I
∨ nths (xs @ []) I = []"
using that by fastforce
then have "nths (xs @ []) I = []"
by (metis (no_types) nths_nil)
then show ?thesis
by simp
qed

lemma nths_eq_appendD:
assumes "nths xs I = as @ bs"
shows
"∃ ys zs.
xs = ys @ zs ∧ nths ys I = as
∧ nths zs {i - length ys | i. i ∈ I ∧ i ≥ length ys} = bs"
using assms
proof (induction as arbitrary: xs I)
case Nil
then show ?case
by (inst_existentials "[] :: 'a list" "nths bs") auto
next
case (Cons a ys xs)
from nths_eq_ConsD[of xs I a "ys @ bs"] Cons.prems
obtain ys' zs' where
"xs = ys' @ a # zs'"
"length ys' ∈ I"
"∀i ∈ I. i ≥ length ys'"
"nths zs' {i - length ys' - 1 |i. i ∈ I ∧ i > length ys'} = ys @ bs"
by auto
moreover from Cons.IH[OF ‹nths zs' _ = _›] obtain ys'' zs'' where
"zs' = ys'' @ zs''"
"ys = nths ys'' {i - length ys' - 1 |i. i ∈ I ∧ length ys' < i}"
"bs = nths zs'' {i - length ys'' |i. i ∈ {i - length ys' - 1 |i. i ∈ I ∧ length ys' < i} ∧ length ys'' ≤ i}"
by auto
ultimately show ?case
apply (inst_existentials "ys' @ a # ys''" zs'')
apply (simp; fail)
subgoal
by (simp add: nths_out_of_bounds nths_append nths_Cons)
(rule arg_cong2[of ys'' ys'' _ _ nths]; force)
subgoal
by safe (rule arg_cong2[of zs'' zs'' _ _ nths]; force) (* Slow *)
done
qed

lemma filter_nths_length:
"length (filter P (nths xs I)) ≤ length (filter P xs)"
proof (induction xs arbitrary: I)
case Nil
then show ?case
by simp
next
case Cons
then show ?case
(* Found by sledgehammer *)
proof -
fix a :: 'a and xsa :: "'a list" and Ia :: "nat set"
assume a1: "⋀I. length (filter P (nths xsa I)) ≤ length (filter P xsa)"
have f2:
"∀b bs N. if 0 ∈ N then nths ((b::'a) # bs) N =
[b] @ nths bs {n. Suc n ∈ N} else nths (b # bs) N = [] @ nths bs {n. Suc n ∈ N}"
have f3:
"nths (a # xsa) Ia = [] @ nths xsa {n. Suc n ∈ Ia}
⟶ length (filter P (nths (a # xsa) Ia)) ≤ length (filter P xsa)"
using a1 by (metis append_Nil)
have f4: "length (filter P (nths xsa {n. Suc n ∈ Ia})) + 0 ≤ length (filter P xsa) + 0"
using a1 by simp
have f5:
"Suc (length (filter P (nths xsa {n. Suc n ∈ Ia})) + 0)
= length (a # filter P (nths xsa {n. Suc n ∈ Ia}))"
by force
have f6: "Suc (length (filter P xsa) + 0) = length (a # filter P xsa)"
by simp
{ assume "¬ length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
{ assume "nths (a # xsa) Ia ≠ [a] @ nths xsa {n. Suc n ∈ Ia}"
moreover
{ assume
"nths (a # xsa) Ia = [] @ nths xsa {n. Suc n ∈ Ia}
∧ length (filter P (a # xsa)) ≤ length (filter P xsa)"
then have "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
using a1 by (metis (no_types) append_Nil filter.simps(2) impossible_Cons) }
ultimately have "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
using f3 f2 by (meson dual_order.trans le_cases) }
then have "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
using f6 f5 f4 a1 by (metis Suc_le_mono append_Cons append_Nil filter.simps(2)) }
then show "length (filter P (nths (a # xsa) Ia)) ≤ length (filter P (a # xsa))"
by meson
qed
qed

end (* Theory *)
```