diff -r 3fb416265ba9 -r d09d0f160888 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sun Dec 16 00:17:18 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Dec 16 00:17:44 2001 +0100
@@ -1,34 +1,36 @@
-(*  Title:      HOL/BCV/JVM.thy
+(*  Title:      HOL/MicroJava/BV/JVM.thy
     ID:         $Id$
-    Author:     Tobias Nipkow
+    Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
-
 *)
 
 header "Kildall for the JVM"
 
-theory JVM = Kildall + JVMType + Opt + Product + Typing_Framework_err +
-             StepMono + BVSpec:
+theory JVM = Kildall_Lift + JVMType + Opt + Product + Typing_Framework_err +
+             EffectMono + BVSpec:
 
 constdefs
-  exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> state"
-  "exec G maxs rT bs == err_step (\<lambda>pc. app (bs!pc) G maxs rT) (\<lambda>pc. step (bs!pc) G)"
+  exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
+  "exec G maxs rT et bs == 
+  err_step (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
 
-  kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list"
-  "kiljvm G maxs maxr rT bs ==
-  kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
+  kiljvm :: "jvm_prog => nat => nat => ty => exception_table => 
+             instr list => state list => state list"
+  "kiljvm G maxs maxr rT et bs ==
+  kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
 
-  wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
-  "wt_kil G C pTs rT mxs mxl ins ==
-   bounded (\<lambda>n. succs (ins!n) n) (size ins) \<and> 0 < size ins \<and> 
+  wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
+             exception_table \<Rightarrow> instr list \<Rightarrow> bool"
+  "wt_kil G C pTs rT mxs mxl et ins ==
+   bounded (exec G mxs rT et ins) (size ins) \<and> 0 < size ins \<and> 
    (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
         start  = OK first#(replicate (size ins - 1) (OK None));
-        result = kiljvm G mxs (1+size pTs+mxl) rT ins start
+        result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
     in \<forall>n < size ins. result!n \<noteq> Err)"
 
   wt_jvm_prog_kildall :: "jvm_prog => bool"
   "wt_jvm_prog_kildall G ==
-  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)). wt_kil G C (snd sig) rT maxs maxl b) G"
+  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
 
 
 lemma special_ex_swap_lemma [iff]: 
@@ -37,66 +39,225 @@
 
 lemmas [iff del] = not_None_eq
 
+lemma non_empty_succs: "succs i pc \<noteq> []"
+  by (cases i) auto
+
+lemma non_empty:
+  "non_empty (\<lambda>pc. eff (bs!pc) G pc et)" 
+  by (simp add: non_empty_def eff_def non_empty_succs)
+
+lemma listn_Cons_Suc [elim!]:
+  "l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
+  by (cases n) auto
+
+lemma listn_appendE [elim!]:
+  "a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P" 
+proof -
+  have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
+    (is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
+  proof (induct a)
+    fix n assume "?list [] n"
+    hence "?P [] n 0 n" by simp
+    thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
+  next
+    fix n l ls
+    assume "?list (l#ls) n"
+    then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
+    assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
+    hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
+    then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
+    with n have "?P (l#ls) n (n1+1) n2" by simp
+    thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
+  qed
+  moreover
+  assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
+  ultimately
+  show ?thesis by blast
+qed
+
+
 theorem exec_pres_type:
-  "[| wf_prog wf_mb S |] ==> 
-      pres_type (exec S maxs rT bs) (size bs) (states S maxs maxr)"
- apply (unfold pres_type_def list_def step_def JVM_states_unfold)
- apply (clarify elim!: option_map_in_optionI lift_in_errI)
- apply (simp add: exec_def err_step_def lift_def split: err.split)
- apply (simp add: step_def option_map_def split: option.splits)  
- apply clarify
- apply (case_tac "bs!p")
+  "wf_prog wf_mb S ==> 
+  pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
+  apply (unfold exec_def JVM_states_unfold)
+  apply (rule pres_type_lift)
+  apply clarify
+  apply (case_tac s)
+   apply simp
+   apply (drule effNone)
+   apply simp  
+  apply (simp add: eff_def xcpt_eff_def norm_eff_def)
+  apply (case_tac "bs!p")
+
+  apply (clarsimp simp add: not_Err_eq)
+  apply (drule listE_nth_in, assumption)
+  apply fastsimp
+
+  apply (fastsimp simp add: not_None_eq)
+
+  apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
+
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x="1" in exI)
+  apply fastsimp
 
