# HG changeset patch
# User kleing
# Date 1024089936 -7200
# Node ID 2aa33ed5f52606c5791bd1dee9838c15cd198e00
# Parent  833ffcb2e92d01229558e54a83165177791a0a13
wt_method now checks bounded+types ==> wt_kildall <=> wt_method

diff -r 833ffcb2e92d -r 2aa33ed5f526 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Jun 14 13:24:32 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Jun 14 23:25:36 2002 +0200
@@ -252,11 +252,27 @@
    (                                    [], [Class list_name, Class list_name]),
    (                          [PrimT Void], [Class list_name, Class list_name])]"
 
+
+lemma bounded_append [simp]:
+  "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"
+  apply (simp add: check_bounded_def)
+  apply (simp add: nat_number append_ins_def)
+  apply (rule allI, rule impI)
+  apply (elim pc_end pc_next pc_0)
+  apply auto
+  done
+
+lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)"
+  apply (auto simp add: check_types_def phi_append_def JVM_states_unfold)
+  apply (unfold list_def)
+  apply auto
+  done
+  
 lemma wt_append [simp]:
   "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
              [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
-  apply (simp add: wt_method_def append_ins_def phi_append_def 
-                   wt_start_def wt_instr_def)
+  apply (simp add: wt_method_def wt_start_def wt_instr_def)
+  apply (simp add: phi_append_def append_ins_def)
   apply clarify
   apply (elim pc_end pc_next pc_0)
   apply simp
@@ -277,42 +293,57 @@
 
 text {* Some abbreviations for readability *} 
 syntax
-  list :: ty 
-  test :: ty
+  Clist :: ty 
+  Ctest :: ty
 translations
-  "list" == "Class list_name"
-  "test" == "Class test_name"
+  "Clist" == "Class list_name"
+  "Ctest" == "Class test_name"
 
 constdefs
   phi_makelist :: method_type ("\<phi>\<^sub>m")
   "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
-    (                                   [], [OK test, Err    , Err    ]),
-    (                               [list], [OK test, Err    , Err    ]),
-    (                         [list, list], [OK test, Err    , Err    ]),
-    (                               [list], [OK list, Err    , Err    ]),
-    (                [PrimT Integer, list], [OK list, Err    , Err    ]),
-    (                                   [], [OK list, Err    , Err    ]),
-    (                               [list], [OK list, Err    , Err    ]),
-    (                         [list, list], [OK list, Err    , Err    ]),
-    (                               [list], [OK list, OK list, Err    ]),
-    (                [PrimT Integer, list], [OK list, OK list, Err    ]),
-    (                                   [], [OK list, OK list, Err    ]),
-    (                               [list], [OK list, OK list, Err    ]),
-    (                         [list, list], [OK list, OK list, Err    ]),
-    (                               [list], [OK list, OK list, OK list]),
-    (                [PrimT Integer, list], [OK list, OK list, OK list]),
-    (                                   [], [OK list, OK list, OK list]),
-    (                               [list], [OK list, OK list, OK list]),
-    (                         [list, list], [OK list, OK list, OK list]),
-    (                         [PrimT Void], [OK list, OK list, OK list]),
-    (                                   [], [OK list, OK list, OK list]),
-    (                               [list], [OK list, OK list, OK list]),
-    (                         [list, list], [OK list, OK list, OK list]),
-    (                         [PrimT Void], [OK list, OK list, OK list])]"
+    (                                   [], [OK Ctest, Err     , Err     ]),
+    (                              [Clist], [OK Ctest, Err     , Err     ]),
+    (                       [Clist, Clist], [OK Ctest, Err     , Err     ]),
+    (                              [Clist], [OK Clist, Err     , Err     ]),
+    (               [PrimT Integer, Clist], [OK Clist, Err     , Err     ]),
+    (                                   [], [OK Clist, Err     , Err     ]),
+    (                              [Clist], [OK Clist, Err     , Err     ]),
+    (                       [Clist, Clist], [OK Clist, Err     , Err     ]),
+    (                              [Clist], [OK Clist, OK Clist, Err     ]),
+    (               [PrimT Integer, Clist], [OK Clist, OK Clist, Err     ]),
+    (                                   [], [OK Clist, OK Clist, Err     ]),
+    (                              [Clist], [OK Clist, OK Clist, Err     ]),
+    (                       [Clist, Clist], [OK Clist, OK Clist, Err     ]),
+    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
+    (               [PrimT Integer, Clist], [OK Clist, OK Clist, OK Clist]),
+    (                                   [], [OK Clist, OK Clist, OK Clist]),
+    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
+    (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
+    (                         [PrimT Void], [OK Clist, OK Clist, OK Clist]),
+    (                                   [], [OK Clist, OK Clist, OK Clist]),
+    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
+    (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
+    (                         [PrimT Void], [OK Clist, OK Clist, OK Clist])]"
+
+lemma bounded_makelist [simp]: "check_bounded make_list_ins []"
+  apply (simp add: check_bounded_def)
+  apply (simp add: nat_number make_list_ins_def)
+  apply (rule allI, rule impI)
+  apply (elim pc_end pc_next pc_0)
+  apply auto
+  done
+
+lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)"
+  apply (auto simp add: check_types_def phi_makelist_def JVM_states_unfold)
+  apply (unfold list_def)
+  apply auto
+  done
 
 lemma wt_makelist [simp]:
   "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
