|
13673
|
1 |
(* Title: HOL/MicroJava/Comp/DefsComp.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Martin Strecker
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
(* Definitions for accessing parts of methods, states etc. *)
|
|
|
7 |
|
|
15481
|
8 |
theory DefsComp
|
|
|
9 |
imports "../JVM/JVMExec"
|
|
|
10 |
begin
|
|
13673
|
11 |
|
|
|
12 |
|
|
|
13 |
constdefs
|
|
|
14 |
method_rT :: "cname \<times> ty \<times> 'c \<Rightarrow> ty"
|
|
|
15 |
"method_rT mtd == (fst (snd mtd))"
|
|
|
16 |
|
|
|
17 |
|
|
|
18 |
constdefs
|
|
|
19 |
(* g = get *)
|
|
|
20 |
gx :: "xstate \<Rightarrow> val option" "gx \<equiv> fst"
|
|
|
21 |
gs :: "xstate \<Rightarrow> state" "gs \<equiv> snd"
|
|
|
22 |
gh :: "xstate \<Rightarrow> aheap" "gh \<equiv> fst\<circ>snd"
|
|
|
23 |
gl :: "xstate \<Rightarrow> State.locals" "gl \<equiv> snd\<circ>snd"
|
|
|
24 |
|
|
|
25 |
gmb :: "'a prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 'a"
|
|
|
26 |
"gmb G cn si \<equiv> snd(snd(the(method (G,cn) si)))"
|
|
|
27 |
gis :: "jvm_method \<Rightarrow> bytecode"
|
|
|
28 |
"gis \<equiv> fst \<circ> snd \<circ> snd"
|
|
|
29 |
|
|
|
30 |
(* jmb = aus einem JavaMaethodBody *)
|
|
|
31 |
gjmb_pns :: "java_mb \<Rightarrow> vname list" "gjmb_pns \<equiv> fst"
|
|
|
32 |
gjmb_lvs :: "java_mb \<Rightarrow> (vname\<times>ty)list" "gjmb_lvs \<equiv> fst\<circ>snd"
|
|
|
33 |
gjmb_blk :: "java_mb \<Rightarrow> stmt" "gjmb_blk \<equiv> fst\<circ>snd\<circ>snd"
|
|
|
34 |
gjmb_res :: "java_mb \<Rightarrow> expr" "gjmb_res \<equiv> snd\<circ>snd\<circ>snd"
|
|
|
35 |
gjmb_plns :: "java_mb \<Rightarrow> vname list"
|
|
|
36 |
"gjmb_plns \<equiv> \<lambda>jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
|
|
14653
|
37 |
|
|
|
38 |
glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
|
|
|
39 |
"glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
|
|
13673
|
40 |
|
|
|
41 |
lemmas gdefs = gx_def gh_def gl_def gmb_def gis_def glvs_def
|
|
|
42 |
lemmas gjmbdefs = gjmb_pns_def gjmb_lvs_def gjmb_blk_def gjmb_res_def gjmb_plns_def
|
|
|
43 |
|
|
|
44 |
lemmas galldefs = gdefs gjmbdefs
|
|
|
45 |
|
|
|
46 |
|
|
|
47 |
|
|
|
48 |
constdefs
|
|
|
49 |
locvars_locals :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> State.locals \<Rightarrow> locvars"
|
|
|
50 |
"locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs"
|
|
|
51 |
|
|
|
52 |
locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals"
|
|
|
53 |
"locals_locvars G C S lvs ==
|
|
|
54 |
empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))"
|
|
|
55 |
|
|
|
56 |
locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars"
|
|
|
57 |
"locvars_xstate G C S xs == locvars_locals G C S (gl xs)"
|
|
|
58 |
|
|
|
59 |
|
|
|
60 |
lemma locvars_xstate_par_dep:
|
|
|
61 |
"lv1 = lv2 \<Longrightarrow>
|
|
|
62 |
locvars_xstate G C S (xcpt1, hp1, lv1) = locvars_xstate G C S (xcpt2, hp2, lv2)"
|
|
|
63 |
by (simp add: locvars_xstate_def gl_def)
|
|
|
64 |
|
|
|
65 |
|
|
|
66 |
|
|
|
67 |
|
|
|
68 |
(**********************************************************************)
|
|
|
69 |
(* Conversions *)
|
|
|
70 |
|
|
|
71 |
|
|
|
72 |
lemma gx_conv [simp]: "gx (xcpt, s) = xcpt" by (simp add: gx_def)
|
|
|
73 |
|
|
|
74 |
lemma gh_conv [simp]: "gh (xcpt, h, l) = h" by (simp add: gh_def)
|
|
|
75 |
|
|
|
76 |
|
|
|
77 |
end
|