# HG changeset patch
# User kleing
# Date 976202559 -3600
# Node ID 022c6b2bcd6bb5f55a7dbadbe9708c06fcd2c955
# Parent  850fdf9ce787d8a1c8e525476dbd1e1ecab0d437
strengthened invariant: current class must be defined

diff -r 850fdf9ce787 -r 022c6b2bcd6b src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Thu Dec 07 16:21:47 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Dec 07 16:22:39 2000 +0100
@@ -39,9 +39,9 @@
 "correct_frames G hp phi rT0 sig0 (f#frs) =
 	(let (stk,loc,C,sig,pc) = f in
   (\<exists>ST LT rT maxs maxl ins.
-    phi C sig ! pc = Some (ST,LT) \<and> 
+    phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> 
     method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
-	(\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and>
+	(\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and> 
          (mn,pTs) = sig0 \<and> 
          (\<exists>apTs D ST' LT'.
          (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
@@ -64,6 +64,7 @@
 			(let (stk,loc,C,sig,pc) = f
 		         in
                          \<exists>rT maxs maxl ins s.
+                         is_class G C \<and>
                          method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
                          phi C sig ! pc = Some s \<and>
 			 correct_frame G hp s maxl ins f \<and>