Theory ListIndex
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)"
by(simp add:inj_on_def)
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(auto simp add:hidden_def index_less_aux nth_append)
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"
by(auto simp add:hidden_def nth_append)
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 (simp add:Let_def)
apply(case_tac ys)
apply (simp add:Let_def)
apply (simp add:Let_def)
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)"
by(simp add:fun_upds_apply Let_def)
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)
apply(simp add:fun_upds_apply index_less_aux eq_sym_conv Let_def)
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(fastforce simp add:neq_commute)
apply(subgoal_tac "x ≠ xa")
prefer 2 apply blast
apply(fastforce simp add:neq_commute)
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(clarsimp simp add: in_set_conv_decomp)
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