src/HOL/MicroJava/Comp/DefsComp.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 15481 fc075ae929e4
child 35416 d8d7d1b785af
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
     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 
     8 theory DefsComp
     9 imports "../JVM/JVMExec"
    10 begin
    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)"
    37 
    38   glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
    39     "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
    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