13673
|
1 |
(* Title: HOL/MicroJava/Comp/Index.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Martin Strecker
|
|
4 |
Copyright GPL 2002
|
|
5 |
*)
|
|
6 |
|
|
7 |
(* Index of variable in list of parameter names and local variables *)
|
|
8 |
|
|
9 |
theory Index = AuxLemmas + DefsComp:
|
|
10 |
|
|
11 |
(*indexing a variable name among all variable declarations in a method body*)
|
|
12 |
constdefs
|
|
13 |
index :: "java_mb => vname => nat"
|
|
14 |
"index == \<lambda> (pn,lv,blk,res) v.
|
|
15 |
if v = This
|
|
16 |
then 0
|
|
17 |
else Suc (length (takeWhile (\<lambda> z. z~=v) (pn @ map fst lv)))"
|
|
18 |
|
|
19 |
|
|
20 |
lemma index_length_pns: "
|
|
21 |
\<lbrakk> i = index (pns,lvars,blk,res) vn;
|
|
22 |
wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res));
|
|
23 |
vn \<in> set pns\<rbrakk>
|
|
24 |
\<Longrightarrow> 0 < i \<and> i < Suc (length pns)"
|
|
25 |
apply (simp add: wf_java_mdecl_def index_def)
|
|
26 |
apply (subgoal_tac "vn \<noteq> This")
|
|
27 |
apply (auto intro: length_takeWhile)
|
|
28 |
done
|
|
29 |
|
|
30 |
lemma index_length_lvars: "
|
|
31 |
\<lbrakk> i = index (pns,lvars,blk,res) vn;
|
|
32 |
wf_java_mdecl G C ((mn,pTs),rT, (pns,lvars,blk,res));
|
|
33 |
vn \<in> set (map fst lvars)\<rbrakk>
|
|
34 |
\<Longrightarrow> (length pns) < i \<and> i < Suc((length pns) + (length lvars))"
|
|
35 |
apply (simp add: wf_java_mdecl_def index_def)
|
|
36 |
apply (subgoal_tac "vn \<noteq> This")
|
|
37 |
apply simp
|
|
38 |
apply (subgoal_tac "\<forall> x \<in> set pns. (\<lambda>z. z \<noteq> vn) x")
|
|
39 |
apply (simp add: takeWhile_append2)
|
|
40 |
apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars)) < length (map fst lvars)")
|
|
41 |
apply simp
|
|
42 |
apply (rule length_takeWhile)
|
|
43 |
apply simp
|
|
44 |
apply (simp add: map_of_in_set)
|
|
45 |
apply (intro strip notI) apply simp apply blast
|
|
46 |
done
|
|
47 |
|
|
48 |
|
|
49 |
(*** index ***)
|
|
50 |
|
|
51 |
lemma select_at_index :
|
|
52 |
"x \<in> set (gjmb_plns (gmb G C S)) \<or> x = This
|
|
53 |
\<Longrightarrow> (the (loc This) # glvs (gmb G C S) loc) ! (index (gmb G C S) x) =
|
|
54 |
the (loc x)"
|
|
55 |
apply (simp only: index_def gjmb_plns_def)
|
|
56 |
apply (case_tac "(gmb G C S)")
|
|
57 |
apply (simp add: galldefs del: set_append map_append)
|
|
58 |
apply (case_tac b, simp add: gmb_def gjmb_lvs_def del: set_append map_append)
|
|
59 |
apply (intro strip)
|
|
60 |
apply (simp del: set_append map_append)
|
|
61 |
apply (frule length_takeWhile)
|
|
62 |
apply (frule_tac f = "(the \<circ> loc)" in nth_map)
|
|
63 |
apply simp
|
|
64 |
done
|
|
65 |
|
|
66 |
lemma update_at_index: "
|
|
67 |
\<lbrakk> distinct (gjmb_plns (gmb G C S));
|
|
68 |
x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>
|
|
69 |
locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
|
|
70 |
locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
|
|
71 |
apply (simp only: locvars_xstate_def locvars_locals_def index_def)
|
|
72 |
apply (case_tac "(gmb G C S)", simp)
|
|
73 |
apply (case_tac b, simp)
|
|
74 |
apply (rule conjI)
|
|
75 |
apply (simp add: gl_def)
|
|
76 |
apply (intro strip, simp)
|
|
77 |
apply (simp add: galldefs del: set_append map_append)
|
|
78 |
apply (auto simp: the_map_upd)
|
|
79 |
done
|
|
80 |
|
|
81 |
|
|
82 |
(* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same
|
|
83 |
way in the second case as in the first case ? *)
|
|
84 |
lemma index_of_var: "\<lbrakk> xvar \<notin> set pns; xvar \<notin> set (map fst zs); xvar \<noteq> This \<rbrakk>
|
|
85 |
\<Longrightarrow> index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)"
|
|
86 |
apply (simp add: index_def)
|
|
87 |
apply (subgoal_tac "(\<And>x. ((x \<in> (set pns)) \<Longrightarrow> ((\<lambda>z. (z \<noteq> xvar))x)))")
|
|
88 |
apply (simp add: List.takeWhile_append2)
|
|
89 |
apply (subgoal_tac "(takeWhile (\<lambda>z. z \<noteq> xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (\<lambda>z. z \<noteq> xvar) (xvar # map fst xys))")
|
|
90 |
apply simp
|
|
91 |
apply (rule List.takeWhile_append2)
|
|
92 |
apply auto
|
|
93 |
done
|
|
94 |
|
|
95 |
|
|
96 |
|
|
97 |
|
|
98 |
(* The following def should replace the conditions in WellType.thy / wf_java_mdecl
|
|
99 |
*)
|
|
100 |
constdefs
|
|
101 |
disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool"
|
|
102 |
(* This corresponds to the original def in wf_java_mdecl:
|
|
103 |
"disjoint_varnames pns lvars \<equiv>
|
|
104 |
nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and>
|
|
105 |
(\<forall>pn\<in>set pns. map_of lvars pn = None)"
|
|
106 |
*)
|
|
107 |
|
|
108 |
"disjoint_varnames pns lvars \<equiv>
|
|
109 |
distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and>
|
|
110 |
(\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))"
|
|
111 |
|
|
112 |
|
|
113 |
lemma index_of_var2: "
|
|
114 |
disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post)
|
|
115 |
\<Longrightarrow> index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn =
|
|
116 |
Suc (length pns + length lvars_pre)"
|
|
117 |
apply (simp add: disjoint_varnames_def index_def unique_def distinct_append)
|
|
118 |
apply (subgoal_tac "vn \<noteq> This", simp)
|
|
119 |
apply (subgoal_tac
|
|
120 |
"takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars_pre @ vn # map fst lvars_post) =
|
|
121 |
map fst lvars_pre @ takeWhile (\<lambda>z. z \<noteq> vn) (vn # map fst lvars_post)")
|
|
122 |
apply simp
|
|
123 |
apply (rule List.takeWhile_append2)
|
|
124 |
apply auto
|
|
125 |
done
|
|
126 |
|
|
127 |
lemma wf_java_mdecl_disjoint_varnames:
|
|
128 |
"wf_java_mdecl G C (S,rT,(pns,lvars,blk,res))
|
|
129 |
\<Longrightarrow> disjoint_varnames pns lvars"
|
|
130 |
apply (case_tac S)
|
|
131 |
apply (simp add: wf_java_mdecl_def disjoint_varnames_def map_of_in_set)
|
|
132 |
done
|
|
133 |
|
|
134 |
lemma wf_java_mdecl_length_pTs_pns:
|
|
135 |
"wf_java_mdecl G C ((mn, pTs), rT, pns, lvars, blk, res)
|
|
136 |
\<Longrightarrow> length pTs = length pns"
|
|
137 |
by (simp add: wf_java_mdecl_def)
|
|
138 |
|
|
139 |
end
|