src/HOL/MicroJava/Comp/DefsComp.thy

--- a/src/HOL/MicroJava/Comp/DefsComp.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/Comp/DefsComp.thy
-    ID:         $Id$
     Author:     Martin Strecker
 *)
 
@@ -10,50 +9,65 @@
 begin
 
 
-constdefs
-  method_rT :: "cname \<times> ty \<times> 'c \<Rightarrow> ty"
+definition method_rT :: "cname \<times> ty \<times> 'c \<Rightarrow> ty" where
   "method_rT mtd == (fst (snd mtd))"
 
 
-constdefs
 (* g = get *)
-  gx :: "xstate \<Rightarrow> val option"  "gx \<equiv> fst"
-  gs :: "xstate \<Rightarrow> state"  "gs \<equiv> snd"
-  gh :: "xstate \<Rightarrow> aheap"        "gh \<equiv> fst\<circ>snd"
-  gl :: "xstate \<Rightarrow> State.locals" "gl \<equiv> snd\<circ>snd"
+definition
+  gx :: "xstate \<Rightarrow> val option" where "gx \<equiv> fst"
+
+definition
+  gs :: "xstate \<Rightarrow> state" where "gs \<equiv> snd"
+
+definition
+  gh :: "xstate \<Rightarrow> aheap" where "gh \<equiv> fst\<circ>snd"
 
+definition
+  gl :: "xstate \<Rightarrow> State.locals" where "gl \<equiv> snd\<circ>snd"
+
+definition
   gmb :: "'a prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 'a"
-    "gmb G cn si \<equiv> snd(snd(the(method (G,cn) si)))"
+    where "gmb G cn si \<equiv> snd(snd(the(method (G,cn) si)))"
+
+definition
   gis :: "jvm_method \<Rightarrow> bytecode"
-    "gis \<equiv> fst \<circ> snd \<circ> snd"
+    where "gis \<equiv> fst \<circ> snd \<circ> snd"
 
 (* jmb = aus einem JavaMaethodBody *)
-  gjmb_pns  :: "java_mb \<Rightarrow> vname list"     "gjmb_pns \<equiv> fst"
-  gjmb_lvs  :: "java_mb \<Rightarrow> (vname\<times>ty)list" "gjmb_lvs \<equiv> fst\<circ>snd"
-  gjmb_blk  :: "java_mb \<Rightarrow> stmt"           "gjmb_blk \<equiv> fst\<circ>snd\<circ>snd"
-  gjmb_res  :: "java_mb \<Rightarrow> expr"           "gjmb_res \<equiv> snd\<circ>snd\<circ>snd"
+definition
+  gjmb_pns  :: "java_mb \<Rightarrow> vname list" where "gjmb_pns \<equiv> fst"
+
+definition
+  gjmb_lvs  :: "java_mb \<Rightarrow> (vname\<times>ty)list" where  "gjmb_lvs \<equiv> fst\<circ>snd"
+
+definition
+  gjmb_blk  :: "java_mb \<Rightarrow> stmt" where  "gjmb_blk \<equiv> fst\<circ>snd\<circ>snd"
+
+definition
+  gjmb_res  :: "java_mb \<Rightarrow> expr" where  "gjmb_res \<equiv> snd\<circ>snd\<circ>snd"
+
+definition
   gjmb_plns :: "java_mb \<Rightarrow> vname list"
-    "gjmb_plns \<equiv> \<lambda>jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
+    where  "gjmb_plns \<equiv> \<lambda>jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
 
+definition
   glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
-    "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
+    where "glvs jmb loc \<equiv> map (the\<circ>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
 
-
-
-constdefs 
-  locvars_locals :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> State.locals \<Rightarrow> locvars"
+definition locvars_locals :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> State.locals \<Rightarrow> locvars" where
   "locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs"
 
-  locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals"
+definition locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals" where
   "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 \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars"
+definition locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars" where
   "locvars_xstate G C S xs == locvars_locals G C S (gl xs)"