-  apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
+  apply (simp add: wt_method_def)
+  apply (simp add: make_list_ins_def phi_makelist_def)
   apply (simp add: wt_start_def nat_number)
   apply (simp add: wt_instr_def)
   apply clarify
@@ -375,8 +406,8 @@
 section "Example for code generation: inferring method types"
 
 constdefs
-  test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty List.list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
-             exception_table \<Rightarrow> instr List.list \<Rightarrow> JVMType.state List.list"
+  test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
+             exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list"
   "test_kil G C pTs rT mxs mxl et instr ==
    (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
         start  = OK first#(replicate (size instr - 1) (OK None))
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> 
diff -r 833ffcb2e92d -r 2aa33ed5f526 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Fri Jun 14 13:24:32 2002 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy	Fri Jun 14 23:25:36 2002 +0200
@@ -10,10 +10,6 @@
 
 
 constdefs
-  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)"
-
   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 (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
@@ -78,23 +74,8 @@
 *}
 
 lemma check_bounded_is_bounded:
-  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"
-  apply (unfold bounded_def eff_def)
-  apply clarify
-  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
-   
+  "check_bounded ins et \<Longrightarrow> bounded (\<lambda>pc. eff (ins!pc) G pc et) (length ins)"  
+  by (unfold bounded_def) (blast dest: check_boundedD)
 
 lemma special_ex_swap_lemma [iff]: 
   "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
@@ -315,6 +296,8 @@
   apply (erule exec_mono, assumption)  
   done
 
+lemma map_id: "\<forall>x \<in> set xs. f (g x) = x \<Longrightarrow> map f (map g xs) = xs"
+  by (induct xs) auto
 
 theorem wt_kil_correct:
   "\<lbrakk> wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G; 
@@ -367,7 +350,7 @@
          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
+    phi': "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 et bs) phi'"
     by blast
@@ -378,10 +361,22 @@
   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  
+  from phi' 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)
+    by (clarsimp simp add: not_Err_eq)  
+
+  from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
+  also from w have "phi' = map OK (map ok_val phi')" 
+    apply (clarsimp simp add: wt_step_def)
+    apply (rule map_id [symmetric])
+    apply (clarsimp simp add: in_set_conv_decomp)
+    apply (erule_tac x = "length ys" in allE)
+    apply (clarsimp simp add: nth_append not_Err_eq)
+    done    
+  finally 
+  have check_types:
+    "check_types G maxs maxr (map OK (map ok_val phi'))" .
 
   from l bounded 
   have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')"
@@ -392,7 +387,7 @@
   have "wt_app_eff (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: wt_err_imp_wt_app_eff simp add: l exec_def)
-  with instrs l le bounded'
+  with instrs l le bounded bounded' check_types maxr
   have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')"
     apply (unfold wt_method_def wt_app_eff_def)
     apply simp
