# Theory Hidden

```theory Hidden
imports "List-Index.List_Index"
begin

definition hidden :: "'a list ⇒ nat ⇒ bool" where
"hidden xs i  ≡  i < size xs ∧ xs!i ∈ set(drop (i+1) xs)"

lemma hidden_last_index: "x ∈ set xs ⟹ hidden (xs @ [x]) (last_index xs x)"
by(auto simp add: hidden_def nth_append rev_nth[symmetric]
dest: last_index_less[OF _ le_refl])

lemma hidden_inacc: "hidden xs i ⟹ last_index xs x ≠ i"
by(auto simp add: hidden_def last_index_drop last_index_less_size_conv)

lemma [simp]: "hidden xs i ⟹ hidden (xs@[x]) i"

lemma fun_upds_apply:
"(m(xs[↦]ys)) x =
(let xs' = take (size ys) xs
in if x ∈ set xs' then Some(ys ! last_index xs' x) else m x)"
proof(induct xs arbitrary: m ys)
case Nil then show ?case by(simp add: Let_def)
next
case Cons show ?case
proof(cases ys)
case Nil
next
case Cons': Cons
then show ?thesis using Cons by(simp add: Let_def last_index_Cons)
qed
qed

lemma map_upds_apply_eq_Some:
"((m(xs[↦]ys)) x = Some y) =
(let xs' = take (size ys) xs
in if x ∈ set xs' then ys ! last_index xs' x = y else m x = Some y)"