# HG changeset patch
# User kleing
# Date 1014913308 -3600
# Node ID 7acfab8361d1d7d32a04a7f208ee679ae93ee4c5
# Parent  8040cce614e5bca947f28cd10c2d50fe16900cf5
enforce positive branch targets

diff -r 8040cce614e5 -r 7acfab8361d1 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Thu Feb 28 15:12:09 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Thu Feb 28 17:21:48 2002 +0100
@@ -127,54 +127,61 @@
 
 text "Conditions under which eff is applicable:"
 consts
-app' :: "instr \<times> jvm_prog \<times> nat \<times> ty \<times> state_type => bool"
+app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type => bool"
 
 recdef app' "{}"
-"app' (Load idx, G, maxs, rT, s)                  = (idx < length (snd s) \<and> 
-                                                    (snd s) ! idx \<noteq> Err \<and> 
-                                                    length (fst s) < maxs)"
-"app' (Store idx, G, maxs, rT, (ts#ST, LT))       = (idx < length LT)"
-"app' (LitPush v, G, maxs, rT, s)                  = (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"
-"app' (Getfield F C, G, maxs, rT, (oT#ST, LT))    = (is_class G C \<and>
-                                              field (G,C) F \<noteq> None \<and>
-                                              fst (the (field (G,C) F)) = C \<and>
-                                              G \<turnstile> oT \<preceq> (Class C))"
-"app' (Putfield F C, G, maxs, rT, (vT#oT#ST, LT)) = (is_class G C \<and> 
-                                              field (G,C) F \<noteq> None \<and>
-                                              fst (the (field (G,C) F)) = C \<and>
-                                              G \<turnstile> oT \<preceq> (Class C) \<and>
-                                              G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
-"app' (New C, G, maxs, rT, s)                     = (is_class G C \<and> length (fst s) < maxs)"
-"app' (Checkcast C, G, maxs, rT, (RefT rt#ST,LT)) = (is_class G C)"
-"app' (Pop, G, maxs, rT, (ts#ST,LT))              = True"
-"app' (Dup, G, maxs, rT, (ts#ST,LT))              = (1+length ST < maxs)"
-"app' (Dup_x1, G, maxs, rT, (ts1#ts2#ST,LT))      = (2+length ST < maxs)"
-"app' (Dup_x2, G, maxs, rT, (ts1#ts2#ts3#ST,LT))  = (3+length ST < maxs)"
-"app' (Swap, G, maxs, rT, (ts1#ts2#ST,LT))        = True"
-"app' (IAdd, G, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) 
-                                                 = True"
-"app' (Ifcmpeq b, G, maxs, rT, (ts#ts'#ST,LT))    = (isPrimT ts \<and> ts' = ts \<or> 
-                                                     isRefT ts \<and> isRefT ts')"
-"app' (Goto b, G, maxs, rT, s)                    = True"
-"app' (Return, G, maxs, rT, (T#ST,LT))            = (G \<turnstile> T \<preceq> rT)"
-"app' (Throw, G, maxs, rT, (T#ST,LT))             = isRefT T"
-
-"app' (Invoke C mn fpTs, G, maxs, rT, s)          = 
-   (length fpTs < length (fst s) \<and> 
-   (let apTs = rev (take (length fpTs) (fst s));
-        X    = hd (drop (length fpTs) (fst s)) 
-    in  
-        G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
-        list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))"
+"app' (Load idx, G, pc, maxs, rT, s) = 
+  (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)"
+"app' (Store idx, G, pc, maxs, rT, (ts#ST, LT)) = 
+  (idx < length LT)"
+"app' (LitPush v, G, pc, maxs, rT, s) = 
+  (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"
+"app' (Getfield F C, G, pc, maxs, rT, (oT#ST, LT)) = 
+  (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and> 
+  G \<turnstile> oT \<preceq> (Class C))"
+"app' (Putfield F C, G, pc, maxs, rT, (vT#oT#ST, LT)) = 
+  (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
+  G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
+"app' (New C, G, pc, maxs, rT, s) = 
+  (is_class G C \<and> length (fst s) < maxs)"
+"app' (Checkcast C, G, pc, maxs, rT, (RefT rt#ST,LT)) = 
+  (is_class G C)"
+"app' (Pop, G, pc, maxs, rT, (ts#ST,LT)) = 
+  True"
+"app' (Dup, G, pc, maxs, rT, (ts#ST,LT)) = 
+  (1+length ST < maxs)"
+"app' (Dup_x1, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = 
+  (2+length ST < maxs)"
+"app' (Dup_x2, G, pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) = 
+  (3+length ST < maxs)"
+"app' (Swap, G, pc, maxs, rT, (ts1#ts2#ST,LT)) = 
+  True"
+"app' (IAdd, G, pc, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) =
+  True"
+"app' (Ifcmpeq b, G, pc, maxs, rT, (ts#ts'#ST,LT)) = 
+  (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))"
+"app' (Goto b, G, pc, maxs, rT, s) = 
+  (0 \<le> int pc + b)"
+"app' (Return, G, pc, maxs, rT, (T#ST,LT)) = 
+  (G \<turnstile> T \<preceq> rT)"
+"app' (Throw, G, pc, maxs, rT, (T#ST,LT)) = 
+  isRefT T"
+"app' (Invoke C mn fpTs, G, pc, maxs, rT, s) = 
+  (length fpTs < length (fst s) \<and> 
+  (let apTs = rev (take (length fpTs) (fst s));
+       X    = hd (drop (length fpTs) (fst s)) 
+   in  
+       G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
+       list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))"
   
-"app' (i,G,maxs,rT,s)                             = False"
+"app' (i,G, pc,maxs,rT,s) = False"
 
 constdefs
   xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"
   "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"
 
   app :: "instr => jvm_prog => nat => ty => nat => exception_table => state_type option => bool"
-  "app i G maxs rT pc et s == case s of None => True | Some t => app' (i,G,maxs,rT,t) \<and> xcpt_app i G pc et"
+  "app i G maxs rT pc et s == case s of None => True | Some t => app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"
 
 
 lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
@@ -303,8 +310,9 @@
 
 
 lemma appIfcmpeq[simp]:
-"app (Ifcmpeq b) G maxs rT pc et (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 
- ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" 
+"app (Ifcmpeq b) G maxs rT pc et (Some s) = 
+  (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 0 \<le> int pc + b \<and>
+  ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" 
   by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
 
 lemma appReturn[simp]:
@@ -312,7 +320,7 @@
   by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
 
 lemma appGoto[simp]:
-"app (Goto branch) G maxs rT pc et (Some s) = True"
+"app (Goto b) G maxs rT pc et (Some s) = (0 \<le> int pc + b)"
   by simp
 
 lemma appThrow[simp]: