author | haftmann |
Tue, 24 Nov 2009 14:37:23 +0100 | |
changeset 33954 | 1bc3b688548c |
parent 32960 | 69916a850301 |
child 35416 | d8d7d1b785af |
permissions | -rwxr-xr-x |
13673 | 1 |
(* Title: HOL/MicroJava/Comp/Index.thy |
2 |
Author: Martin Strecker |
|
3 |
*) |
|
4 |
||
5 |
(* Index of variable in list of parameter names and local variables *) |
|
6 |
||
17778 | 7 |
theory Index |
8 |
imports AuxLemmas DefsComp |
|
9 |
begin |
|
13673 | 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) |
|
27117 | 56 |
apply (case_tac "gmb G C S" rule: prod.exhaust) |
13673 | 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 |
||
14045 | 66 |
lemma lift_if: "(f (if b then t else e)) = (if b then (f t) else (f e))" |
67 |
apply auto |
|
68 |
done |
|
69 |
||
13673 | 70 |
lemma update_at_index: " |
71 |
\<lbrakk> distinct (gjmb_plns (gmb G C S)); |
|
72 |
x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> |
|
73 |
locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] = |
|
74 |
locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))" |
|
75 |
apply (simp only: locvars_xstate_def locvars_locals_def index_def) |
|
27117 | 76 |
apply (case_tac "gmb G C S" rule: prod.exhaust, simp) |
13673 | 77 |
apply (case_tac b, simp) |
78 |
apply (rule conjI) |
|
79 |
apply (simp add: gl_def) |
|
80 |
apply (simp add: galldefs del: set_append map_append) |
|
81 |
done |
|
82 |
||
83 |
||
84 |
(* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same |
|
85 |
way in the second case as in the first case ? *) |
|
86 |
lemma index_of_var: "\<lbrakk> xvar \<notin> set pns; xvar \<notin> set (map fst zs); xvar \<noteq> This \<rbrakk> |
|
87 |
\<Longrightarrow> index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)" |
|
88 |
apply (simp add: index_def) |
|
89 |
apply (subgoal_tac "(\<And>x. ((x \<in> (set pns)) \<Longrightarrow> ((\<lambda>z. (z \<noteq> xvar))x)))") |
|
90 |
apply (simp add: List.takeWhile_append2) |
|
91 |
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))") |
|
92 |
apply simp |
|
93 |
apply (rule List.takeWhile_append2) |
|
94 |
apply auto |
|
95 |
done |
|
96 |
||
97 |
||
98 |
||
99 |
||
100 |
(* The following def should replace the conditions in WellType.thy / wf_java_mdecl |
|
101 |
*) |
|
102 |
constdefs |
|
103 |
disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" |
|
104 |
(* This corresponds to the original def in wf_java_mdecl: |
|
105 |
"disjoint_varnames pns lvars \<equiv> |
|
106 |
nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27117
diff
changeset
|
107 |
(\<forall>pn\<in>set pns. map_of lvars pn = None)" |
13673 | 108 |
*) |
109 |
||
110 |
"disjoint_varnames pns lvars \<equiv> |
|
111 |
distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
|
112 |
(\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))" |
|
113 |
||
114 |
||
115 |
lemma index_of_var2: " |
|
116 |
disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post) |
|
117 |
\<Longrightarrow> index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn = |
|
118 |
Suc (length pns + length lvars_pre)" |
|
119 |
apply (simp add: disjoint_varnames_def index_def unique_def distinct_append) |
|
120 |
apply (subgoal_tac "vn \<noteq> This", simp) |
|
121 |
apply (subgoal_tac |
|
122 |
"takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars_pre @ vn # map fst lvars_post) = |
|
123 |
map fst lvars_pre @ takeWhile (\<lambda>z. z \<noteq> vn) (vn # map fst lvars_post)") |
|
124 |
apply simp |
|
125 |
apply (rule List.takeWhile_append2) |
|
126 |
apply auto |
|
127 |
done |
|
128 |
||
129 |
lemma wf_java_mdecl_disjoint_varnames: |
|
130 |
"wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) |
|
131 |
\<Longrightarrow> disjoint_varnames pns lvars" |
|
132 |
apply (case_tac S) |
|
133 |
apply (simp add: wf_java_mdecl_def disjoint_varnames_def map_of_in_set) |
|
134 |
done |
|
135 |
||
136 |
lemma wf_java_mdecl_length_pTs_pns: |
|
137 |
"wf_java_mdecl G C ((mn, pTs), rT, pns, lvars, blk, res) |
|
138 |
\<Longrightarrow> length pTs = length pns" |
|
139 |
by (simp add: wf_java_mdecl_def) |
|
140 |
||
141 |
end |