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)"
(*<*)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, xy) = 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