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"
by(auto simp add:hidden_def nth_append)


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
    then show ?thesis by(simp add:Let_def)
  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)"
by(simp add:fun_upds_apply Let_def)


lemma map_upds_upd_conv_last_index:
  "x  set xs; size xs  size ys 
   m(xs[↦]ys, xy) = m(xs[↦]ys[last_index xs x := y])"
by(rule ext) (simp add:fun_upds_apply eq_sym_conv Let_def)

end