# Theory ListIndex

(*  Title:      JinjaThreads/Compiler/ListIndex.thy
Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Indexing variables in variable lists›

theory ListIndex imports Main begin

text‹In order to support local variables and arbitrarily nested
blocks, the local variables are arranged as an indexed list. The
outermost local variable (this'') is the first element in the list,
the most recently created local variable the last element. When
descending into a block structure, a corresponding list @{term Vs} of
variable names is maintained. To find the index of some variable
@{term V}, we have to find the index of the \emph{last} occurrence of
@{term V} in @{term Vs}. This is what @{term index} does:›

primrec index :: "'a list ⇒ 'a ⇒ nat"
where
"index [] y = 0"
| "index (x#xs) y =
(if x=y then if x ∈ set xs then index xs y + 1 else 0 else index xs y + 1)"

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

subsection ‹@{term index}›

lemma [simp]: "index (xs @ [x]) x = size xs"
(*<*)by(induct xs) simp_all(*>*)

lemma [simp]: "(index (xs @ [x]) y = size xs) = (x = y)"
(*<*)by(induct xs) auto(*>*)

lemma [simp]: "x ∈ set xs ⟹ xs ! index xs x = x"
(*<*)by(induct xs) auto(*>*)

lemma [simp]: "x ∉ set xs ⟹ index xs x = size xs"
(*<*)by(induct xs) auto(*>*)

lemma index_size_conv[simp]: "(index xs x = size xs) = (x ∉ set xs)"
(*<*)by(induct xs) auto(*>*)

lemma size_index_conv[simp]: "(size xs = index xs x) = (x ∉ set xs)"
(*<*)by(induct xs) auto(*>*)

lemma "(index xs x < size xs) = (x ∈ set xs)"
(*<*)by(induct xs) auto(*>*)

lemma [simp]: "⟦ y ∈ set xs; x ≠ y ⟧ ⟹ index (xs @ [x]) y = index xs y"
(*<*)by(induct xs) auto(*>*)

lemma index_less_size[simp]: "x ∈ set xs ⟹ index xs x < size xs"
(*<*)
apply(induct xs)
apply simp
apply(fastforce)
done
(*>*)

lemma index_less_aux: "⟦x ∈ set xs; size xs ≤ n⟧ ⟹ index xs x < n"
(*<*)
apply(subgoal_tac "index xs x < size xs")
apply(simp (no_asm_simp))
apply simp
done
(*>*)

lemma [simp]: "x ∈ set xs ∨ y ∈ set xs ⟹ (index xs x = index xs y) = (x = y)"
(*<*)by (induct xs) auto(*>*)

lemma inj_on_index: "inj_on (index xs) (set xs)"

lemma index_drop: "⋀x i. ⟦ x ∈ set xs; index xs x < i ⟧ ⟹ x ∉ set(drop i xs)"
(*<*)
apply(induct xs)
apply (auto simp:drop_Cons split:if_split_asm nat.splits dest:in_set_dropD)
done
(*>*)

subsection ‹@{term hidden}›

lemma hidden_index: "x ∈ set xs ⟹ hidden (xs @ [x]) (index xs x)"
(*<*)
apply(drule index_less_size)
apply(simp del:index_less_size)
done
(*>*)

lemma hidden_inacc: "hidden xs i ⟹ index xs x ≠ i"
(*<*)
apply(case_tac "x ∈ set xs")
apply(auto simp add:hidden_def index_less_aux nth_append index_drop)
done
(*>*)

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

lemma fun_upds_apply: "⋀m ys.
(m(xs[↦]ys)) x =
(let xs' = take (size ys) xs
in if x ∈ set xs' then Some(ys ! index xs' x) else m x)"
(*<*)
apply(induct xs)
apply(case_tac ys)
done
(*>*)

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 ! index xs' x = y else m x = Some y)"

lemma map_upds_upd_conv_index:
"⟦x ∈ set xs; size xs ≤ size ys ⟧
⟹ m(xs[↦]ys, x↦y) = m(xs[↦]ys[index xs x := y])"
(*<*)
apply(rule ext)
done
(*>*)

lemma image_index:
"A ⊆ set(xs@[x]) ⟹ index (xs @ [x])  A =
(if x ∈ A then insert (size xs) (index xs  (A-{x})) else index xs  A)"
(*<*)
apply(auto simp:image_def)
apply(rule bexI)
prefer 2 apply blast
apply simp
apply(rule ccontr)
apply(erule_tac x=xa in ballE)
prefer 2 apply blast
apply(subgoal_tac "x ≠ xa")
prefer 2 apply blast
apply(subgoal_tac "x ≠ xa")
prefer 2 apply blast
apply(force)
done
(*>*)

lemma index_le_lengthD: "index xs x < length xs ⟹ x ∈ set xs"
by(erule contrapos_pp)(simp)

lemma not_hidden_index_nth: "⟦ i < length Vs; ¬ hidden Vs i ⟧ ⟹ index Vs (Vs ! i) = i"
by(induct Vs arbitrary: i)(auto split: if_split_asm nat.split_asm simp add: nth_Cons hidden_def)

lemma hidden_snoc_nth:
assumes len: "i < length Vs"
shows "hidden (Vs @ [Vs ! i]) i"
proof(cases "hidden Vs i")
case True thus ?thesis by simp
next
case False
with len have "index Vs (Vs ! i) = i" by(rule not_hidden_index_nth)
moreover from len have "hidden (Vs @ [Vs ! i]) (index Vs (Vs ! i))"
by(auto intro: hidden_index)
ultimately show ?thesis by simp
qed

lemma map_upds_Some_eq_nth_index:
assumes "[Vs [↦] vs] V = Some v" "length Vs ≤ length vs"
shows "vs ! index Vs V = v"
proof -
from ‹[Vs [↦] vs] V = Some v› have "V ∈ set Vs"
by -(rule classical, auto)
with ‹[Vs [↦] vs] V = Some v› ‹length Vs ≤ length vs› show ?thesis
proof(induct Vs arbitrary: vs)
case Nil thus ?case by simp
next
case (Cons x xs ys)
note IH = ‹⋀vs. ⟦ [xs [↦] vs] V = Some v; length xs ≤ length vs; V ∈ set xs ⟧ ⟹ vs ! index xs V = v›
from ‹[x # xs [↦] ys] V = Some v› obtain y Ys where "ys = y # Ys" by(cases ys, auto)
with ‹length (x # xs) ≤ length ys› have "length xs ≤ length Ys" by simp
show ?case
proof(cases "V ∈ set xs")
case True
with ‹[x # xs [↦] ys] V = Some v› ‹length xs ≤ length Ys› ‹ys = y # Ys›
have "[xs [↦] Ys] V = Some v"
apply(auto simp add: map_upds_def map_of_eq_None_iff set_zip image_Collect split: if_split_asm)
apply(hypsubst_thin)
apply(erule_tac x="length ys" in allE)
by(simp)
with IH[OF this ‹length xs ≤ length Ys› True] ‹ys = y # Ys› True
show ?thesis by(simp)
next
case False with ‹V ∈ set (x # xs)› have "x = V" by auto
with False ‹[x # xs [↦] ys] V = Some v› ‹ys = y # Ys› have "y = v"
by(auto)
with False ‹x = V› ‹ys = y # Ys›
show ?thesis by(simp)
qed
qed
qed

end
`