- apply (fastsimp simp add: not_Err_eq dest: subsetD nth_mem)
- apply fastsimp
- apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
- apply fastsimp
- apply (fastsimp dest: field_fields fields_is_type)
- apply fastsimp
- apply fastsimp
- defer
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
+  apply clarsimp
+  apply (erule disjE)
+   apply (fastsimp dest: field_fields fields_is_type)
+  apply simp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply simp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+
+  defer 
+
+  apply fastsimp
+  apply fastsimp
+
+  apply clarsimp
+  apply (rule_tac x="n'+2" in exI)  
+  apply simp
+  apply (drule listE_length)+
+  apply fastsimp
 
- (* Invoke *)
- apply (clarsimp simp add: Un_subset_iff)
- apply (drule method_wf_mdecl, assumption+)
- apply (simp add: wf_mdecl_def wf_mhead_def)
- done
+  apply clarsimp
+  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)  
+  apply simp
+  apply (drule listE_length)+
+  apply fastsimp
+
+  apply clarsimp
+  apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)  
+  apply simp
+  apply (drule listE_length)+
+  apply fastsimp
+
+  apply fastsimp
+  apply fastsimp
+  apply fastsimp
+  apply fastsimp
 
+  apply clarsimp
+  apply (erule disjE)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+  
+  apply (erule disjE)
+   apply (clarsimp simp add: Un_subset_iff)  
+   apply (drule method_wf_mdecl, assumption+)
+   apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
+   apply fastsimp
+  apply clarsimp
+  apply (rule_tac x=1 in exI)
+  apply fastsimp
+  done
 
 lemmas [iff] = not_None_eq
 
+lemma map_fst_eq:
+  "map fst (map (\<lambda>z. (f z, x z)) a) = map fst (map (\<lambda>z. (f z, y z)) a)"
+  by (induct a) auto
+
+lemma succs_stable_eff:
+  "succs_stable (sup_state_opt G) (\<lambda>pc. eff (bs!pc) G pc et)"
+  apply (unfold succs_stable_def eff_def xcpt_eff_def)
+  apply (simp add: map_fst_eq)
+  done
+
+lemma sup_state_opt_unfold:
+  "sup_state_opt G \<equiv> Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))))"
+  by (simp add: sup_state_opt_def sup_state_def sup_loc_def sup_ty_opt_def)
+
+constdefs
+  opt_states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (ty list \<times> ty err list) option set"
+  "opt_states G maxs maxr \<equiv> opt (\<Union>{list n (types G) |n. n \<le> maxs} \<times> list maxr (err (types G)))"
+
+lemma app_mono:
+  "app_mono (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (length bs) (opt_states G maxs maxr)"
+  by (unfold app_mono_def lesub_def) (blast intro: EffectMono.app_mono)
+
+lemma le_list_appendI:
+  "\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
+apply (induct a)
+ apply simp
+apply (case_tac b)
+apply auto
+done
+
+lemma le_listI:
+  "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
+  apply (unfold lesub_def Listn.le_def)
+  apply (simp add: list_all2_conv_all_nth)
+  done
+  
+lemma eff_mono:
+  "\<lbrakk>p < length bs; s <=_(sup_state_opt G) t; app (bs!p) G maxs rT pc et t\<rbrakk>
+  \<Longrightarrow> eff (bs!p) G p et s <=|sup_state_opt G| eff (bs!p) G p et t"
+  apply (unfold eff_def)
+  apply (rule le_list_appendI)
+   apply (simp add: norm_eff_def)
+   apply (rule le_listI)
+    apply simp
+   apply simp
+   apply (simp add: lesub_def)
+   apply (case_tac s)
+    apply simp
+   apply (simp del: split_paired_All split_paired_Ex)
+   apply (elim exE conjE)
+   apply simp
+   apply (drule eff'_mono, assumption)
+   apply assumption
+  apply (simp add: xcpt_eff_def)
+  apply (rule le_listI)
+    apply simp
+  apply simp
+  apply (simp add: lesub_def)
+  apply (case_tac s)
+   apply simp
+  apply simp
+  apply (case_tac t)
+   apply simp
+  apply (clarsimp simp add: sup_state_conv)
+  done
+
+lemma order_sup_state_opt:
+  "wf_prog wf_mb G \<Longrightarrow> order (sup_state_opt G)"
+  by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
 
 theorem exec_mono:
   "wf_prog wf_mb G ==>
-  mono (JVMType.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)"
-  apply (unfold mono_def)
+  mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
+  apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
+  apply (rule mono_lift)
+     apply (fold sup_state_opt_unfold opt_states_def)
+     apply (erule order_sup_state_opt)
+    apply (rule succs_stable_eff)
+   apply (rule app_mono)
   apply clarify
-  apply (unfold lesub_def)
-  apply (case_tac t)
-   apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def)
-  apply (case_tac s)
-   apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def)
-  apply (simp add: JVM_le_convert exec_def err_step_def lift_def)
-  apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def)
-  apply (rule conjI)
-   apply clarify
-   apply (rule step_mono, assumption+)
-  apply (rule impI)
-  apply (erule contrapos_nn)
-  apply (rule app_mono, assumption+)
+  apply (rule eff_mono)
+  apply assumption+
   done
 
 theorem semilat_JVM_slI:
