|
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 |