Theory Index

(*  Title:      HOL/MicroJava/Comp/Index.thy
    Author:     Martin Strecker
*)

(* Index of variable in list of parameter names and local variables *)

theory Index
imports AuxLemmas DefsComp
begin

(*indexing a variable name among all variable declarations in a method body*)
definition index :: "java_mb => vname => nat" where
 "index ==  λ (pn,lv,blk,res) v.
  if v = This
  then 0 
  else Suc (length (takeWhile (λ z. z~=v) (pn @ map fst lv)))"


lemma index_length_pns: "
  ⟦ i = index (pns,lvars,blk,res) vn;
  wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res));
  vn ∈ set pns⟧
  ⟹ 0 < i ∧ i < Suc (length pns)"
  apply (simp add: wf_java_mdecl_def index_def)
  apply (subgoal_tac "vn ≠ This")
   apply (auto intro: length_takeWhile)
  done

lemma index_length_lvars: "
  ⟦ i = index (pns,lvars,blk,res) vn;
  wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res));
  vn ∈ set (map fst lvars)⟧
  ⟹ (length pns) < i ∧ i < Suc((length pns) + (length lvars))"
  apply (simp add: wf_java_mdecl_def index_def)
  apply (subgoal_tac "vn ≠ This")
   apply simp
   apply (subgoal_tac "∀ x ∈ set pns. (λz. z ≠ vn) x")
    apply simp
    apply (subgoal_tac "length (takeWhile (λz. z ≠ vn) (map fst lvars)) < length (map fst lvars)")
     apply simp
    apply (rule length_takeWhile)
    apply simp
   apply (simp add: map_of_in_set)
   apply (intro strip notI) 
   apply simp 
  apply blast
  done


(***  index  ***)

lemma select_at_index : 
  "x ∈ set (gjmb_plns (gmb G C S)) ∨ x = This
  ⟹ (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) = the (loc x)"
  apply (simp only: index_def gjmb_plns_def)
  apply (case_tac "gmb G C S" rule: prod.exhaust)
  apply (simp add: galldefs del: set_append map_append)
  apply (rename_tac a b)
  apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
  apply (intro strip)
  apply (simp del: set_append map_append)
  apply (frule length_takeWhile)
  apply (frule_tac f = "(the ∘ loc)" in nth_map)
  apply simp
  done

lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))"
  by auto

lemma update_at_index: "
  ⟦ distinct (gjmb_plns (gmb G C S));
  x ∈ set (gjmb_plns (gmb G C S)); x ≠ This ⟧ ⟹
  (locvars_xstate G C S (Norm (h, l)))[index (gmb G C S) x := val] =
  locvars_xstate G C S (Norm (h, l(x↦val)))"
  apply (simp only: locvars_xstate_def locvars_locals_def index_def)
  apply (case_tac "gmb G C S" rule: prod.exhaust, simp)
  apply (rename_tac a b)
  apply (case_tac b, simp)
  apply (rule conjI)
   apply (simp add: gl_def)
  apply (simp add: galldefs del: set_append map_append)
  done


(* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same 
  way in the second case as in the first case ? *)
lemma index_of_var: "⟦ xvar ∉ set pns; xvar ∉ set (map fst zs); xvar ≠ This ⟧
  ⟹ index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)"
  apply (simp add: index_def)
  apply (subgoal_tac "(⋀x. ((x ∈ (set pns)) ⟹ ((λz. (z ≠ xvar))x)))")
   apply simp
   apply (subgoal_tac "(takeWhile (λz. z ≠ xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (λz. z ≠ xvar) (xvar # map fst xys))")
    apply simp
   apply (rule List.takeWhile_append2)
   apply auto
  done




(* The following definition should replace the conditions in WellType.thy / wf_java_mdecl
*)
definition disjoint_varnames :: "[vname list, (vname × ty) list] ⇒ bool" where
  "disjoint_varnames pns lvars ≡ 
  distinct pns ∧ unique lvars ∧ This ∉ set pns ∧ This ∉ set (map fst lvars) ∧ 
  (∀pn∈set pns. pn ∉ set (map fst lvars))"


lemma index_of_var2: "
  disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post)
  ⟹ index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn =
  Suc (length pns + length lvars_pre)"
  apply (simp add: disjoint_varnames_def index_def unique_def)
  apply (subgoal_tac "vn ≠ This", simp)
   apply (subgoal_tac
    "takeWhile (λz. z ≠ vn) (map fst lvars_pre @ vn # map fst lvars_post) =
    map fst lvars_pre @ takeWhile (λz. z ≠ vn) (vn # map fst lvars_post)")
    apply simp
   apply (rule List.takeWhile_append2)
   apply auto
  done

lemma wf_java_mdecl_disjoint_varnames: 
  "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res))
  ⟹ disjoint_varnames pns lvars"
  apply (cases S)
  apply (simp add: wf_java_mdecl_def disjoint_varnames_def  map_of_in_set)
  done

lemma wf_java_mdecl_length_pTs_pns: 
  "wf_java_mdecl G C ((mn, pTs), rT, pns, lvars, blk, res)
  ⟹ length pTs = length pns"
  by (simp add: wf_java_mdecl_def)

end