-  "[| wf_prog wf_mb G |] ==> semilat (JVMType.sl G maxs maxr)"
+  "wf_prog wf_mb G ==> semilat (JVMType.sl G maxs maxr)"
   apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
   apply (rule semilat_opt)
   apply (rule err_semilat_Product_esl)
@@ -114,9 +275,9 @@
 
 
 theorem is_bcv_kiljvm:
-  "[| wf_prog wf_mb G; bounded (\<lambda>pc. succs (bs!pc) pc) (size bs) |] ==> 
-      is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
-             (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)"
+  "[| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) |] ==> 
+      is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
+             (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
   apply (unfold kiljvm_def sl_triple_conv)
   apply (rule is_bcv_kildall)
        apply (simp (no_asm) add: sl_triple_conv [symmetric]) 
@@ -132,9 +293,9 @@
 
 
 theorem wt_kil_correct:
-  "[| wt_kil G C pTs rT maxs mxl bs; wf_prog wf_mb G; 
+  "[| wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G; 
       is_class G C; \<forall>x \<in> set pTs. is_type G x |]
-  ==> \<exists>phi. wt_method G C pTs rT maxs mxl bs phi"
+  ==> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
 proof -
   let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                 #(replicate (size bs - 1) (OK None))"
@@ -143,41 +304,25 @@
   assume isclass: "is_class G C"
   assume istype:  "\<forall>x \<in> set pTs. is_type G x"
 
-  assume "wt_kil G C pTs rT maxs mxl bs"
+  assume "wt_kil G C pTs rT maxs mxl et bs"
   then obtain maxr r where    
-    bounded: "bounded (\<lambda>pc. succs (bs!pc) pc) (size bs)" and
-    result:  "r = kiljvm G maxs maxr rT bs ?start" and
+    bounded: "bounded (exec G maxs rT et bs) (size bs)" and
+    result:  "r = kiljvm G maxs maxr rT et bs ?start" and
     success: "\<forall>n < size bs. r!n \<noteq> Err" and
     instrs:  "0 < size bs" and
     maxr:    "maxr = Suc (length pTs + mxl)" 
     by (unfold wt_kil_def) simp
 
-  { fix pc
-    have "succs (bs!pc) pc \<noteq> []"
-      by (cases "bs!pc") auto
-  }
-
-  hence non_empty: "non_empty (\<lambda>pc. succs (bs!pc) pc)"
-    by (unfold non_empty_def) blast
-
   from wf bounded
   have bcv:
