Theory DefsComp

(*  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  fstsnd"

definition
  gl :: "xstate  State.locals" where "gl  sndsnd"

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  fstsnd"

definition
  gjmb_blk  :: "java_mb  stmt" where  "gjmb_blk  fstsndsnd"

definition
  gjmb_res  :: "java_mb  expr" where  "gjmb_res  sndsndsnd"

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 (theloc) (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))[↦](tl lvs), This(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