|
(* Title: HOL/MicroJava/Comp/DefsComp.thy
Author: Martin Strecker
*)
(* Definitions for accessing parts of methods, states etc. *)
theory DefsComp
imports "../JVM/JVMExec"
begin
definition method_rT :: "cname \ ty \ 'c \ ty" where
"method_rT mtd == (fst (snd mtd))"
(* g = get *)
definition
gx :: "xstate \ val option" where "gx \ fst"
definition
gs :: "xstate \ state" where "gs \ snd"
definition
gh :: "xstate \ aheap" where "gh \ fst\snd"
definition
gl :: "xstate \ State.locals" where "gl \ snd\snd"
definition
gmb :: "'a prog \ cname \ sig \ 'a"
where "gmb G cn si \ snd(snd(the(method (G,cn) si)))"
definition
gis :: "jvm_method \ bytecode"
where "gis \ fst \ snd \ snd"
(* jmb = aus einem JavaMaethodBody *)
definition
gjmb_pns :: "java_mb \ vname list" where "gjmb_pns \ fst"
definition
gjmb_lvs :: "java_mb \ (vname\ty)list" where "gjmb_lvs \ fst\snd"
definition
gjmb_blk :: "java_mb \ stmt" where "gjmb_blk \ fst\snd\snd"
definition
gjmb_res :: "java_mb \ expr" where "gjmb_res \ snd\snd\snd"
definition
gjmb_plns :: "java_mb \ vname list"
where "gjmb_plns \ \jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
definition
glvs :: "java_mb \ State.locals \ locvars"
where "glvs jmb loc \ map (the\loc) (gjmb_plns jmb)"
lemmas gdefs = gx_def gh_def gl_def gmb_def gis_def glvs_def
lemmas gjmbdefs = gjmb_pns_def gjmb_lvs_def gjmb_blk_def gjmb_res_def gjmb_plns_def
lemmas galldefs = gdefs gjmbdefs
definition locvars_locals :: "java_mb prog \ cname \ sig \ State.locals \ locvars" where
"locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs"
definition locals_locvars :: "java_mb prog \ cname \ sig \ locvars \ State.locals" where
"locals_locvars G C S lvs ==
Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))"
definition locvars_xstate :: "java_mb prog \ cname \ sig \ xstate \ locvars" where
"locvars_xstate G C S xs == locvars_locals G C S (gl xs)"
lemma locvars_xstate_par_dep:
"lv1 = lv2 \
locvars_xstate G C S (xcpt1, hp1, lv1) = locvars_xstate G C S (xcpt2, hp2, lv2)"
by (simp add: locvars_xstate_def gl_def)
(**********************************************************************)
(* Conversions *)
lemma gx_conv [simp]: "gx (xcpt, s) = xcpt" by (simp add: gx_def)
lemma gh_conv [simp]: "gh (xcpt, h, l) = h" by (simp add: gh_def)
end
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
