diff -r 833ffcb2e92d -r 2aa33ed5f526 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Fri Jun 14 13:24:32 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Fri Jun 14 23:25:36 2002 +0200
@@ -16,29 +16,70 @@
 *}
 
 constdefs
+  -- "The program counter will always be inside the method:"
+  check_bounded :: "instr list \<Rightarrow> exception_table \<Rightarrow> bool"
+  "check_bounded ins et \<equiv> 
+  (\<forall>pc < length ins. \<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins) \<and>
+                     (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
+
+  -- "The method type only contains declared classes:"
+  check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
+  "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
+
+  -- "An instruction is welltyped if it is applicable and its effect"
+  -- "is compatible with the type at all successor instructions:"
   wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
                 exception_table,p_count] \<Rightarrow> bool"
-  "wt_instr i G rT phi mxs max_pc et pc == 
+  "wt_instr i G rT phi mxs max_pc et pc \<equiv>
   app i G mxs rT pc et (phi!pc) \<and>
   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
 
+  -- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
   wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
   "wt_start G C pTs mxl phi == 
   G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
 
+  -- "A method is welltyped if the body is not empty, if execution does not"
+  -- "leave the body, if the method type covers all instructions and mentions"
+  -- "declared classes only, if the method calling convention is respected, and"
+  -- "if all instructions are welltyped."
   wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
                  exception_table,method_type] \<Rightarrow> bool"
-  "wt_method G C pTs rT mxs mxl ins et phi ==
+  "wt_method G C pTs rT mxs mxl ins et phi \<equiv>
   let max_pc = length ins in
-  0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
-  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
+  0 < max_pc \<and> 
+  length phi = length ins \<and>
+  check_bounded ins et \<and> 
+  check_types G mxs (1+length pTs+mxl) (map OK phi) \<and>
+  wt_start G C pTs mxl phi \<and>
+  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G rT phi mxs max_pc et pc)"
 
+  -- "A program is welltyped if it is wellformed and all methods are welltyped"
   wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
   "wt_jvm_prog G phi ==
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
            wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
 
 
+lemma check_boundedD:
+  "\<lbrakk> check_bounded ins et; pc < length ins; 
+    (pc',s') \<in> set (eff (ins!pc) G pc et s)  \<rbrakk> \<Longrightarrow> 
+  pc' < length ins"
+  apply (unfold eff_def)
+  apply simp
+  apply (unfold check_bounded_def)
+  apply clarify
+  apply (erule disjE)
+   apply blast
+  apply (erule allE, erule impE, assumption)
+  apply (unfold xcpt_eff_def)
+  apply clarsimp    
+  apply (drule xcpt_names_in_et)
+  apply clarify
+  apply (drule bspec, assumption)
+  apply simp
+  done
+
 lemma wt_jvm_progD:
   "wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
   by (unfold wt_jvm_prog_def, blast)
@@ -46,10 +87,28 @@
 lemma wt_jvm_prog_impl_wt_instr:
   "\<lbrakk> wt_jvm_prog G phi; is_class G C;
       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk> 
-  \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
+  \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
   by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
       simp, simp, simp add: wf_mdecl_def wt_method_def)
 
+text {*
+  We could leave out the check @{term "pc' < max_pc"} in the 
+  definition of @{term wt_instr} in the context of @{term wt_method}.
+*}
+lemma wt_instr_def2:
+  "\<lbrakk> wt_jvm_prog G Phi; is_class G C;
+      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins; 
+      i = ins!pc; phi = Phi C sig; max_pc = length ins \<rbrakk> 
+  \<Longrightarrow> wt_instr i G rT phi maxs max_pc et pc =
+     (app i G maxs rT pc et (phi!pc) \<and>
+     (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). G \<turnstile> s' <=' phi!pc'))"
+apply (simp add: wt_instr_def)
+apply (unfold wt_jvm_prog_def)
+apply (drule method_wf_mdecl)
+apply (simp, simp, simp add: wf_mdecl_def wt_method_def)
+apply (auto dest: check_boundedD)
+done
+
 lemma wt_jvm_prog_impl_wt_start:
   "\<lbrakk> wt_jvm_prog G phi; is_class G C;
       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow>