cleanup, beautified

--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Thu Oct 24 12:06:43 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Thu Oct 24 12:07:31 2002 +0200
@@ -36,21 +36,21 @@
 
 consts
   check_instr :: "[instr, jvm_prog, aheap, opstack, locvars, 
-                  cname, sig, p_count, p_count, frame list] \<Rightarrow> bool"
+                  cname, sig, p_count, frame list] \<Rightarrow> bool"
 primrec 
-  "check_instr (Load idx) G hp stk vars C sig pc maxpc frs = 
+  "check_instr (Load idx) G hp stk vars C sig pc frs = 
   (idx < length vars)"
 
-  "check_instr (Store idx) G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr (Store idx) G hp stk vars Cl sig pc frs = 
   (0 < length stk \<and> idx < length vars)"
 
-  "check_instr (LitPush v) G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr (LitPush v) G hp stk vars Cl sig pc frs = 
   (\<not>isAddr v)"
 
-  "check_instr (New C) G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr (New C) G hp stk vars Cl sig pc frs = 
   is_class G C"
 
-  "check_instr (Getfield F C) G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
   (0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
   (let (C', T) = the (field (G,C) F); ref = hd stk in 
     C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 
@@ -58,7 +58,7 @@
       (let (D,vs) = the (hp (the_Addr ref)) in 
         G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" 
 
-  "check_instr (Putfield F C) G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr (Putfield F C) G hp stk vars Cl sig pc frs = 
   (1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
   (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in 
     C' = C \<and> isRef ref \<and> (ref \<noteq> Null \<longrightarrow> 
@@ -66,11 +66,10 @@
       (let (D,vs) = the (hp (the_Addr ref)) in 
         G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))" 
 
-  "check_instr (Checkcast C) G hp stk vars Cl sig pc maxpc frs =
+  "check_instr (Checkcast C) G hp stk vars Cl sig pc frs =
   (0 < length stk \<and> is_class G C \<and> isRef (hd stk))"
 
-
-  "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc maxpc frs =
+  "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc frs =
   (length ps < length stk \<and> 
   (let n = length ps; v = stk!n in
   isRef v \<and> (v \<noteq> Null \<longrightarrow> 
@@ -78,37 +77,37 @@
     method (G,cname_of hp v) (mn,ps) \<noteq> None \<and>
     list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))"
   
-  "check_instr Return G hp stk0 vars Cl sig0 pc maxpc frs =
+  "check_instr Return G hp stk0 vars Cl sig0 pc frs =
   (0 < length stk0 \<and> (0 < length frs \<longrightarrow> 
     method (G,Cl) sig0 \<noteq> None \<and>    
     (let v = hd stk0;  (C, rT, body) = the (method (G,Cl) sig0) in
     Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT)))"
  
-  "check_instr Pop G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr Pop G hp stk vars Cl sig pc frs = 
   (0 < length stk)"
 
-  "check_instr Dup G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr Dup G hp stk vars Cl sig pc frs = 
   (0 < length stk)"
 
-  "check_instr Dup_x1 G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr Dup_x1 G hp stk vars Cl sig pc frs = 
   (1 < length stk)"
 
-  "check_instr Dup_x2 G hp stk vars Cl sig pc maxpc frs = 
+  "check_instr Dup_x2 G hp stk vars Cl sig pc frs = 
   (2 < length stk)"
 
-  "check_instr Swap G hp stk vars Cl sig pc maxpc frs =
+  "check_instr Swap G hp stk vars Cl sig pc frs =
   (1 < length stk)"
 
-  "check_instr IAdd G hp stk vars Cl sig pc maxpc frs =
+  "check_instr IAdd G hp stk vars Cl sig pc frs =
   (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))"
 
-  "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc maxpc frs =
-  (1 < length stk \<and> 0 \<le> int pc+b \<and> nat(int pc+b) < maxpc)"
+  "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc frs =
+  (1 < length stk \<and> 0 \<le> int pc+b)"
 
-  "check_instr (Goto b) G hp stk vars Cl sig pc maxpc frs =
-  (0 \<le> int pc+b \<and> nat(int pc+b) < maxpc)"
+  "check_instr (Goto b) G hp stk vars Cl sig pc frs =
+  (0 \<le> int pc+b)"
 
-  "check_instr Throw G hp stk vars Cl sig pc maxpc frs =
+  "check_instr Throw G hp stk vars Cl sig pc frs =
   (0 < length stk \<and> isRef (hd stk))"
 
 constdefs
@@ -116,7 +115,8 @@
   "check G s \<equiv> let (xcpt, hp, frs) = s in
                (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> 
                 (let ins = fifth (the (method (G,C) sig)); i = ins!pc in
-                 check_instr i G hp stk loc C sig pc (length ins) frs'))"
+                 pc < size ins \<and>
+                 check_instr i G hp stk loc C sig pc frs'))"
 
 
   exec_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state option type_error"

--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Oct 24 12:06:43 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Oct 24 12:07:31 2002 +0200
@@ -28,19 +28,17 @@
   (let (oref,xp') = new_Addr hp;
        fs   = init_vars (fields(G,C));
        hp'  = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
-       stk' = if xp'=None then (Addr oref)#stk else stk;
        pc'  = if xp'=None then pc+1 else pc
    in 
-      (xp', hp', (stk', vars, Cl, sig, pc')#frs))"
+      (xp', hp', (Addr oref#stk, vars, Cl, sig, pc')#frs))"
 
  "exec_instr (Getfield F C) G hp stk vars Cl sig pc frs = 
   (let oref = hd stk;
        xp'  = raise_system_xcpt (oref=Null) NullPointer;
        (oc,fs)  = the(hp(the_Addr oref));
-       stk' = if xp'=None then the(fs(F,C))#(tl stk) else tl stk;
        pc'  = if xp'=None then pc+1 else pc
    in
-      (xp', hp, (stk', vars, Cl, sig, pc')#frs))"
+      (xp', hp, (the(fs(F,C))#(tl stk), vars, Cl, sig, pc')#frs))"
 
  "exec_instr (Putfield F C) G hp stk vars Cl sig pc frs = 
   (let (fval,oref)= (hd stk, hd(tl stk));