-    "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)
-            (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)"
+    "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) 
+            (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
     by (rule is_bcv_kiljvm)
 
-  { fix l x
-    have "set (replicate l x) \<subseteq> {x}"
-      by (cases "0 < l") simp+
+  { fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
   } note subset_replicate = this
-
-  from istype
-  have "set pTs \<subseteq> types G"
-    by auto
-
-  hence "OK ` set pTs \<subseteq> err (types G)"
-    by auto
-
+  from istype have "set pTs \<subseteq> types G" by auto
+  hence "OK ` set pTs \<subseteq> err (types G)" by auto
   with instrs maxr isclass 
   have "?start \<in> list (length bs) (states G maxs maxr)"
     apply (unfold list_def JVM_states_unfold)
@@ -191,51 +336,37 @@
      apply (simp add: subset_replicate)
     apply simp
     done
-
-  with bcv success result 
-  have 
+  with bcv success result have 
     "\<exists>ts\<in>list (length bs) (states G maxs maxr).
          ?start <=[JVMType.le G maxs maxr] ts \<and>
-         wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts"
+         wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts"
     by (unfold is_bcv_def) auto
-
   then obtain phi' where
     l: "phi' \<in> list (length bs) (states G maxs maxr)" and
     s: "?start <=[JVMType.le G maxs maxr] phi'" and
-    w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+    w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'"
     by blast
-   
   hence dynamic:
-    "dynamic_wt (sup_state_opt G) (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+    "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) phi'"
     by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv)
 
-  from s
-  have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"    
+  from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)"
     by (drule_tac p=0 in le_listD) (simp add: lesub_def)+
 
-  from l
-  have l: "size phi' = size bs"
-    by simp
-  
-  with instrs w
-  have "phi' ! 0 \<noteq> Err"
-    by (unfold wt_step_def) simp
-
-  with instrs l
-  have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
+  from l have l: "size phi' = size bs" by simp  
+  with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
+  with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
     by (clarsimp simp add: not_Err_eq)
 
-  from l bounded
-  have "bounded (\<lambda>pc. succs (bs ! pc) pc) (length phi')"
-    by simp
-
-  with dynamic non_empty
-  have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT) (\<lambda>pc. step (bs!pc) G) 
-                                    (\<lambda>pc. succs (bs!pc) pc) (map ok_val phi')"
-    by (auto intro: dynamic_imp_static simp add: exec_def)
-
-  with instrs l le bounded
-  have "wt_method G C pTs rT maxs mxl bs (map ok_val phi')"
+  from l bounded 
+  have bounded': "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
+    by (simp add: exec_def bounded_lift)  
+  with dynamic
+  have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) 
+                  (\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')"
+    by (auto intro: dynamic_imp_static simp add: exec_def non_empty)
+  with instrs l le bounded'
+  have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
     apply (unfold wt_method_def static_wt_def)
     apply simp
     apply (rule conjI)
@@ -254,74 +385,77 @@
 qed
 
 
-(* there's still one easy, and one nontrivial (but provable) sorry in here  *)
-(*
 theorem wt_kil_complete:
-  "[| wt_method G C pTs rT maxs mxl bs phi; wf_prog wf_mb G; 
-      length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x |]
-  ==> wt_kil G C pTs rT maxs mxl bs"
+  "[| wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
+      length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
+      map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) |]
+  ==> wt_kil G C pTs rT maxs mxl et bs"
 proof -
-  assume wf:      "wf_prog wf_mb G"  
+  assume wf: "wf_prog wf_mb G"  
   assume isclass: "is_class G C"
-  assume istype:  "\<forall>x \<in> set pTs. is_type G x"
-  assume length:  "length phi = length bs"
+  assume istype: "\<forall>x \<in> set pTs. is_type G x"
+  assume length: "length phi = length bs"
+  assume istype_phi: "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
 
-  assume "wt_method G C pTs rT maxs mxl bs phi"
+  assume "wt_method G C pTs rT maxs mxl bs et phi"
   then obtain
     instrs:   "0 < length bs" and
     wt_start: "wt_start G C pTs mxl phi" and
     wt_ins:   "\<forall>pc. pc < length bs \<longrightarrow> 
-                    wt_instr (bs ! pc) G rT phi maxs (length bs) pc"
+                    wt_instr (bs ! pc) G rT phi maxs (length bs) et pc"
     by (unfold wt_method_def) simp
 