@@ -415,26 +410,32 @@
 
 theorem wt_kil_complete:
   "\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
-     check_bounded bs et; 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)) \<rbrakk>
+      is_class G C; 
+      \<forall>x \<in> set pTs. is_type G x \<rbrakk>
   \<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
 proof -
   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_phi: "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
-  assume bounded: "check_bounded bs et"
-
+  
+  let ?mxr = "1+size pTs+mxl"
+  
   assume "wt_method G C pTs rT maxs mxl bs et phi"
   then obtain
     instrs:   "0 < length bs" and
+    len:      "length phi = length bs" and
+    bounded:  "check_bounded bs et" and
+    ck_types: "check_types G maxs ?mxr (map OK phi)" 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) et pc"
     by (unfold wt_method_def) simp
 
+  from ck_types len
+  have istype_phi: 
+    "map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))"
+    by (auto simp add: check_types_def intro!: listI)
+
   let ?eff  = "\<lambda>pc. eff (bs!pc) G pc et"
   let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT pc et"
 
@@ -445,15 +446,15 @@
   from wt_ins
   have "wt_app_eff (sup_state_opt G) ?app ?eff phi"
     apply (unfold wt_app_eff_def wt_instr_def lesub_def)
-    apply (simp (no_asm) only: length)
+    apply (simp (no_asm) only: len)
     apply blast
     done
   with bounded_exec
   have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)"
-    by - (erule wt_app_eff_imp_wt_err,simp add: exec_def length)
+    by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len)
   hence wt_err:
     "wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)"
-    by (unfold exec_def) (simp add: length)
+    by (unfold exec_def) (simp add: len)
  
   let ?maxr = "1+size pTs+mxl"
   from wf bounded_exec
@@ -487,7 +488,7 @@
   let ?phi = "map OK phi"  
   have less_phi: "?start <=[JVMType.le G maxs ?maxr] ?phi"
   proof -
-    from length instrs
+    from len instrs
     have "length ?start = length (map OK phi)" by simp
     moreover
     { fix n
@@ -495,7 +496,7 @@
       have "G \<turnstile> ok_val (?start!0) <=' phi!0"
         by (simp add: wt_start_def)
       moreover
-      from instrs length
+      from instrs len
       have "0 < length phi" by simp
       ultimately
       have "JVMType.le G maxs ?maxr (?start!0) (?phi!0)"
@@ -525,35 +526,7 @@
   with bounded 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}.
 
-  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:
   "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
       t \<in> set (snd sig) \<rbrakk>
@@ -573,9 +546,9 @@
 qed
 
 
-theorem jvm_kildall_correct:
-  "wt_jvm_prog_kildall G \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
-proof -  
+theorem jvm_kildall_sound_complete:
+  "wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)"
+proof 
   assume wtk: "wt_jvm_prog_kildall G"
 
   then obtain wf_mb where
@@ -605,8 +578,34 @@
     apply (auto intro: someI)
     done
 
-  thus ?thesis by blast
+  thus "\<exists>Phi. wt_jvm_prog G Phi" by blast
+next
+  assume "\<exists>Phi. wt_jvm_prog G Phi"
+  then obtain Phi where wt: "wt_jvm_prog G Phi" ..
+
+  then obtain wf_mb where
+    wf: "wf_prog wf_mb G"
+    by (auto simp add: wt_jvm_prog_def)
+
+  { fix C S fs mdecls sig rT code
+    assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls"
+    with wf
+    have "method (G,C) sig = Some (C,rT,code) \<and> is_class G C \<and> (\<forall>t \<in> set (snd sig). is_type G t)"
+      by (simp add: methd is_type_pTs)
+  } note this [simp]
+ 
+  from wt
+  show "wt_jvm_prog_kildall G"
+    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def wf_prog_def wf_cdecl_def)
+    apply clarsimp
+    apply (drule bspec, assumption)
+    apply (unfold wf_mdecl_def)
+    apply clarsimp
+    apply (drule bspec, assumption)
+    apply clarsimp
+    apply (drule wt_kil_complete [OF _ wf])
+    apply (auto intro: someI)
+    done
 qed
 
-
 end