Quelle Index.thy Sprache: Isabelle

(*  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 (\<lambda> z. z~=v) (pn @ map fst lv)))"

lemma index_length_pns: "
  \<lbrakk> i = index (pns,lvars,blk,res) vn;
  wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res));
  vn \<in> set pns\<rbrakk>
  \<Longrightarrow> 0 < i \<and> 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: "
  \<lbrakk> i = index (pns,lvars,blk,res) vn;
  wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res));
  vn \<in> set (map fst lvars)\<rbrakk>
  \<Longrightarrow> (length pns) < i \<and> 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
  \<Longrightarrow> (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: "
  \<lbrakk> distinct (gjmb_plns (gmb G C S));
  x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>
  (locvars_xstate G C S (Norm (h, l)))[index (gmb G C S) x := val] =
  locvars_xstate G C S (Norm (h, l(x\<mapsto>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 \
  \<Longrightarrow> 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 \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and>
  (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))"

lemma index_of_var2: "
  disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post)
  \<Longrightarrow> 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 (\<lambda>z. z \<noteq> 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))
  \<Longrightarrow> 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)
  \<Longrightarrow> length pTs = length pns"
  by (simp add: wf_java_mdecl_def)

end

quality99%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.