|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
sq107a.cob
Sprache: Unknown
(* 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
[ Seitenstruktur0.0Drucken
etwas mehr zur Ethik
]
|
|
|
|
|
|