-  let ?succs = "\<lambda>pc. succs (bs!pc) pc"
-  let ?step  = "\<lambda>pc. step (bs!pc) G"
-  let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT"
+  let ?eff  = "\<lambda>pc. eff (bs!pc) G pc et"
+  let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
 
+  have bounded_eff: "bounded ?eff (size bs)"
+  proof (unfold bounded_def, clarify)
+    fix pc pc' s s' assume "pc < length bs"
+    with wt_ins have "wt_instr (bs!pc) G rT phi maxs (length bs) et pc" by fast
+    then obtain "\<forall>(pc',s') \<in> set (?eff pc (phi!pc)). pc' < length bs"
+      by (unfold wt_instr_def) fast
+    hence "\<forall>pc' \<in> set (map fst (?eff pc (phi!pc))). pc' < length bs" by auto
+    also 
+    note succs_stable_eff 
+    hence "map fst (?eff pc (phi!pc)) = map fst (?eff pc s)" 
+      by (rule succs_stableD)
+    finally have "\<forall>(pc',s') \<in> set (?eff pc s). pc' < length bs" by auto
+    moreover assume "(pc',s') \<in> set (?eff pc s)"
+    ultimately show "pc' < length bs" by blast
+  qed
+  hence bounded_exec: "bounded (exec G maxs rT et bs) (size bs)" 
+    by (simp add: exec_def bounded_lift)
+ 
   from wt_ins
-  have bounded: "bounded ?succs (size bs)"
-    by (unfold wt_instr_def bounded_def) blast
-
-  from wt_ins
-  have "static_wt (sup_state_opt G) ?app ?step ?succs phi"
+  have "static_wt (sup_state_opt G) ?app ?eff phi"
     apply (unfold static_wt_def wt_instr_def lesub_def)
     apply (simp (no_asm) only: length)
     apply blast
     done
 
-  with bounded
-  have "dynamic_wt (sup_state_opt G) (err_step ?app ?step) ?succs (map OK phi)"
+  with bounded_eff
+  have "dynamic_wt (sup_state_opt G) (err_step ?app ?eff) (map OK phi)"
     by - (erule static_imp_dynamic, simp add: length)
-
   hence dynamic:
-    "dynamic_wt (sup_state_opt G) (exec G maxs rT bs) ?succs (map OK phi)"
+    "dynamic_wt (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
     by (unfold exec_def)
  
   let ?maxr = "1+size pTs+mxl"
-
-  from wf bounded
+  from wf bounded_exec
   have is_bcv: 
-    "is_bcv (JVMType.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs 
-            (size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT bs)"
+    "is_bcv (JVMType.le G maxs ?maxr) Err (exec G maxs rT et bs) 
+            (size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT et bs)"
     by (rule is_bcv_kiljvm)
 
   let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                 #(replicate (size bs - 1) (OK None))"
 
