Theory Index

(*  Title:      Jinja/Compiler/Index.thy
    ID:         $Id: Index.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

header {* \isaheader{Indexing variables in variable lists} *}

theory Index =  Main:

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: *}

consts
  index :: "'a list => 'a => nat"
primrec
  "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)"

constdefs
  hidden :: "'a list => nat => bool"
  "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(fastsimp)
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:split_if_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[\<mapsto>]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[\<mapsto>]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[\<mapsto>]ys)(x\<mapsto>y) = m(xs[\<mapsto>]ys[index xs x := y])"
(*<*)
apply(rule ext)
apply(simp add:fun_upds_apply index_less_aux eq_sym_conv Let_def)
done
(*>*)


end