equal
deleted
inserted
replaced
3 Author: Martin Strecker |
3 Author: Martin Strecker |
4 *) |
4 *) |
5 |
5 |
6 (* Index of variable in list of parameter names and local variables *) |
6 (* Index of variable in list of parameter names and local variables *) |
7 |
7 |
8 theory Index imports AuxLemmas DefsComp begin |
8 theory Index |
|
9 imports AuxLemmas DefsComp |
|
10 begin |
9 |
11 |
10 (*indexing a variable name among all variable declarations in a method body*) |
12 (*indexing a variable name among all variable declarations in a method body*) |
11 constdefs |
13 constdefs |
12 index :: "java_mb => vname => nat" |
14 index :: "java_mb => vname => nat" |
13 "index == \<lambda> (pn,lv,blk,res) v. |
15 "index == \<lambda> (pn,lv,blk,res) v. |
74 apply (simp only: locvars_xstate_def locvars_locals_def index_def) |
76 apply (simp only: locvars_xstate_def locvars_locals_def index_def) |
75 apply (case_tac "(gmb G C S)", simp) |
77 apply (case_tac "(gmb G C S)", simp) |
76 apply (case_tac b, simp) |
78 apply (case_tac b, simp) |
77 apply (rule conjI) |
79 apply (rule conjI) |
78 apply (simp add: gl_def) |
80 apply (simp add: gl_def) |
79 apply (intro strip, simp) |
|
80 apply (simp add: galldefs del: set_append map_append) |
81 apply (simp add: galldefs del: set_append map_append) |
81 done |
82 done |
82 |
83 |
83 |
84 |
84 (* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same |
85 (* !!!! incomprehensible: why can't List.takeWhile_append2 be applied the same |