-  { fix l x
-    have "set (replicate l x) \<subseteq> {x}"
-      by (cases "0 < l") simp+
+  { fix l x have "set (replicate l x) \<subseteq> {x}" by (cases "0 < l") simp+
   } note subset_replicate = this
 
-  from istype
-  have "set pTs \<subseteq> types G"
-    by auto
-
-  hence "OK ` set pTs \<subseteq> err (types G)"
-    by auto
-
-  with instrs isclass 
-  have start:
+  from istype have "set pTs \<subseteq> types G" by auto
+  hence "OK ` set pTs \<subseteq> err (types G)" by auto
+  with instrs isclass have start:
     "?start \<in> list (length bs) (states G maxs ?maxr)"
     apply (unfold list_def JVM_states_unfold)
     apply simp
@@ -335,12 +469,12 @@
     apply simp
     done
 
-  let ?phi = "map OK phi"
-
-  have 1: "?phi \<in> list (length bs) (states G maxs ?maxr)" sorry
-
-  have 2: "?start <=[le G maxs ?maxr] ?phi"
+  let ?phi = "map OK phi"  
+  have less_phi: "?start <=[JVMType.le G maxs ?maxr] ?phi"
   proof -
+    from length instrs
+    have "length ?start = length (map OK phi)" by simp
+    moreover
     { fix n
       from wt_start
       have "G \<turnstile> ok_val (?start!0) <=' phi!0"
@@ -349,38 +483,62 @@
       from instrs length
       have "0 < length phi" by simp
       ultimately
-      have "le G maxs ?maxr (?start!0) (?phi!0)"
+      have "JVMType.le G maxs ?maxr (?start!0) (?phi!0)"
         by (simp add: JVM_le_Err_conv Err.le_def lesub_def)
       moreover
       { fix n'
-        have "le G maxs ?maxr (OK None) (?phi!n)"
+        have "JVMType.le G maxs ?maxr (OK None) (?phi!n)"
           by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
             split: err.splits)        
         hence "[| n = Suc n'; n < length ?start |] 
-          ==> le G maxs ?maxr (?start!n) (?phi!n)"
+          ==> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
           by simp
       }
       ultimately
-      have "n < length ?start ==> le G maxs ?maxr (?start!n) (?phi!n)"
-        by - (cases n, blast+)
-    }
-    thus ?thesis sorry
+      have "n < length ?start ==> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
+        by (unfold lesub_def) (cases n, blast+)
+    } 
+    ultimately show ?thesis by (rule le_listI)
   qed         
 
   from dynamic
-  have "wt_step (le G maxs ?maxr) Err (exec G maxs rT bs) ?succs ?phi"
-    by (simp add: dynamic_wt_def JVM_le_Err_conv)
-  
-  with start 1 2 is_bcv
-  have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT bs ?start ! p \<noteq> Err"
-    by (unfold is_bcv_def) blast
+  have "wt_step (JVMType.le G maxs ?maxr) Err (exec G maxs rT et bs) ?phi"
+    by (simp add: dynamic_wt_def JVM_le_Err_conv)  
+  with start istype_phi less_phi is_bcv
+  have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT et bs ?start ! p \<noteq> Err"
+    by (unfold is_bcv_def) auto
+  with bounded_exec instrs
+  show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp
+qed
+text {*
+  The above theorem @{text wt_kil_complete} is all nice'n shiny except
+  for one assumption: @{term "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"}  
+  It does not hold for all @{text phi} that satisfy @{text wt_method}.
 
-  with bounded instrs
-  show "wt_kil G C pTs rT maxs mxl bs"
-    by (unfold wt_kil_def) simp
-qed
-*)
+  The assumption states mainly that all entries in @{text phi} are legal
+  types in the program context, that the stack size is bounded by @{text maxs},
+  and that the register sizes are exactly @{term "1+size pTs+mxl"}. 
+  The BV specification, i.e.~@{text wt_method}, only gives us this
+  property for \emph{reachable} code. For unreachable code, 
+  e.g.~unused registers may contain arbitrary garbage. Even the stack
+  and register sizes can be different from the rest of the program (as 
+  long as they are consistent inside each chunk of unreachable code).
+  
+  All is not lost, though: for each @{text phi} that satisfies 
+  @{text wt_method} there is a @{text phi'} that also satisfies 
+  @{text wt_method} and that additionally satisfies our assumption.
+  The construction is quite easy: the entries for reachable code
+  are the same in @{text phi} and @{text phi'}, the entries for
+  unreachable code are all @{text None} in @{text phi'} (as it would
+  be produced by Kildall's algorithm). 
 
+  Although this is proved easily by comment, it requires some more
+  overhead (i.e.~talking about reachable instructions) if you try
+  it the hard way. Thus it is missing here for the time being.
+
+  The other direction (@{text wt_kil_correct}) can be lifted to
+  programs without problems:
+*}
 lemma is_type_pTs:
   "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
       t \<in> set (snd sig) |]
@@ -409,8 +567,8 @@
     wf: "wf_prog wf_mb G"
     by (auto simp add: wt_jvm_prog_kildall_def)
 
-  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins)) = the (method (G,C) sig) in 
-              SOME phi. wt_method G C (snd sig) rT maxs maxl ins phi"
+  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
+              SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi"
    
   { fix C S fs mdecls sig rT code
     assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"