(* Title: HOL/MicroJava/Comp/DefsComp.thy ID: $Id: DefsComp.thy,v 1.4 2005/02/01 17:02:05 paulson Exp $ Author: Martin Strecker *) (* Definitions for accessing parts of methods, states etc. *) theory DefsComp imports "../JVM/JVMExec" begin constdefs method_rT :: "cname × ty × 'c => ty" "method_rT mtd == (fst (snd mtd))" constdefs (* g = get *) gx :: "xstate => val option" "gx ≡ fst" gs :: "xstate => state" "gs ≡ snd" gh :: "xstate => aheap" "gh ≡ fstosnd" gl :: "xstate => State.locals" "gl ≡ sndosnd" gmb :: "'a prog => cname => sig => 'a" "gmb G cn si ≡ snd(snd(the(method (G,cn) si)))" gis :: "jvm_method => bytecode" "gis ≡ fst o snd o snd" (* jmb = aus einem JavaMaethodBody *) gjmb_pns :: "java_mb => vname list" "gjmb_pns ≡ fst" gjmb_lvs :: "java_mb => (vname×ty)list" "gjmb_lvs ≡ fstosnd" gjmb_blk :: "java_mb => stmt" "gjmb_blk ≡ fstosndosnd" gjmb_res :: "java_mb => expr" "gjmb_res ≡ sndosndosnd" gjmb_plns :: "java_mb => vname list" "gjmb_plns ≡ λjmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)" glvs :: "java_mb => State.locals => locvars" "glvs jmb loc ≡ map (theoloc) (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 constdefs locvars_locals :: "java_mb prog => cname => sig => State.locals => locvars" "locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs" locals_locvars :: "java_mb prog => cname => sig => locvars => State.locals" "locals_locvars G C S lvs == empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))" locvars_xstate :: "java_mb prog => cname => sig => xstate => locvars" "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
lemmas gdefs:
gx == fst
gh == fst o snd
gl == snd o snd
gmb G cn si == snd (snd (the (method (G, cn) si)))
gis == fst o snd o snd
glvs jmb loc == map (the o loc) (gjmb_plns jmb)
lemmas gdefs:
gx == fst
gh == fst o snd
gl == snd o snd
gmb G cn si == snd (snd (the (method (G, cn) si)))
gis == fst o snd o snd
glvs jmb loc == map (the o loc) (gjmb_plns jmb)
lemmas gjmbdefs:
gjmb_pns == fst
gjmb_lvs == fst o snd
gjmb_blk == fst o snd o snd
gjmb_res == snd o snd o snd
gjmb_plns == %jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)
lemmas gjmbdefs:
gjmb_pns == fst
gjmb_lvs == fst o snd
gjmb_blk == fst o snd o snd
gjmb_res == snd o snd o snd
gjmb_plns == %jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)
lemmas galldefs:
gx == fst
gh == fst o snd
gl == snd o snd
gmb G cn si == snd (snd (the (method (G, cn) si)))
gis == fst o snd o snd
glvs jmb loc == map (the o loc) (gjmb_plns jmb)
gjmb_pns == fst
gjmb_lvs == fst o snd
gjmb_blk == fst o snd o snd
gjmb_res == snd o snd o snd
gjmb_plns == %jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)
lemmas galldefs:
gx == fst
gh == fst o snd
gl == snd o snd
gmb G cn si == snd (snd (the (method (G, cn) si)))
gis == fst o snd o snd
glvs jmb loc == map (the o loc) (gjmb_plns jmb)
gjmb_pns == fst
gjmb_lvs == fst o snd
gjmb_blk == fst o snd o snd
gjmb_res == snd o snd o snd
gjmb_plns == %jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)
lemma locvars_xstate_par_dep:
lv1.0 = lv2.0 ==> locvars_xstate G C S (xcpt1.0, hp1.0, lv1.0) = locvars_xstate G C S (xcpt2.0, hp2.0, lv2.0)
lemma gx_conv:
gx (xcpt, s) = xcpt
lemma gh_conv:
gh (xcpt, h, l) = h