(* 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)" :: "'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 : "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 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 : "⟦ 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 : 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