diff --git a/thys/JinjaDCI/BV/BVExec.thy b/thys/JinjaDCI/BV/BVExec.thy
--- a/thys/JinjaDCI/BV/BVExec.thy
+++ b/thys/JinjaDCI/BV/BVExec.thy
@@ -1,253 +1,506 @@
 (*  Title:      JinjaDCI/BV/BVExec.thy
 
     Author:     Tobias Nipkow, Gerwin Klein, Susannah Mansky
     Copyright   2000 TUM, 2020 UIUC
 
     Based on the Jinja theory BV/BVExec.thy by Tobias Nipkow and Gerwin Klein
 *)
 
 section \<open> Kildall for the JVM \label{sec:JVM} \<close>
 
 theory BVExec
-imports Jinja.Abstract_BV TF_JVM
+imports Jinja.Abstract_BV TF_JVM Jinja.Typing_Framework_2
 begin
 
 definition kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> 
              instr list \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i' err list \<Rightarrow> ty\<^sub>i' err list"
 where
   "kiljvm P mxs mxl T\<^sub>r is xt \<equiv>
   kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl) 
           (exec P mxs T\<^sub>r xt is)"
 
 definition wt_kildall :: "jvm_prog \<Rightarrow> cname \<Rightarrow> staticb \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
                  instr list \<Rightarrow> ex_table \<Rightarrow> bool"
 where
-  "wt_kildall P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<equiv>
-   0 < size is \<and> 
+  "wt_kildall P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<equiv> (b = Static \<or> b = NonStatic) \<and>
+   0 < size is \<and>  
    (let first  = Some ([],(case b of Static \<Rightarrow> [] | NonStatic \<Rightarrow> [OK (Class C')])
                             @(map OK Ts)@(replicate mxl\<^sub>0 Err));
         start  = (OK first)#(replicate (size is - 1) (OK None));
         result = kiljvm P mxs
                    ((case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1)+size Ts+mxl\<^sub>0)
                      T\<^sub>r is xt start
     in \<forall>n < size is. result!n \<noteq> Err)"
 
 definition wf_jvm_prog\<^sub>k :: "jvm_prog \<Rightarrow> bool"
 where
   "wf_jvm_prog\<^sub>k P \<equiv>
   wf_prog (\<lambda>P C' (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). wt_kildall P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt) P"
 
 
+context start_context
+begin
+
+lemma Cons_less_Conss3 [simp]:
+  "x#xs [\<sqsubset>\<^bsub>r\<^esub>] y#ys = (x \<sqsubset>\<^bsub>r\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys)"
+  apply (unfold lesssub_def )
+  apply auto
+  apply (insert sup_state_opt_err)
+  apply (unfold lesssub_def lesub_def sup_state_opt_def sup_state_def sup_ty_opt_def)
+  apply (simp only: JVM_le_unfold )
+  apply fastforce
+  done
+
+lemma acc_le_listI3 [intro!]:
+  " acc r \<Longrightarrow> acc (Listn.le r)"
+apply (unfold acc_def)
+apply (subgoal_tac
+ "wf(UN n. {(ys,xs). size xs = n \<and> size ys = n \<and> xs <_(Listn.le r) ys})")
+   apply (erule wf_subset)
+ apply (blast intro: lesssub_lengthD)
+apply (rule wf_UN)
+ prefer 2
+ apply (rename_tac m n)
+ apply (case_tac "m=n")
+  apply simp
+ apply (fast intro!: equals0I dest: not_sym)
+apply (rename_tac n)
+apply (induct_tac n)
+ apply (simp add: lesssub_def cong: conj_cong)
+apply (rename_tac k)
+apply (simp add: wf_eq_minimal del: r_def f_def step_def A_def)
+apply (simp (no_asm) add: length_Suc_conv cong: conj_cong del: r_def f_def step_def A_def)
+apply clarify
+apply (rename_tac M m)
+apply (case_tac "\<exists>x xs. size xs = k \<and> x#xs \<in> M")
+ prefer 2
+ apply (erule thin_rl)
+ apply (erule thin_rl)
+ apply blast
+apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
+apply (erule impE)
+ apply blast
+apply (thin_tac "\<exists>x xs. P x xs" for P)
+apply clarify
+apply (rename_tac maxA xs)
+apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
+apply (erule impE)
+ apply blast
+apply clarify
+apply (thin_tac "m \<in> M")
+apply (thin_tac "maxA#xs \<in> M")
+apply (rule bexI)
+ prefer 2
+ apply assumption
+apply clarify
+apply (simp del: r_def f_def step_def A_def)
+apply blast
+  done
+
+
+lemma wf_jvm: " wf {(ss', ss). ss [\<sqsubset>\<^bsub>r\<^esub>] ss'}"
+  apply (insert acc_le_listI3 acc_JVM [OF wf])
+  by (simp add: acc_def r_def) 
+
+lemma iter_properties_bv[rule_format]:
+shows "\<lbrakk> \<forall>p\<in>w0. p < n; ss0 \<in> list n A; \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
+         iter f step ss0 w0 = (ss',w') \<longrightarrow>
+         ss' \<in> list n A \<and> stables r step ss' \<and> ss0 [\<sqsubseteq>\<^sub>r] ss' \<and>
+         (\<forall>ts\<in>list n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> ss' [\<sqsubseteq>\<^sub>r] ts)"
+(*<*) (is "PROP ?P")
+
+proof -
+  show "PROP ?P"
+    apply (insert semi bounded_step exec_pres_type step_mono[OF wf])  
+    apply (unfold iter_def stables_def)
+
+    apply (rule_tac P = "\<lambda>(ss,w).
+                ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 [\<sqsubseteq>\<^sub>r] ss \<and>
+   (\<forall>ts\<in>list n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow> ss [\<sqsubseteq>\<^sub>r] ts) \<and>
+   (\<forall>p\<in>w. p < n)" and
+   r = "{(ss',ss) . ss [\<sqsubset>\<^sub>r] ss'} <*lex*> finite_psubset"
+         in while_rule)
+
+  \<comment> \<open>Invariant holds initially:\<close>  
+        apply (simp add:stables_def  semilat_Def   del: n_def A_def r_def f_def step_def)
+        apply (blast intro:le_list_refl')     
+   
+  \<comment> \<open>Invariant is preserved:\<close>
+       apply(simp add: stables_def split_paired_all del: A_def r_def f_def step_def n_def)
+       apply(rename_tac ss w)
+       apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
+        prefer 2 apply (fast intro: someI)
+       apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
+        prefer 2
+        apply clarify
+        apply (rule conjI)
+         apply(clarsimp, blast dest!: boundedD)
+        apply (subgoal_tac "(SOME p. p \<in> w) < n")
+         apply (subgoal_tac "(ss ! (SOME p. p \<in> w)) \<in> A")
+          apply (fastforce simp only:n_def dest:pres_typeD )   
+         apply simp
+        apply simp
+       apply (subst decomp_propa)
+        apply blast
+       apply (simp del:A_def r_def f_def step_def n_def)
+       apply (rule conjI)
+        apply (rule Semilat.merges_preserves_type[OF Semilat.intro, OF semi])
+         apply blast
+        apply clarify
+        apply (rule conjI)
+         apply(clarsimp, blast dest!: boundedD)
+        apply (erule pres_typeD)
+          prefer 3
+          apply assumption
+         apply (erule listE_nth_in)
+         apply blast
+        apply (simp only:n_def)
+       apply (rule conjI)
+        apply clarify
+        apply (subgoal_tac "ss \<in> list (length is) A" "\<forall>p\<in>w. p <  (length is) " "\<forall>p<(length is). p \<notin> w \<longrightarrow> stable r step ss p "
+ "p < length is")
+            apply (blast   intro!: Semilat.stable_pres_lemma[OF Semilat.intro, OF semi])
+           apply (simp only:n_def)
+          apply (simp only:n_def)
+         apply (simp only:n_def)
+        apply (simp only:n_def)
+       apply (rule conjI)
+        apply (subgoal_tac "ss \<in> list (length is) A" 
+               "\<forall>(q,t)\<in>set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length is \<and> t \<in> A"
+               "ss [\<sqsubseteq>\<^bsub>r\<^esub>] merges f (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))) ss" "ss0\<in> list (size is) A"
+               "merges f (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))) ss \<in> list (size is) A" 
+               "ss \<in>list (size is) A" "order r A" "ss0 [\<sqsubseteq>\<^bsub>r\<^esub>] ss ")
+                apply (blast dest: le_list_trans)
+               apply simp
+              apply (simp only:semilat_Def)
+             apply (simp only:n_def)
+            apply (fastforce simp only: n_def dest:Semilat.merges_preserves_type[OF Semilat.intro, OF semi] )
+           apply (simp only:n_def)
+          apply (blast intro:Semilat.merges_incr[OF Semilat.intro, OF semi])
+         apply (subgoal_tac "length ss = n")
+          apply (simp only:n_def)
+         apply (subgoal_tac "ss \<in>list n A")
+          defer
+          apply simp
+         apply (simp only:n_def)
+        prefer 5
+        apply (simp only:listE_length n_def)
+       apply(rule conjI)
+        apply (clarsimp simp del: A_def r_def f_def step_def)
+        apply (blast intro!: Semilat.merges_bounded_lemma[OF Semilat.intro, OF semi])       
+       apply (subgoal_tac "bounded step n")
+        apply (blast dest!: boundedD)
+       apply (simp only:n_def)
+
+  \<comment> \<open>Postcondition holds upon termination:\<close>
+      apply(clarsimp simp add: stables_def split_paired_all)
+  
+  \<comment> \<open>Well-foundedness of the termination relation:\<close>    
+      apply (rule wf_lex_prod)
+     apply (simp only:wf_jvm) 
+    apply (rule wf_finite_psubset) 
+
+  \<comment> \<open>Loop decreases along termination relation:\<close>
+     apply(simp add: stables_def split_paired_all del: A_def r_def f_def step_def)
+     apply(rename_tac ss w)
+     apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
+      prefer 2 apply (fast intro: someI)
+     apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
+      prefer 2
+      apply clarify
+      apply (rule conjI)
+       apply(clarsimp, blast dest!: boundedD)
+      apply (erule pres_typeD)
+        prefer 3
+        apply assumption
+       apply (erule listE_nth_in)
+       apply blast
+      apply blast
+     apply (subst decomp_propa)
+      apply blast
+     apply clarify
+  apply (simp del: listE_length  A_def r_def f_def step_def
+      add: lex_prod_def finite_psubset_def 
+           bounded_nat_set_is_finite)
+     apply (rule termination_lemma)
+        apply (insert Semilat.intro)
+        apply assumption+
+      defer
+      apply assumption
+     defer
+     apply clarsimp   
+    done
+qed
+
+(*>*)
+
+
+lemma kildall_properties_bv: 
+shows "\<lbrakk> ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
+  kildall r f step ss0 \<in> list n A \<and>
+  stables r step (kildall r f step ss0) \<and>
+  ss0 [\<sqsubseteq>\<^sub>r] kildall r f step ss0 \<and>
+  (\<forall>ts\<in>list n A. ss0 [\<sqsubseteq>\<^sub>r] ts \<and> stables r step ts \<longrightarrow>
+                 kildall r f step ss0 [\<sqsubseteq>\<^sub>r] ts)"
+(*<*) (is "PROP ?P")
+proof -
+  show "PROP ?P"
+  apply (unfold kildall_def)
+    apply(case_tac "iter f step ss0 (unstables r step ss0)")
+    apply (simp del:r_def f_def n_def step_def A_def)
+    apply (rule iter_properties_bv)      
+     apply (simp_all add: unstables_def stable_def)
+    done
+qed
+
+end
+
 theorem (in start_context) is_bcv_kiljvm:
   "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
 (*<*)
+  apply (insert wf)
+  apply (unfold kiljvm_def)
+  apply (fold r_def f_def step_def_exec n_def)
+  apply(unfold is_bcv_def wt_step_def)
+  apply(insert semi  kildall_properties_bv)
+  apply(simp only:stables_def)
+  apply clarify
+  apply(subgoal_tac "kildall r f step \<tau>s\<^sub>0 \<in> list n A")
+   prefer 2
+   apply (fastforce intro: kildall_properties_bv)
+  apply (rule iffI)
+   apply (rule_tac x = "kildall r f step \<tau>s\<^sub>0" in bexI) 
+    apply (rule conjI)
+     apply (fastforce intro: kildall_properties_bv)
+  apply (force intro: kildall_properties_bv)
+   apply simp
+  apply clarify
+  apply(subgoal_tac "kildall r f step \<tau>s\<^sub>0!pa <=_r \<tau>s!pa")
+   defer
+   apply (blast intro!: le_listD less_lengthI)
+  apply (subgoal_tac "\<tau>s!pa \<noteq> Err")
+   defer
+   apply simp
+  apply (rule ccontr)
+  apply (simp only:top_def r_def JVM_le_unfold)
+  apply fastforce
+  done
+(*
 proof -
   let ?n = "length is"
   have "Semilat A r f" using semilat_JVM[OF wf]
     by (simp add: Semilat.intro sl_def2)
   moreover have "acc r" using wf by simp blast
   moreover have "top r Err" by (simp add: JVM_le_unfold)
   moreover have "pres_type step ?n A" by (rule exec_pres_type)
   moreover have "bounded step ?n" by (rule bounded_step)
   moreover have "mono r step ?n A" using step_mono[OF wf] by simp
   ultimately have "is_bcv r Err step ?n A (kildall r f step)"
     by(rule is_bcv_kildall)
   moreover have kileq: "kiljvm P mxs mxl T\<^sub>r is xt = kildall r f step"
     using f_def kiljvm_def r_def step_def_exec by blast
   ultimately show ?thesis by simp
 qed
+*)
 (*>*)
 
 (* FIXME: move? *)
 lemma subset_replicate [intro?]: "set (replicate n x) \<subseteq> {x}"
   by (induct n) auto
 
 lemma in_set_replicate:
   assumes "x \<in> set (replicate n y)"
   shows "x = y"
 (*<*)
 proof -
   note assms
   also have "set (replicate n y) \<subseteq> {y}" ..
   finally show ?thesis by simp
 qed
 (*>*)
 
 lemma (in start_context) start_in_A [intro?]:
   "0 < size is \<Longrightarrow> start \<in> list (size is) A"
   using Ts C
 (*<*)
 proof(cases b)
 qed (force simp: JVM_states_unfold intro!: listI list_appendI
            dest!: in_set_replicate)+
 (*>*)
 
 
 theorem (in start_context) wt_kil_correct:
   assumes wtk: "wt_kildall P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
   shows "\<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
 (*<*)
 proof -
   from wtk obtain res where    
     result:   "res = kiljvm P mxs mxl T\<^sub>r is xt start" and
     success:  "\<forall>n < size is. res!n \<noteq> Err" and
-    instrs:   "0 < size is" 
+    instrs:   "0 < size is" and
+    stab:     "b = Static \<or> b = NonStatic" 
     by (unfold wt_kildall_def) simp
       
   have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
     by (rule is_bcv_kiljvm)
     
   from instrs have "start \<in> list (size is) A" ..
   with bcv success result have 
     "\<exists>ts\<in>list (size is) A. start [\<sqsubseteq>\<^sub>r] ts \<and> wt_step r Err step ts"
     by (unfold is_bcv_def) blast
   then obtain \<tau>s' where
     in_A: "\<tau>s' \<in> list (size is) A" and
     s:    "start [\<sqsubseteq>\<^sub>r] \<tau>s'" and
     w:    "wt_step r Err step \<tau>s'"
     by blast
   hence wt_err_step: "wt_err_step (sup_state_opt P) step \<tau>s'"
     by (simp add: wt_err_step_def JVM_le_Err_conv)
 
   from in_A have l: "size \<tau>s' = size is" by simp  
   moreover {
     from in_A  have "check_types P mxs mxl \<tau>s'" by (simp add: check_types_def)
     also from w have "\<forall>x \<in> set \<tau>s'. x \<noteq> Err" 
       by (auto simp add: wt_step_def all_set_conv_all_nth)
     hence [symmetric]: "map OK (map ok_val \<tau>s') = \<tau>s'" 
       by (auto intro!: map_idI simp add: wt_step_def)
     finally  have "check_types P mxs mxl (map OK (map ok_val \<tau>s'))" .
   } 
   moreover {  
     from s have "start!0 \<sqsubseteq>\<^sub>r \<tau>s'!0" by (rule le_listD) simp
     moreover
     from instrs w l 
     have "\<tau>s'!0 \<noteq> Err" by (unfold wt_step_def) simp
     then obtain \<tau>s0 where "\<tau>s'!0 = OK \<tau>s0" by auto
     ultimately
     have "wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s')" using l instrs
       by (unfold wt_start_def) 
          (cases b; simp add: lesub_def JVM_le_Err_conv Err.le_def)
   }
   moreover 
   from in_A have "set \<tau>s' \<subseteq> A" by simp  
   with wt_err_step bounded_step
   have "wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s')"
     by (auto intro: wt_err_imp_wt_app_eff simp add: l)
   ultimately
   have "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s')"
-    using instrs by (simp add: wt_method_def2 check_types_def del: map_map)
+    using instrs stab by (simp add: wt_method_def2 check_types_def del: map_map)
   thus ?thesis by blast
 qed
 (*>*)
 
 
 theorem (in start_context) wt_kil_complete:
   assumes wtm: "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
   shows "wt_kildall P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
 (*<*)
 proof -
   from wtm obtain
     instrs:   "0 < size is" and
     length:   "length \<tau>s = length is" and 
     ck_type:  "check_types P mxs mxl (map OK \<tau>s)" and
     wt_start: "wt_start P C b Ts mxl\<^sub>0 \<tau>s" and
-    app_eff:  "wt_app_eff (sup_state_opt P) app eff \<tau>s"
-    by (simp add: wt_method_def2 check_types_def)
+    app_eff:  "wt_app_eff (sup_state_opt P) app eff \<tau>s"  and
+    stab: "b = Static \<or> b = NonStatic" 
+    by (simp add: wt_method_def2 check_types_def )
 
   from ck_type
   have in_A: "set (map OK \<tau>s) \<subseteq> A" 
     by (simp add: check_types_def)  
   with app_eff in_A bounded_step
   have "wt_err_step (sup_state_opt P) (err_step (size \<tau>s) app eff) (map OK \<tau>s)"
     by - (erule wt_app_eff_imp_wt_err,
           auto simp add: exec_def length states_def)
   hence wt_err: "wt_err_step (sup_state_opt P) step (map OK \<tau>s)" 
     by (simp add: length)
   have is_bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
     by (rule is_bcv_kiljvm)
   moreover from instrs have "start \<in> list (size is) A" ..
   moreover
   let ?\<tau>s = "map OK \<tau>s"  
   have less_\<tau>s: "start [\<sqsubseteq>\<^sub>r] ?\<tau>s"
   proof (rule le_listI)
     from length instrs
     show "length start = length (map OK \<tau>s)" by simp
   next
     fix n
     from wt_start have "P \<turnstile> ok_val (start!0) \<le>' \<tau>s!0" 
       by (cases b; simp add: wt_start_def)
     moreover from instrs length have "0 < length \<tau>s" by simp
     ultimately have "start!0 \<sqsubseteq>\<^sub>r ?\<tau>s!0" 
       by (simp add: JVM_le_Err_conv lesub_def)
     moreover {
       fix n'
       have "OK None \<sqsubseteq>\<^sub>r ?\<tau>s!n"
         by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
                  split: err.splits)
       hence "\<lbrakk>n = Suc n'; n < size start\<rbrakk> \<Longrightarrow> start!n \<sqsubseteq>\<^sub>r ?\<tau>s!n" by simp
     }
     ultimately
     show "n < size start \<Longrightarrow> start!n \<sqsubseteq>\<^sub>r ?\<tau>s!n" by (cases n, blast+)   
   qed
   moreover
   from ck_type length
   have "?\<tau>s \<in> list (size is) A"
     by (auto intro!: listI simp add: check_types_def)
   moreover
   from wt_err have "wt_step r Err step ?\<tau>s" 
     by (simp add: wt_err_step_def JVM_le_Err_conv)
   ultimately
   have "\<forall>p. p < size is \<longrightarrow> kiljvm P  mxs mxl T\<^sub>r is xt start ! p \<noteq> Err" 
     by (unfold is_bcv_def) blast
   with instrs 
-  show "wt_kildall P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt" by (unfold wt_kildall_def) simp
+  show "wt_kildall P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt" 
+    using start_context_intro_auxi[OF staticb] using stab by (unfold wt_kildall_def) simp
 qed
 (*>*)
 
 
 theorem jvm_kildall_correct:
   "wf_jvm_prog\<^sub>k P = wf_jvm_prog P"
 (*<*)
 proof -
   let ?\<Phi> = "\<lambda>C M. let (C,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)) = method P C M in 
               SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
   let ?A = "\<lambda>P C' (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_kildall P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
   let ?B\<^sub>\<Phi> = "\<lambda>\<Phi>. (\<lambda>P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
                 wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M))"
 
   show ?thesis proof(rule iffI)
     \<comment> \<open>soundness\<close>
     assume wt: "wf_jvm_prog\<^sub>k P"
-    then have "wf_prog ?A P" by(simp add: wf_jvm_prog\<^sub>k_def)
+    then have wt': "wf_prog ?A P" by(simp add: wf_jvm_prog\<^sub>k_def)
     moreover {
       fix wf_md C M b Ts Ca T m bd
-      assume "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
-             "set Ts \<subseteq> types P" and "bd = (M, b, Ts, T, m)" and
-             "?A P Ca bd"
-      then have "(?B\<^sub>\<Phi> ?\<Phi>) P Ca bd" using sees_method_is_class[OF sees]
-        by (auto dest!: start_context.wt_kil_correct [OF start_context.intro] 
+
+      assume ass1: "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
+             ass2: "set Ts \<subseteq> types P" and ass3: "bd = (M, b, Ts, T, m)" and
+             ass4: "?A P Ca bd" 
+      from ass3 ass4 have stab: "b = Static \<or> b = NonStatic" by (simp add:wt_kildall_def)
+      from ass1 sees ass2 ass3 ass4 have "(?B\<^sub>\<Phi> ?\<Phi>) P Ca bd" using sees_method_is_class[OF sees]
+        by (auto dest!: start_context.wt_kil_correct[OF start_context_intro_auxi[OF stab]]
                  intro: someI)
     }
     ultimately have "wf_prog (?B\<^sub>\<Phi> ?\<Phi>) P" by(rule wf_prog_lift)
     then have "wf_jvm_prog\<^bsub>?\<Phi>\<^esub> P" by (simp add: wf_jvm_prog_phi_def)
     thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
   next  
     \<comment> \<open>completeness\<close>
-    assume wt: "wf_jvm_prog P"
+    
+    assume wt: "wf_jvm_prog P" 
     then obtain \<Phi> where "wf_prog (?B\<^sub>\<Phi> \<Phi>) P" by(clarsimp simp: wf_jvm_prog_def wf_jvm_prog_phi_def)
     moreover {
       fix wf_md C M b Ts Ca T m bd
-      assume "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
-             "set Ts \<subseteq> types P" and "bd = (M, b, Ts, T, m)" and
-             "(?B\<^sub>\<Phi> \<Phi>) P Ca bd"
-      then have "?A P Ca bd" using sees_method_is_class[OF sees]
-        by (auto intro!: start_context.wt_kil_complete start_context.intro)
+      assume ass1: "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
+             ass2: "set Ts \<subseteq> types P" and ass3: "bd = (M, b, Ts, T, m)" and
+             ass4: "(?B\<^sub>\<Phi> \<Phi>) P Ca bd"
+      from ass3 ass4 have stab: "b = Static \<or> b = NonStatic"  by (simp add:wt_method_def)
+      from ass1 sees ass2 ass3 ass4 have "?A P Ca bd" using sees_method_is_class[OF sees] using JVM_sl.staticb
+        by (auto intro!: start_context.wt_kil_complete start_context_intro_auxi[OF stab])
     }
     ultimately have "wf_prog ?A P" by(rule wf_prog_lift)
     thus "wf_jvm_prog\<^sub>k P" by (simp add: wf_jvm_prog\<^sub>k_def)
   qed
 qed
 (*>*)
 
 end
diff --git a/thys/JinjaDCI/BV/BVSpec.thy b/thys/JinjaDCI/BV/BVSpec.thy
--- a/thys/JinjaDCI/BV/BVSpec.thy
+++ b/thys/JinjaDCI/BV/BVSpec.thy
@@ -1,113 +1,113 @@
 (*  Title:      JinjaDCI/BV/BVSpec.thy
 
     Author:     Cornelia Pusch, Gerwin Klein, Susannah Mansky
     Copyright   1999 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory BV/BVSpec.thy by Tobias Nipkow
 *)
 
 section \<open> The Bytecode Verifier \label{sec:BVSpec} \<close>
 
 theory BVSpec
 imports Effect
 begin
 
 text \<open>
   This theory contains a specification of the BV. The specification
   describes correct typings of method bodies; it corresponds 
   to type \emph{checking}.
 \<close>
 
 
 definition
   \<comment> \<open>The method type only contains declared classes:\<close>
   check_types :: "'m prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty\<^sub>i' err list \<Rightarrow> bool"
 where 
   "check_types P mxs mxl \<tau>s \<equiv> set \<tau>s \<subseteq> states P mxs mxl"
 
   \<comment> \<open>An instruction is welltyped if it is applicable and its effect\<close>
   \<comment> \<open>is compatible with the type at all successor instructions:\<close>
 definition
   wt_instr :: "['m prog,ty,nat,pc,ex_table,instr,pc,ty\<^sub>m] \<Rightarrow> bool"
   ("_,_,_,_,_ \<turnstile> _,_ :: _" [60,0,0,0,0,0,0,61] 60)
 where
   "P,T,mxs,mpc,xt \<turnstile> i,pc :: \<tau>s \<equiv>
   app i P mxs T pc mpc xt (\<tau>s!pc) \<and> 
   (\<forall>(pc',\<tau>') \<in> set (eff i P pc xt (\<tau>s!pc)). P \<turnstile> \<tau>' \<le>' \<tau>s!pc')"
 
   \<comment> \<open>The type at @{text "pc=0"} conforms to the method calling convention:\<close>
 definition wt_start :: "['m prog,cname,staticb,ty list,nat,ty\<^sub>m] \<Rightarrow> bool"
 where
   "wt_start P C b Ts mxl\<^sub>0 \<tau>s \<equiv>
 case b of NonStatic \<Rightarrow> P \<turnstile> Some ([],OK (Class C)#map OK Ts@replicate mxl\<^sub>0 Err) \<le>' \<tau>s!0
         | Static \<Rightarrow>  P \<turnstile> Some ([],map OK Ts@replicate mxl\<^sub>0 Err) \<le>' \<tau>s!0"
 
   \<comment> \<open>A method is welltyped if the body is not empty,\<close>
   \<comment> \<open>if the method type covers all instructions and mentions\<close>
   \<comment> \<open>declared classes only, if the method calling convention is respected, and\<close>
   \<comment> \<open>if all instructions are welltyped.\<close>
 definition wt_method :: "['m prog,cname,staticb,ty list,ty,nat,nat,instr list,
                  ex_table,ty\<^sub>m] \<Rightarrow> bool"
 where
-  "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s \<equiv>
+  "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s \<equiv> (b = Static \<or> b = NonStatic) \<and>
   0 < size is \<and> size \<tau>s = size is \<and>
   check_types P mxs ((case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1)+size Ts+mxl\<^sub>0) (map OK \<tau>s) \<and>
   wt_start P C b Ts mxl\<^sub>0 \<tau>s \<and>
   (\<forall>pc < size is. P,T\<^sub>r,mxs,size is,xt \<turnstile> is!pc,pc :: \<tau>s)"
 
   \<comment> \<open>A program is welltyped if it is wellformed and all methods are welltyped\<close>
 definition  wf_jvm_prog_phi :: "ty\<^sub>P \<Rightarrow> jvm_prog \<Rightarrow> bool" ("wf'_jvm'_prog\<^bsub>_\<^esub>")
 where
   "wf_jvm_prog\<^bsub>\<Phi>\<^esub> \<equiv>
     wf_prog (\<lambda>P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
       wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M))"
 
 definition wf_jvm_prog :: "jvm_prog \<Rightarrow> bool"
 where
   "wf_jvm_prog P \<equiv> \<exists>\<Phi>. wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
 
 lemma wt_jvm_progD:
   "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P \<Longrightarrow> \<exists>wt. wf_prog wt P"
 (*<*) by (unfold wf_jvm_prog_phi_def, blast) (*>*)
 
 lemma wt_jvm_prog_impl_wt_instr:
 assumes wf: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P" and
       sees: "P \<turnstile> C sees M,b:Ts \<rightarrow> T = (mxs,mxl\<^sub>0,ins,xt) in C" and
         pc: "pc < size ins"
 shows "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: \<Phi> C M"
 (*<*)
 proof -
   have wfm: "wf_prog
      (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
          wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P" using wf
     by (unfold wf_jvm_prog_phi_def)
   show ?thesis using sees_wf_mdecl[OF wfm sees] pc
     by (simp add: wf_mdecl_def wt_method_def)
 qed
 (*>*)
 
 lemma wt_jvm_prog_impl_wt_start:
 assumes wf: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P" and
       sees: "P \<turnstile> C sees M,b:Ts \<rightarrow> T = (mxs,mxl\<^sub>0,ins,xt) in C"
 shows "0 < size ins \<and> wt_start P C b Ts mxl\<^sub>0 (\<Phi> C M)"
 (*<*)
 proof -
   have wfm: "wf_prog
      (\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
          wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)) P" using wf
     by (unfold wf_jvm_prog_phi_def)
   show ?thesis using sees_wf_mdecl[OF wfm sees]
     by (simp add: wf_mdecl_def wt_method_def)
 qed
 (*>*)
 
 lemma wf_jvm_prog_nclinit:
 assumes wtp: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
   and meth:  "P \<turnstile> C sees M, b :  Ts\<rightarrow>T = (mxs, mxl\<^sub>0, ins, xt) in D"
   and wt:    "P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: \<Phi> C M"
   and pc:    "pc < length ins" and \<Phi>: "\<Phi> C M ! pc = Some(ST,LT)"
   and ins:   "ins ! pc = Invokestatic C\<^sub>0 M\<^sub>0 n"
 shows "M\<^sub>0 \<noteq> clinit"
  using assms by(simp add: wf_jvm_prog_phi_def wt_instr_def app_def)
 
 end
diff --git a/thys/JinjaDCI/BV/JVM_SemiType.thy b/thys/JinjaDCI/BV/JVM_SemiType.thy
--- a/thys/JinjaDCI/BV/JVM_SemiType.thy
+++ b/thys/JinjaDCI/BV/JVM_SemiType.thy
@@ -1,256 +1,388 @@
 (*  Title:      HOL/MicroJava/BV/JVM.thy
 
     Author:     Gerwin Klein
     Copyright   2000 TUM
 
 *)
 
 section \<open> The JVM Type System as Semilattice \<close>
 
 theory JVM_SemiType imports SemiType begin
 
 type_synonym ty\<^sub>l = "ty err list"
 type_synonym ty\<^sub>s = "ty list"
 type_synonym ty\<^sub>i = "ty\<^sub>s \<times> ty\<^sub>l"
 type_synonym ty\<^sub>i' = "ty\<^sub>i option"
 type_synonym ty\<^sub>m = "ty\<^sub>i' list"
 type_synonym ty\<^sub>P = "mname \<Rightarrow> cname \<Rightarrow> ty\<^sub>m"
 
 
 definition stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty\<^sub>s esl"
 where
   "stk_esl P mxs \<equiv> upto_esl mxs (SemiType.esl P)"
 
 definition loc_sl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty\<^sub>l sl"
 where
   "loc_sl P mxl \<equiv> Listn.sl mxl (Err.sl (SemiType.esl P))"
 
 definition sl :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty\<^sub>i' err sl"
 where
   "sl P mxs mxl \<equiv>
   Err.sl(Opt.esl(Product.esl (stk_esl P mxs) (Err.esl(loc_sl P mxl))))"
 
 
 definition states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty\<^sub>i' err set"
 where "states P mxs mxl \<equiv> fst(sl P mxs mxl)"
 
 definition le :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty\<^sub>i' err ord"
 where
   "le P mxs mxl \<equiv> fst(snd(sl P mxs mxl))"
 
 definition sup :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty\<^sub>i' err binop"
 where
   "sup P mxs mxl \<equiv> snd(snd(sl P mxs mxl))"
 
 
 definition sup_ty_opt :: "['c prog,ty err,ty err] \<Rightarrow> bool" 
     ("_ \<turnstile> _ \<le>\<^sub>\<top> _" [71,71,71] 70)
 where
   "sup_ty_opt P \<equiv> Err.le (subtype P)"
 
 definition sup_state :: "['c prog,ty\<^sub>i,ty\<^sub>i] \<Rightarrow> bool"   
     ("_ \<turnstile> _ \<le>\<^sub>i _" [71,71,71] 70)
 where
   "sup_state P \<equiv> Product.le (Listn.le (subtype P)) (Listn.le (sup_ty_opt P))"
 
 definition sup_state_opt :: "['c prog,ty\<^sub>i',ty\<^sub>i'] \<Rightarrow> bool" 
     ("_ \<turnstile> _ \<le>'' _" [71,71,71] 70)
 where
   "sup_state_opt P \<equiv> Opt.le (sup_state P)"
 
 abbreviation
   sup_loc :: "['c prog,ty\<^sub>l,ty\<^sub>l] \<Rightarrow> bool"  ("_ \<turnstile> _ [\<le>\<^sub>\<top>] _"  [71,71,71] 70)
   where "P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<equiv> list_all2 (sup_ty_opt P) LT LT'"
 
 notation (ASCII)
   sup_ty_opt  ("_ |- _ <=T _" [71,71,71] 70) and
   sup_state  ("_ |- _ <=i _"  [71,71,71] 70) and
   sup_state_opt  ("_ |- _ <=' _"  [71,71,71] 70) and
   sup_loc  ("_ |- _ [<=T] _"  [71,71,71] 70)
 
 
 subsection "Unfolding"
 
 lemma JVM_states_unfold: 
   "states P mxs mxl \<equiv> err(opt((Union {list n (types P) |n. n <= mxs}) \<times>
                                  list mxl (err(types P))))"
 (*<*)
   apply (unfold states_def sl_def Opt.esl_def Err.sl_def
          stk_esl_def loc_sl_def Product.esl_def
          Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def)
   apply simp
   done
 (*>*)
 
 lemma JVM_le_unfold:
  "le P m n \<equiv> 
   Err.le(Opt.le(Product.le(Listn.le(subtype P))(Listn.le(Err.le(subtype P)))))" 
 (*<*)
   apply (unfold le_def sl_def Opt.esl_def Err.sl_def
          stk_esl_def loc_sl_def Product.esl_def  
          Listn.sl_def upto_esl_def SemiType.esl_def Err.esl_def) 
   apply simp
   done
 (*>*)
     
 lemma sl_def2:
   "JVM_SemiType.sl P mxs mxl \<equiv> 
   (states P mxs mxl, JVM_SemiType.le P mxs mxl, JVM_SemiType.sup P mxs mxl)"
 (*<*) by (unfold JVM_SemiType.sup_def states_def JVM_SemiType.le_def) simp (*>*)
 
 
 lemma JVM_le_conv:
   "le P m n (OK t1) (OK t2) = P \<turnstile> t1 \<le>' t2"
 (*<*) by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def  
                 sup_state_def sup_ty_opt_def) (*>*)
 
 lemma JVM_le_Err_conv:
   "le P m n = Err.le (sup_state_opt P)"
 (*<*) by (unfold sup_state_opt_def sup_state_def  
              sup_ty_opt_def JVM_le_unfold) simp (*>*)
 
 lemma err_le_unfold [iff]: 
   "Err.le r (OK a) (OK b) = r a b"
 (*<*) by (simp add: Err.le_def lesub_def) (*>*)
   
 
 subsection \<open> Semilattice \<close>
-
+lemma order_sup_state_opt' [intro, simp]:
+  "wf_prog wf_mb P \<Longrightarrow> 
+      order (sup_state_opt P) (opt ((\<Union> {list n (types P) |n. n \<le> mxs} ) \<times> list (Suc (length Ts + mxl\<^sub>0)) (err (types P))))"   
+(*<*) 
+  apply (unfold sup_state_opt_def sup_state_def sup_ty_opt_def  ) 
+  apply (blast intro:order_le_prodI) \<comment>\<open> use Listn.thy.order_listI2  \<close>
+  done 
+(*<*) 
+lemma order_sup_state_opt'' [intro, simp]:
+  "wf_prog wf_mb P \<Longrightarrow> 
+      order (sup_state_opt P) (opt ((\<Union> {list n (types P) |n. n \<le> mxs} ) \<times> list ((length Ts + mxl\<^sub>0)) (err (types P))))"   
+(*<*) 
+  apply (unfold sup_state_opt_def sup_state_def sup_ty_opt_def  ) 
+  apply (blast intro:order_le_prodI) \<comment>\<open> use Listn.thy.order_listI2  \<close>
+  done 
+(*<*)
+(*
 lemma order_sup_state_opt [intro, simp]: 
   "wf_prog wf_mb P \<Longrightarrow> order (sup_state_opt P)"   
 (*<*) by (unfold sup_state_opt_def sup_state_def sup_ty_opt_def) blast (*>*)
+*)
 
 lemma semilat_JVM [intro?]:
   "wf_prog wf_mb P \<Longrightarrow> semilat (JVM_SemiType.sl P mxs mxl)"
 (*<*)
   apply (unfold JVM_SemiType.sl_def stk_esl_def loc_sl_def)  
   apply (blast intro: err_semilat_Product_esl err_semilat_upto_esl 
                       Listn_sl err_semilat_JType_esl)
   done
 (*>*)
 
-lemma acc_JVM [intro]:
-  "wf_prog wf_mb P \<Longrightarrow> acc (JVM_SemiType.le P mxs mxl)"
-(*<*) by (unfold JVM_le_unfold) blast (*>*)
-
-
 subsection \<open> Widening with @{text "\<top>"} \<close>
 
 lemma subtype_refl[iff]: "subtype P t t" (*<*) by (simp add: fun_of_def) (*>*)
 
 lemma sup_ty_opt_refl [iff]: "P \<turnstile> T \<le>\<^sub>\<top> T"
 (*<*)
   apply (unfold sup_ty_opt_def)
   apply (fold lesub_def)
   apply (rule le_err_refl)
   apply (simp add: lesub_def)
   done
 (*>*)
 
 lemma Err_any_conv [iff]: "P \<turnstile> Err \<le>\<^sub>\<top> T = (T = Err)"
 (*<*) by (unfold sup_ty_opt_def) (rule Err_le_conv [simplified lesub_def]) (*>*)
 
 lemma any_Err [iff]: "P \<turnstile> T \<le>\<^sub>\<top> Err"
 (*<*) by (unfold sup_ty_opt_def) (rule le_Err [simplified lesub_def]) (*>*)
 
 lemma OK_OK_conv [iff]:
   "P \<turnstile> OK T \<le>\<^sub>\<top> OK T' = P \<turnstile> T \<le> T'"
 (*<*) by (simp add: sup_ty_opt_def fun_of_def) (*>*)
 
 lemma any_OK_conv [iff]:
   "P \<turnstile> X \<le>\<^sub>\<top> OK T' = (\<exists>T. X = OK T \<and> P \<turnstile> T \<le> T')"
 (*<*)
   apply (unfold sup_ty_opt_def) 
   apply (rule le_OK_conv [simplified lesub_def])
   done  
 (*>*)
 
 lemma OK_any_conv:
  "P \<turnstile> OK T \<le>\<^sub>\<top> X = (X = Err \<or> (\<exists>T'. X = OK T' \<and> P \<turnstile> T \<le> T'))"
 (*<*)
   apply (unfold sup_ty_opt_def) 
   apply (rule OK_le_conv [simplified lesub_def])
   done
 (*>*)
 
 lemma sup_ty_opt_trans [intro?, trans]:
   "\<lbrakk>P \<turnstile> a \<le>\<^sub>\<top> b; P \<turnstile> b \<le>\<^sub>\<top> c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>\<top> c"
 (*<*) by (auto intro: widen_trans  
            simp add: sup_ty_opt_def Err.le_def lesub_def fun_of_def
            split: err.splits) (*>*)
 
 
 subsection "Stack and Registers"
 
 lemma stk_convert:
   "P \<turnstile> ST [\<le>] ST' = Listn.le (subtype P) ST ST'"
 (*<*) by (simp add: Listn.le_def lesub_def) (*>*)
 
 lemma sup_loc_refl [iff]: "P \<turnstile> LT [\<le>\<^sub>\<top>] LT"
 (*<*) by (rule list_all2_refl) simp (*>*)
 
 lemmas sup_loc_Cons1 [iff] = list_all2_Cons1 [of "sup_ty_opt P"] for P
 
 lemma sup_loc_def:
   "P \<turnstile> LT [\<le>\<^sub>\<top>] LT' \<equiv> Listn.le (sup_ty_opt P) LT LT'"
 (*<*) by (simp add: Listn.le_def lesub_def) (*>*)
 
 lemma sup_loc_widens_conv [iff]:
   "P \<turnstile> map OK Ts [\<le>\<^sub>\<top>] map OK Ts' = P \<turnstile> Ts [\<le>] Ts'"
 (*<*)
   by (simp add: list_all2_map1 list_all2_map2)
 (*>*)
 
 
 lemma sup_loc_trans [intro?, trans]:
   "\<lbrakk>P \<turnstile> a [\<le>\<^sub>\<top>] b; P \<turnstile> b [\<le>\<^sub>\<top>] c\<rbrakk> \<Longrightarrow> P \<turnstile> a [\<le>\<^sub>\<top>] c"
 (*<*) by (rule list_all2_trans, rule sup_ty_opt_trans) (*>*)
 
 
 subsection "State Type"
 
 lemma sup_state_conv [iff]:
   "P \<turnstile> (ST,LT) \<le>\<^sub>i (ST',LT') = (P \<turnstile> ST [\<le>] ST' \<and> P \<turnstile> LT [\<le>\<^sub>\<top>] LT')"
 (*<*) by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_def) (*>*)
   
 lemma sup_state_conv2:
   "P \<turnstile> s1 \<le>\<^sub>i s2 = (P \<turnstile> fst s1 [\<le>] fst s2 \<and> P \<turnstile> snd s1 [\<le>\<^sub>\<top>] snd s2)"
 (*<*) by (cases s1, cases s2) simp (*>*)
 
 lemma sup_state_refl [iff]: "P \<turnstile> s \<le>\<^sub>i s"
 (*<*) by (auto simp add: sup_state_conv2) (*>*)
 
 lemma sup_state_trans [intro?, trans]:
   "\<lbrakk>P \<turnstile> a \<le>\<^sub>i b; P \<turnstile> b \<le>\<^sub>i c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>\<^sub>i c"
 (*<*) by (auto intro: sup_loc_trans widens_trans simp add: sup_state_conv2) (*>*)
 
 
 lemma sup_state_opt_None_any [iff]:
   "P \<turnstile> None \<le>' s"
 (*<*) by (simp add: sup_state_opt_def Opt.le_def) (*>*)
 
 lemma sup_state_opt_any_None [iff]:
   "P \<turnstile> s \<le>' None = (s = None)"
 (*<*) by (simp add: sup_state_opt_def Opt.le_def) (*>*)
 
 lemma sup_state_opt_Some_Some [iff]:
   "P \<turnstile> Some a \<le>' Some b = P \<turnstile> a \<le>\<^sub>i b"  
 (*<*) by (simp add: sup_state_opt_def Opt.le_def lesub_def) (*>*)
 
 lemma sup_state_opt_any_Some:
   "P \<turnstile> (Some s) \<le>' X = (\<exists>s'. X = Some s' \<and> P \<turnstile> s \<le>\<^sub>i s')"
 (*<*) by (simp add: sup_state_opt_def Opt.le_def lesub_def) (*>*)
 
 lemma sup_state_opt_refl [iff]: "P \<turnstile> s \<le>' s"
 (*<*) by (simp add: sup_state_opt_def Opt.le_def lesub_def) (*>*)
 
 lemma sup_state_opt_trans [intro?, trans]:
   "\<lbrakk>P \<turnstile> a \<le>' b; P \<turnstile> b \<le>' c\<rbrakk> \<Longrightarrow> P \<turnstile> a \<le>' c"
 (*<*)
   apply (unfold sup_state_opt_def Opt.le_def lesub_def)
   apply (simp del: split_paired_All)
   apply (rule sup_state_trans, assumption+)
   done
 (*>*)
 
+
+lemma sup_state_opt_err  : "(Err.le (sup_state_opt P)) s s"
+  apply (unfold JVM_le_unfold Product.le_def Opt.le_def Err.le_def lesssub_def lesub_def Listn.le_def)
+  apply (auto split: err.splits)
+  done
+
+lemma Cons_less_Conss1 [simp]:
+  "x#xs [\<sqsubset>\<^bsub>subtype P\<^esub>] y#ys = (x \<sqsubset>\<^bsub>subtype P\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>subtype P\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys)"
+  apply (unfold lesssub_def )
+  apply auto
+  apply (simp add:lesssub_def lesub_def) \<comment>\<open>widen_refl, subtype_refl \<close>
+  done
+
+lemma Cons_less_Conss2 [simp]:
+  "x#xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y#ys = (x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<and> xs [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] ys \<or> x = y \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys)"
+  apply (unfold lesssub_def )
+  apply auto
+  apply (simp add:lesssub_def lesub_def Err.le_def split: err.splits)
+  done
+
+lemma acc_le_listI1 [intro!]:
+  " acc (subtype P) \<Longrightarrow> acc (Listn.le (subtype P))"
+  (*<*) 
+apply (unfold acc_def)
+apply (subgoal_tac
+ "wf(UN n. {(ys,xs). size xs = n \<and> size ys = n \<and> xs <_(Listn.le (subtype P)) ys})")
+   apply (erule wf_subset)
+
+ apply (blast intro: lesssub_lengthD)
+apply (rule wf_UN)
+ prefer 2
+ apply (rename_tac m n)
+ apply (case_tac "m=n")
+  apply simp
+ apply (fast intro!: equals0I dest: not_sym)
+apply (rename_tac n)
+apply (induct_tac n)
+ apply (simp add: lesssub_def cong: conj_cong)
+apply (rename_tac k)
+apply (simp add: wf_eq_minimal)
+apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
+apply clarify
+apply (rename_tac M m)
+apply (case_tac "\<exists>x xs. size xs = k \<and> x#xs \<in> M")
+ prefer 2
+ apply (erule thin_rl)
+ apply (erule thin_rl)
+ apply blast
+apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
+apply (erule impE)
+ apply blast
+apply (thin_tac "\<exists>x xs. P x xs" for P)
+apply clarify
+apply (rename_tac maxA xs)
+apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
+apply (erule impE)
+ apply blast
+apply clarify
+apply (thin_tac "m \<in> M")
+apply (thin_tac "maxA#xs \<in> M")
+apply (rule bexI)
+ prefer 2
+ apply assumption
+apply clarify
+apply simp
+apply blast
+  done
+
+lemma acc_le_listI2 [intro!]:
+  " acc (Err.le (subtype P)) \<Longrightarrow> acc (Listn.le (Err.le (subtype P)))"
+    (*<*) 
+apply (unfold acc_def)
+apply (subgoal_tac
+ "wf(UN n. {(ys,xs). size xs = n \<and> size ys = n \<and> xs <_(Listn.le (Err.le (subtype P))) ys})")
+   apply (erule wf_subset)
+
+ apply (blast intro: lesssub_lengthD)
+apply (rule wf_UN)
+ prefer 2
+ apply (rename_tac m n)
+ apply (case_tac "m=n")
+  apply simp
+ apply (fast intro!: equals0I dest: not_sym)
+apply (rename_tac n)
+apply (induct_tac n)
+ apply (simp add: lesssub_def cong: conj_cong)
+apply (rename_tac k)
+apply (simp add: wf_eq_minimal)
+apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
+apply clarify
+apply (rename_tac M m)
+apply (case_tac "\<exists>x xs. size xs = k \<and> x#xs \<in> M")
+ prefer 2
+ apply (erule thin_rl)
+ apply (erule thin_rl)
+ apply blast
+apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
+apply (erule impE)
+ apply blast
+apply (thin_tac "\<exists>x xs. P x xs" for P)
+apply clarify
+apply (rename_tac maxA xs)
+apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
+apply (erule impE)
+ apply blast
+apply clarify
+apply (thin_tac "m \<in> M")
+apply (thin_tac "maxA#xs \<in> M")
+apply (rule bexI)
+ prefer 2
+ apply assumption
+apply clarify
+apply simp
+apply blast
+  done
+
+lemma acc_JVM [intro]:
+  "wf_prog wf_mb P \<Longrightarrow> acc (JVM_SemiType.le P mxs mxl)"
+(*<*) by (unfold JVM_le_unfold) blast (*>*)  \<comment>\<open> use acc_listI1, acc_listI2 \<close>
+
 end
diff --git a/thys/JinjaDCI/BV/LBVJVM.thy b/thys/JinjaDCI/BV/LBVJVM.thy
--- a/thys/JinjaDCI/BV/LBVJVM.thy
+++ b/thys/JinjaDCI/BV/LBVJVM.thy
@@ -1,245 +1,250 @@
 (*  Title:      JinjaDCI/BV/LBVJVM.thy
 
     Author:     Tobias Nipkow, Gerwin Klein, Susannah Mansky
     Copyright   2000 TUM, 2020 UIUC
 
     Based on the Jinja theory BV/LBVJVM.thy by Tobias Nipkow and Gerwin Klein
 *)
 
 section \<open> LBV for the JVM \label{sec:JVM} \<close>
 
 theory LBVJVM
 imports Jinja.Abstract_BV TF_JVM
 begin
 
 type_synonym prog_cert = "cname \<Rightarrow> mname \<Rightarrow> ty\<^sub>i' err list"
 
 definition check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty\<^sub>i' err list \<Rightarrow> bool"
 where
   "check_cert P mxs mxl n cert \<equiv> check_types P mxs mxl cert \<and> size cert = n+1 \<and>
                                  (\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None"
 
 definition lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> ex_table \<Rightarrow> 
              ty\<^sub>i' err list \<Rightarrow> instr list \<Rightarrow> ty\<^sub>i' err \<Rightarrow> ty\<^sub>i' err"
 where
   "lbvjvm P mxs maxr T\<^sub>r et cert bs \<equiv>
   wtl_inst_list bs cert (JVM_SemiType.sup P mxs maxr) (JVM_SemiType.le P mxs maxr) Err (OK None) (exec P mxs T\<^sub>r et bs) 0"
 
 definition wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> staticb \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
              ex_table \<Rightarrow> ty\<^sub>i' err list \<Rightarrow> instr list \<Rightarrow> bool"
 where
-  "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et cert ins \<equiv>
+  "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et cert ins \<equiv> (b = Static \<or> b = NonStatic) \<and>
    check_cert P mxs ((case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1)+size Ts+mxl\<^sub>0) (size ins) cert \<and>
    0 < size ins \<and> 
    (let start  = Some ([],(case b of Static \<Rightarrow> [] | NonStatic \<Rightarrow> [OK (Class C)])
                             @((map OK Ts))@(replicate mxl\<^sub>0 Err));
         result = lbvjvm P mxs ((case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1)+size Ts+mxl\<^sub>0) T\<^sub>r et cert ins (OK start)
     in result \<noteq> Err)"
 
 definition wt_jvm_prog_lbv :: "jvm_prog \<Rightarrow> prog_cert \<Rightarrow> bool"
 where
   "wt_jvm_prog_lbv P cert \<equiv>
   wf_prog (\<lambda>P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (cert C mn) ins) P"
 
 definition mk_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> ex_table \<Rightarrow> instr list 
               \<Rightarrow> ty\<^sub>m \<Rightarrow> ty\<^sub>i' err list"
 where
   "mk_cert P mxs T\<^sub>r et bs phi \<equiv> make_cert (exec P mxs T\<^sub>r et bs) (map OK phi) (OK None)"
 
 definition prg_cert :: "jvm_prog \<Rightarrow> ty\<^sub>P \<Rightarrow> prog_cert"
 where
   "prg_cert P phi C mn \<equiv> let (C,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)) = method P C mn
                          in  mk_cert P mxs T\<^sub>r et ins (phi C mn)"
    
 lemma check_certD [intro?]:
   "check_cert P mxs mxl n cert \<Longrightarrow> cert_ok cert n Err (OK None) (states P mxs mxl)"
   by (unfold cert_ok_def check_cert_def check_types_def) auto
 
 
 lemma (in start_context) wt_lbv_wt_step:
   assumes lbv: "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is"
   shows "\<exists>\<tau>s \<in> list (size is) A. wt_step r Err step \<tau>s \<and> OK first \<sqsubseteq>\<^sub>r \<tau>s!0"
 (*<*)
 proof -
   from wf have "semilat (JVM_SemiType.sl P mxs mxl)" ..
   hence "semilat (A, r, f)" by (simp add: sl_def2)
   moreover have "top r Err" by (simp add: JVM_le_Err_conv)
   moreover have "Err \<in> A" by (simp add: JVM_states_unfold)
   moreover have "bottom r (OK None)" 
     by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
   moreover have "OK None \<in> A" by (simp add: JVM_states_unfold)
   moreover note bounded_step
   moreover from lbv have "cert_ok cert (size is) Err (OK None) A"
     by (unfold wt_lbv_def) (auto dest: check_certD)
   moreover note exec_pres_type
   moreover
   from lbv 
   have "wtl_inst_list is cert f r Err (OK None) step 0 (OK first) \<noteq> Err"
     by (cases b; simp add: wt_lbv_def lbvjvm_def step_def_exec [symmetric])
   moreover note first_in_A
   moreover from lbv have "0 < size is" by (simp add: wt_lbv_def)
   ultimately show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro])
 qed
 (*>*)
 
 
 lemma (in start_context) wt_lbv_wt_method:
   assumes lbv: "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is"  
   shows "\<exists>\<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
 (*<*)
 proof -
-  from lbv have l: "is \<noteq> []" by (simp add: wt_lbv_def)
+  from lbv have l: "is \<noteq> []" and  
+             stab: "b = Static \<or> b = NonStatic" by (auto simp add: wt_lbv_def)
   moreover
   from wf lbv C Ts obtain \<tau>s where 
     list:  "\<tau>s \<in> list (size is) A" and
     step:  "wt_step r Err step \<tau>s" and    
     start: "OK first \<sqsubseteq>\<^sub>r \<tau>s!0" 
     by (blast dest: wt_lbv_wt_step)
   from list have [simp]: "size \<tau>s = size is" by simp
   have "size (map ok_val \<tau>s) = size is" by simp  
   moreover from l have 0: "0 < size \<tau>s" by simp
   with step obtain \<tau>s0 where "\<tau>s!0 = OK \<tau>s0"
     by (unfold wt_step_def) blast
   with start 0 have "wt_start P C b Ts mxl\<^sub>0 (map ok_val \<tau>s)"
     by (cases b; simp add: wt_start_def JVM_le_Err_conv lesub_def Err.le_def)    
   moreover {
     from list have "check_types P mxs mxl \<tau>s" by (simp add: check_types_def)
     also from step  have "\<forall>x \<in> set \<tau>s. x \<noteq> Err" 
       by (auto simp add: all_set_conv_all_nth wt_step_def)    
     hence [symmetric]: "map OK (map ok_val \<tau>s) = \<tau>s"
       by (auto intro!: map_idI)
     finally have "check_types P mxs mxl (map OK (map ok_val \<tau>s))" .
   }
   moreover {  
     note bounded_step
     moreover from list have "set \<tau>s \<subseteq> A" by simp
     moreover from step have "wt_err_step (sup_state_opt P) step \<tau>s"
       by (simp add: wt_err_step_def JVM_le_Err_conv)
     ultimately have "wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s)"
       by (auto intro: wt_err_imp_wt_app_eff simp add: exec_def states_def)
   }    
   ultimately have "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s)"
     by (simp add: wt_method_def2 check_types_def del: map_map)
   thus ?thesis ..
 qed
 (*>*)
 
   
 lemma (in start_context) wt_method_wt_lbv:
   assumes wt: "wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s" 
   defines [simp]: "cert \<equiv> mk_cert P mxs T\<^sub>r xt is \<tau>s"
   
   shows "wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is" 
 (*<*)
 proof -
   let ?\<tau>s  = "map OK \<tau>s"
   let ?cert = "make_cert step ?\<tau>s (OK None)"
 
   from wt obtain 
     0:        "0 < size is" and
     size:     "size is = size ?\<tau>s" and
     ck_types: "check_types P mxs mxl ?\<tau>s" and
     wt_start: "wt_start P C b Ts mxl\<^sub>0 \<tau>s" and
     app_eff:  "wt_app_eff (sup_state_opt P) app eff \<tau>s"
     by (force simp add: wt_method_def2 check_types_def) 
   
   from wf have "semilat (JVM_SemiType.sl P mxs mxl)" ..
   hence "semilat (A, r, f)" by (simp add: sl_def2)
   moreover have "top r Err" by (simp add: JVM_le_Err_conv)
   moreover have "Err \<in> A" by (simp add: JVM_states_unfold)
   moreover have "bottom r (OK None)" 
     by (simp add: JVM_le_Err_conv bottom_def lesub_def Err.le_def split: err.split)
   moreover have "OK None \<in> A" by (simp add: JVM_states_unfold)
   moreover from wf have "mono r step (size is) A" by (rule step_mono)
   hence "mono r step (size ?\<tau>s) A" by (simp add: size)
   moreover from exec_pres_type 
   have "pres_type step (size ?\<tau>s) A" by (simp add: size) 
   moreover
   from ck_types have \<tau>s_in_A: "set ?\<tau>s \<subseteq> A" by (simp add: check_types_def)
   hence "\<forall>pc. pc < size ?\<tau>s \<longrightarrow> ?\<tau>s!pc \<in> A \<and> ?\<tau>s!pc \<noteq> Err" by auto
   moreover from bounded_step 
   have "bounded step (size ?\<tau>s)" by (simp add: size)
   moreover have "OK None \<noteq> Err" by simp
   moreover from bounded_step size \<tau>s_in_A app_eff
   have "wt_err_step (sup_state_opt P) step ?\<tau>s"
     by (auto intro: wt_app_eff_imp_wt_err simp add: exec_def states_def)    
   hence "wt_step r Err step ?\<tau>s"
     by (simp add: wt_err_step_def JVM_le_Err_conv)
   moreover
   from 0 size have "0 < size \<tau>s" by auto
   hence "?\<tau>s!0 = OK (\<tau>s!0)" by simp
   with wt_start have "OK first \<sqsubseteq>\<^sub>r ?\<tau>s!0"
     by (cases b; clarsimp simp add: wt_start_def lesub_def Err.le_def JVM_le_Err_conv)
   moreover note first_in_A
   moreover have "OK first \<noteq> Err" by simp
   moreover note size 
   ultimately
   have "wtl_inst_list is ?cert f r Err (OK None) step 0 (OK first) \<noteq> Err"
     by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro])
   moreover from 0 size have "\<tau>s \<noteq> []" by auto
   moreover from ck_types have "check_types P mxs mxl ?cert"
     by (fastforce simp: make_cert_def check_types_def JVM_states_unfold
                   dest!: nth_mem)
   moreover note 0 size
-  ultimately show ?thesis 
+  ultimately show ?thesis using staticb
     by (simp add: wt_lbv_def lbvjvm_def mk_cert_def step_def_exec [symmetric]
                   check_cert_def make_cert_def nth_append)
 qed  
 (*>*)
 
 
+
 theorem jvm_lbv_correct:
   "wt_jvm_prog_lbv P Cert \<Longrightarrow> wf_jvm_prog P"
 (*<*)
 proof -  
   let ?\<Phi> = "\<lambda>C mn. let (C,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)) = method P C mn in 
               SOME \<tau>s. wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
   
   let ?A = "\<lambda>P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)). wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins"
   let ?B = "\<lambda>P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
                 wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (?\<Phi> C M)"
 
   assume wt: "wt_jvm_prog_lbv P Cert"
   then have "wf_prog ?A P" by(simp add: wt_jvm_prog_lbv_def)
   moreover {
     fix wf_md C M b Ts Ca T m bd
-    assume "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
-           "set Ts \<subseteq> types P" and "bd = (M, b, Ts, T, m)" and
-           "?A P Ca bd"
-    then have "?B P Ca bd" using sees_method_is_class[OF sees]
-      by (auto dest!: start_context.wt_lbv_wt_method [OF start_context.intro] 
-               intro: someI)
+    
+    assume ass1: "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
+           ass2: "set Ts \<subseteq> types P" and ass3: "bd = (M, b, Ts, T, m)" and
+           ass4: "?A P Ca bd"
+    from ass3 ass4 have stab: "b = Static \<or> b = NonStatic" by (simp add:wt_lbv_def)        
+    from ass1 sees ass2 ass3 ass4 have "?B P Ca bd" using sees_method_is_class[OF sees] 
+      by (auto  dest!: start_context.wt_lbv_wt_method [OF start_context_intro_auxi[OF stab]]
+               intro: someI)  
   }
   ultimately have "wf_prog ?B P" by(rule wf_prog_lift)
   hence "wf_jvm_prog\<^bsub>?\<Phi>\<^esub> P" by (simp add: wf_jvm_prog_phi_def)
   thus ?thesis by (unfold wf_jvm_prog_def) blast
 qed
 (*>*)
 
 theorem jvm_lbv_complete:
   assumes wt: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P" 
   shows "wt_jvm_prog_lbv P (prg_cert P \<Phi>)"
 (*<*)
 proof -
   let ?cert = "prg_cert P \<Phi>"
   let ?A = "\<lambda>P C (M,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
                 wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)"
   let ?B = "\<lambda>P C (mn,b,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)).
                 wt_lbv P C b Ts T\<^sub>r mxs mxl\<^sub>0 et (?cert C mn) ins"
 
   from wt have "wf_prog ?A P" by(clarsimp simp: wf_jvm_prog_def wf_jvm_prog_phi_def)
   moreover {
     fix wf_md C M b Ts Ca T m bd
-    assume "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
-           "set Ts \<subseteq> types P" and "bd = (M, b, Ts, T, m)" and
-           "?A P Ca bd"
-    then have "?B P Ca bd" using sees_method_is_class[OF sees]
+    assume ass1: "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M, b :  Ts\<rightarrow>T = m in Ca" and
+           ass2: "set Ts \<subseteq> types P" and ass3: "bd = (M, b, Ts, T, m)" and
+           ass4: "?A P Ca bd"
+    from ass3 ass4 have stab: "b = Static \<or> b = NonStatic" by (simp add:wt_method_def)
+    from ass1 sees ass2 ass3 ass4 have "?B P Ca bd" using sees_method_is_class[OF sees]  
       by (auto simp add: prg_cert_def 
-               intro!: start_context.wt_method_wt_lbv start_context.intro)
+               intro!: start_context.wt_method_wt_lbv start_context_intro_auxi[OF stab])
   }
   ultimately have "wf_prog ?B P" by(rule wf_prog_lift)
   thus "wt_jvm_prog_lbv P (prg_cert P \<Phi>)" by (simp add: wt_jvm_prog_lbv_def)
 qed
 (*>*)
 
 end
diff --git a/thys/JinjaDCI/BV/SemiType.thy b/thys/JinjaDCI/BV/SemiType.thy
--- a/thys/JinjaDCI/BV/SemiType.thy
+++ b/thys/JinjaDCI/BV/SemiType.thy
@@ -1,280 +1,280 @@
 (*  Title:      Jinja/BV/SemiType.thy
 
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
 
 section \<open> The Jinja Type System as a Semilattice \<close>
 
 theory SemiType
 imports "../Common/WellForm" Jinja.Semilattices
 begin
 
 definition super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname"
 where "super P C \<equiv> fst (the (class P C))"
 
 lemma superI:
   "(C,D) \<in> subcls1 P \<Longrightarrow> super P C = D"
   by (unfold super_def) (auto dest: subcls1D)
 
 
 primrec the_Class :: "ty \<Rightarrow> cname"
 where
   "the_Class (Class C) = C"
 
 definition sup :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty err"
 where
   "sup P T\<^sub>1 T\<^sub>2 \<equiv>
   if is_refT T\<^sub>1 \<and> is_refT T\<^sub>2 then 
   OK (if T\<^sub>1 = NT then T\<^sub>2 else
       if T\<^sub>2 = NT then T\<^sub>1 else
       (Class (exec_lub (subcls1 P) (super P) (the_Class T\<^sub>1) (the_Class T\<^sub>2))))
   else 
   (if T\<^sub>1 = T\<^sub>2 then OK T\<^sub>1 else Err)"
 
 lemma sup_def':
   "sup P = (\<lambda>T\<^sub>1 T\<^sub>2.
   if is_refT T\<^sub>1 \<and> is_refT T\<^sub>2 then 
   OK (if T\<^sub>1 = NT then T\<^sub>2 else
       if T\<^sub>2 = NT then T\<^sub>1 else
       (Class (exec_lub (subcls1 P) (super P) (the_Class T\<^sub>1) (the_Class T\<^sub>2))))
   else 
   (if T\<^sub>1 = T\<^sub>2 then OK T\<^sub>1 else Err))"
   by (simp add: sup_def fun_eq_iff)
 
 abbreviation
   subtype :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   where "subtype P \<equiv> widen P"
 
 definition esl :: "'c prog \<Rightarrow> ty esl"
 where
   "esl P \<equiv> (types P, subtype P, sup P)"
 
 
 (* FIXME: move to wellform *)
 lemma is_class_is_subcls:
   "wf_prog m P \<Longrightarrow> is_class P C = P \<turnstile> C \<preceq>\<^sup>* Object"
 (*<*)by (fastforce simp:is_class_def
                   elim: subcls_C_Object converse_rtranclE subcls1I
                   dest: subcls1D)
 (*>*)
 
 
 (* FIXME: move to wellform *)
 lemma subcls_antisym:
   "\<lbrakk>wf_prog m P; P \<turnstile> C \<preceq>\<^sup>* D; P \<turnstile> D \<preceq>\<^sup>* C\<rbrakk> \<Longrightarrow> C = D"
   (*<*) by (auto dest: acyclic_subcls1 acyclic_impl_antisym_rtrancl antisymD) (*>*)
 
 (* FIXME: move to wellform *)
 lemma widen_antisym:
   "\<lbrakk> wf_prog m P; P \<turnstile> T \<le> U; P \<turnstile> U \<le> T \<rbrakk> \<Longrightarrow> T = U"
 (*<*)
 apply (cases T)
  apply (cases U)
  apply auto
 apply (cases U)
  apply (auto elim!: subcls_antisym)
 done
 (*>*)
 
 lemma order_widen [intro,simp]: 
-  "wf_prog m P \<Longrightarrow> order (subtype P)"
+  "wf_prog m P \<Longrightarrow> order (subtype P)  (types P)"
 (*<*)
   apply (unfold Semilat.order_def lesub_def)
   apply (auto intro: widen_trans widen_antisym)
   done
 (*>*)
 
 (* FIXME: move to TypeRel *)
 lemma NT_widen:
   "P \<turnstile> NT \<le> T = (T = NT \<or> (\<exists>C. T = Class C))"
 (*<*) by (cases T) auto (*>*)
 
 (* FIXME: move to TypeRel *)
 lemma Class_widen2: "P \<turnstile> Class C \<le> T = (\<exists>D. T = Class D \<and> P \<turnstile> C \<preceq>\<^sup>* D)"
 (*<*) by (cases T) auto (*>*)
  
 lemma wf_converse_subcls1_impl_acc_subtype:
   "wf ((subcls1 P)^-1) \<Longrightarrow> acc (subtype P)"
 (*<*)
 apply (unfold Semilat.acc_def lesssub_def)
 apply (drule_tac p = "(subcls1 P)^-1 - Id" in wf_subset)
  apply blast
 apply (drule wf_trancl)
 apply (simp add: wf_eq_minimal)
 apply clarify
 apply (unfold lesub_def)
 apply (rename_tac M T) 
 apply (case_tac "\<exists>C. Class C \<in> M")
  prefer 2
  apply (case_tac T)
      apply fastforce
     apply fastforce
    apply fastforce
   apply simp
   apply (rule_tac x = NT in bexI)
    apply (rule allI)
    apply (rule impI, erule conjE) 
    apply (clarsimp simp add: NT_widen)
   apply simp
  apply clarsimp
 apply (erule_tac x = "{C. Class C : M}" in allE)
 apply auto
 apply (rename_tac D)
 apply (rule_tac x = "Class D" in bexI)
  prefer 2
  apply assumption
 apply clarify
 apply (clarsimp simp: Class_widen2)
 apply (insert rtrancl_r_diff_Id [symmetric, of "subcls1 P"])
 apply simp
 apply (erule rtranclE)
  apply blast
 apply (drule rtrancl_converseI)
 apply (subgoal_tac "((subcls1 P)-Id)^-1 = ((subcls1 P)^-1 - Id)")
  prefer 2
  apply blast
 apply simp
 apply (blast intro: rtrancl_into_trancl2)
 done
 (*>*)
 
 lemma wf_subtype_acc [intro, simp]:
   "wf_prog wf_mb P \<Longrightarrow> acc (subtype P)"
 (*<*) by (rule wf_converse_subcls1_impl_acc_subtype, rule wf_subcls1) (*>*)
 
 lemma exec_lub_refl [simp]: "exec_lub r f T T = T"
 (*<*) by (simp add: exec_lub_def while_unfold) (*>*)
 
 lemma closed_err_types:
   "wf_prog wf_mb P \<Longrightarrow> closed (err (types P)) (lift2 (sup P))"
 (*<*)
   apply (unfold closed_def plussub_def lift2_def sup_def')
   apply (frule acyclic_subcls1)
   apply (frule single_valued_subcls1)
   apply (auto simp: is_type_def is_refT_def is_class_is_subcls split: err.split ty.splits)
   apply (blast dest!: is_lub_exec_lub is_lubD is_ubD intro!: is_ubI superI)
   done
 (*>*)
 
 
 lemma sup_subtype_greater:
   "\<lbrakk> wf_prog wf_mb P; is_type P t1; is_type P t2; sup P t1 t2 = OK s \<rbrakk> 
   \<Longrightarrow> subtype P t1 s \<and> subtype P t2 s"
 (*<*)
 proof -
   assume wf_prog: "wf_prog wf_mb P"
  
   { fix c1 c2
     assume is_class: "is_class P c1" "is_class P c2"
     with wf_prog 
     obtain 
       "P \<turnstile> c1 \<preceq>\<^sup>* Object"
       "P \<turnstile> c2 \<preceq>\<^sup>* Object"
       by (blast intro: subcls_C_Object)
     with single_valued_subcls1[OF wf_prog]
     obtain u where
       "is_lub ((subcls1 P)^* ) c1 c2 u"      
       by (blast dest: single_valued_has_lubs)
     moreover
     note acyclic_subcls1[OF wf_prog]
     moreover
     have "\<forall>x y. (x, y) \<in> subcls1 P \<longrightarrow> super P x = y"
       by (blast intro: superI)
     ultimately
     have "P \<turnstile> c1 \<preceq>\<^sup>* exec_lub (subcls1 P) (super P) c1 c2 \<and>
           P \<turnstile> c2 \<preceq>\<^sup>* exec_lub (subcls1 P) (super P) c1 c2"
       by (simp add: exec_lub_conv) (blast dest: is_lubD is_ubD)
   } note this [simp]
 
   assume "is_type P t1" "is_type P t2" "sup P t1 t2 = OK s"
   thus ?thesis
     apply (unfold sup_def) 
     apply (cases s)
     apply (auto simp add: is_refT_def split: if_split_asm)
     done
 qed
 (*>*)
 
 lemma sup_subtype_smallest:
   "\<lbrakk> wf_prog wf_mb P; is_type P a; is_type P b; is_type P c; 
       subtype P a c; subtype P b c; sup P a b = OK d \<rbrakk>
   \<Longrightarrow> subtype P d c"
 (*<*)
 proof -
   assume wf_prog: "wf_prog wf_mb P"
 
   { fix c1 c2 D
     assume is_class: "is_class P c1" "is_class P c2"
     assume le: "P \<turnstile> c1 \<preceq>\<^sup>* D" "P \<turnstile> c2 \<preceq>\<^sup>* D"
     from wf_prog is_class
     obtain 
       "P \<turnstile> c1 \<preceq>\<^sup>* Object"
       "P \<turnstile> c2 \<preceq>\<^sup>* Object"
       by (blast intro: subcls_C_Object)
     with single_valued_subcls1[OF wf_prog]
     obtain u where
       lub: "is_lub ((subcls1 P)^* ) c1 c2 u"
       by (blast dest: single_valued_has_lubs)   
     with acyclic_subcls1[OF wf_prog]
     have "exec_lub (subcls1 P) (super P) c1 c2 = u"
       by (blast intro: superI exec_lub_conv)
     moreover
     from lub le
     have "P \<turnstile> u \<preceq>\<^sup>* D" 
       by (simp add: is_lub_def is_ub_def)
     ultimately     
     have "P \<turnstile> exec_lub (subcls1 P) (super P) c1 c2 \<preceq>\<^sup>* D"
       by blast
   } note this [intro]
 
   have [dest!]:
     "\<And>C T. P \<turnstile> Class C \<le> T \<Longrightarrow> \<exists>D. T=Class D \<and> P \<turnstile> C \<preceq>\<^sup>* D"
     by (frule Class_widen, auto)
 
   assume "is_type P a" "is_type P b" "is_type P c"
          "subtype P a c" "subtype P b c" "sup P a b = OK d"
   thus ?thesis
     by (auto simp add: sup_def is_refT_def
              split: if_split_asm)
 qed
 (*>*)
 
 lemma sup_exists:
   "\<lbrakk> subtype P a c; subtype P b c \<rbrakk> \<Longrightarrow> \<exists>T. sup P a b = OK T"
 (*<*)
 apply (unfold sup_def)
 apply (cases b)
 apply auto
 apply (cases a)
 apply auto
 apply (cases a)
 apply auto
 done
 (*>*)
 
 lemma err_semilat_JType_esl:
   "wf_prog wf_mb P \<Longrightarrow> err_semilat (esl P)"
 (*<*)
 proof -
   assume wf_prog: "wf_prog wf_mb P"  
-  hence "order (subtype P)"..
+  hence "order (subtype P) (types P)"..
   moreover from wf_prog
   have "closed (err (types P)) (lift2 (sup P))"
     by (rule closed_err_types)
   moreover
   from wf_prog have
     "(\<forall>x\<in>err (types P). \<forall>y\<in>err (types P). x \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> x \<squnion>\<^bsub>lift2 (sup P)\<^esub> y) \<and> 
      (\<forall>x\<in>err (types P). \<forall>y\<in>err (types P). y \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> x \<squnion>\<^bsub>lift2 (sup P)\<^esub> y)"
     by (auto simp add: lesub_def plussub_def Err.le_def lift2_def sup_subtype_greater split: err.split)
   moreover from wf_prog have
     "\<forall>x\<in>err (types P). \<forall>y\<in>err (types P). \<forall>z\<in>err (types P). 
     x \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> z \<longrightarrow> x \<squnion>\<^bsub>lift2 (sup P)\<^esub> y \<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub> z"
     by (unfold lift2_def plussub_def lesub_def Err.le_def)
        (auto intro: sup_subtype_smallest dest:sup_exists split: err.split)
   ultimately show ?thesis by (simp add: esl_def semilat_def sl_def Err.sl_def)
 qed
 (*>*)
 
 
 end
diff --git a/thys/JinjaDCI/BV/TF_JVM.thy b/thys/JinjaDCI/BV/TF_JVM.thy
--- a/thys/JinjaDCI/BV/TF_JVM.thy
+++ b/thys/JinjaDCI/BV/TF_JVM.thy
@@ -1,319 +1,355 @@
 (*  Title:      JinjaDCI/BV/TF_JVM.thy
 
     Author:     Tobias Nipkow, Gerwin Klein, Susannah Mansky
     Copyright   2000 TUM, 2019-20 UIUC
 
     Based on the Jinja theory BV/TF_JVM.thy by Tobias Nipkow and Gerwin Klein
 *)
 
 section \<open> The Typing Framework for the JVM \label{sec:JVM} \<close>
 
 theory TF_JVM
 imports Jinja.Typing_Framework_err EffectMono BVSpec
 begin
 
 definition exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> ex_table \<Rightarrow> instr list \<Rightarrow> ty\<^sub>i' err step_type"
 where 
   "exec G maxs rT et bs \<equiv>
   err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc (size bs) et) 
                      (\<lambda>pc. eff (bs!pc) G pc et)"
 
 locale JVM_sl =
-  fixes P :: jvm_prog and mxs and mxl\<^sub>0
+  fixes P :: jvm_prog and mxs and mxl\<^sub>0 and n
   fixes b and Ts :: "ty list" and "is" and xt and T\<^sub>r
 
   fixes mxl and A and r and f and app and eff and step
   defines [simp]: "mxl \<equiv> (case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1)+size Ts+mxl\<^sub>0"
   defines [simp]: "A   \<equiv> states P mxs mxl"
   defines [simp]: "r   \<equiv> JVM_SemiType.le P mxs mxl"
   defines [simp]: "f   \<equiv> JVM_SemiType.sup P mxs mxl"
 
   defines [simp]: "app \<equiv> \<lambda>pc. Effect.app (is!pc) P mxs T\<^sub>r pc (size is) xt"
   defines [simp]: "eff \<equiv> \<lambda>pc. Effect.eff (is!pc) P pc xt"
   defines [simp]: "step \<equiv> err_step (size is) app eff"
 
+  defines [simp]: "n \<equiv> size is"
+  assumes staticb: "b = Static \<or> b = NonStatic" 
 
 locale start_context = JVM_sl +
   fixes p and C
+
   assumes wf: "wf_prog p P"
   assumes C:  "is_class P C"
   assumes Ts: "set Ts \<subseteq> types P"
 
+ 
   fixes first :: ty\<^sub>i' and start
   defines [simp]: 
   "first \<equiv> Some ([],(case b of Static \<Rightarrow> [] | NonStatic \<Rightarrow> [OK (Class C)]) @ map OK Ts @ replicate mxl\<^sub>0 Err)"
   defines [simp]:
   "start \<equiv> (OK first) #  replicate (size is - 1) (OK None)"
+thm start_context.intro
 
-
+lemma start_context_intro_auxi: 
+  fixes  P b Ts p C
+  assumes "b = Static \<or> b = NonStatic " 
+      and "wf_prog p P"
+      and "is_class P C"
+      and "set Ts \<subseteq> types P"
+    shows " start_context P b Ts p C"
+  using start_context.intro[OF JVM_sl.intro] start_context_axioms_def assms  by auto
 
 subsection \<open> Connecting JVM and Framework \<close>
 
+lemma (in start_context) semi: "semilat (A, r, f)"
+  apply (insert semilat_JVM[OF wf])
+  apply (unfold A_def r_def f_def JVM_SemiType.le_def JVM_SemiType.sup_def states_def)
+  apply auto
+  done
+
 
 lemma (in JVM_sl) step_def_exec: "step \<equiv> exec P mxs T\<^sub>r xt is" 
   by (simp add: exec_def)  
 
 lemma special_ex_swap_lemma [iff]: 
   "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"
   by blast
 
 lemma ex_in_list [iff]:
   "(\<exists>n. ST \<in> list n A \<and> n \<le> mxs) = (set ST \<subseteq> A \<and> size ST \<le> mxs)"
   by (unfold list_def) auto
 
 lemma singleton_list: 
   "(\<exists>n. [Class C] \<in> list n (types P) \<and> n \<le> mxs) = (is_class P C \<and> 0 < mxs)"
   by auto
 
 lemma set_drop_subset:
   "set xs \<subseteq> A \<Longrightarrow> set (drop n xs) \<subseteq> A"
   by (auto dest: in_set_dropD)
 
 lemma Suc_minus_minus_le:
   "n < mxs \<Longrightarrow> Suc (n - (n - b)) \<le> mxs"
   by arith
 
 lemma in_listE:
   "\<lbrakk> xs \<in> list n A; \<lbrakk>size xs = n; set xs \<subseteq> A\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   by (unfold list_def) blast
 
 declare is_relevant_entry_def [simp]
 declare set_drop_subset [simp]
 
 theorem (in start_context) exec_pres_type:
   "pres_type step (size is) A"
 (*<*)
 proof -
   let ?n = "size is" and ?app = app and ?step = eff
   let ?mxl = "(case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1) + length Ts + mxl\<^sub>0"
   let ?A = "opt((Union {list n (types P) |n. n <= mxs}) \<times>
                                  list ?mxl (err(types P)))"
   have "pres_type (err_step ?n ?app ?step) ?n (err ?A)"
   proof(rule pres_type_lift)
     have "\<And>s pc pc' s'. s\<in>?A \<Longrightarrow> pc < ?n \<Longrightarrow> ?app pc s
              \<Longrightarrow> (pc', s')\<in>set (?step pc s) \<Longrightarrow> s' \<in> ?A"
     proof -
       fix s pc pc' s'
       assume asms: "s\<in>?A" "pc < ?n" "?app pc s" "(pc', s')\<in>set (?step pc s)"
       show "s' \<in> ?A"
       proof(cases s)
         case None
         then show ?thesis using asms by (fastforce dest: effNone)
       next
         case (Some ab)
         then show ?thesis using asms proof(cases "is!pc")
           case Load
           then show ?thesis using asms
             by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def  
                                 xcpt_eff_def norm_eff_def
                           dest: listE_nth_in)
         next
           case Push
           then show ?thesis using asms Some
             by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
                                 xcpt_eff_def norm_eff_def typeof_lit_is_type)
         next
           case Getfield
           then show ?thesis using asms wf
             by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
                                 xcpt_eff_def norm_eff_def
                           dest: sees_field_is_type)
         next
           case Getstatic
           then show ?thesis using asms wf
             by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def
                                 xcpt_eff_def norm_eff_def
                           dest: sees_field_is_type)
         next
           case (Invoke M n)
           obtain a b where [simp]: "s = \<lfloor>(a,b)\<rfloor>" using Some asms(1) by blast
           show ?thesis
           proof(cases "a!n = NT")
             case True
             then show ?thesis using Invoke asms wf
               by (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def  
                                   xcpt_eff_def norm_eff_def)
           next
             case False
             have "(pc', s') \<in> set (norm_eff (Invoke M n) P pc (a, b)) \<or>
               (pc', s') \<in> set (xcpt_eff (Invoke M n) P pc (a, b) xt)"
               using Invoke asms(4) by (simp add: Effect.eff_def)
             then show ?thesis proof(rule disjE)
               assume "(pc', s') \<in> set (xcpt_eff (Invoke M n) P pc (a, b) xt)"
               then show ?thesis using Invoke asms(1-3)
                 by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def)
             next
               assume norm: "(pc', s') \<in> set (norm_eff (Invoke M n) P pc (a, b))"
               also have "Suc (length a - Suc n) \<le> mxs" using Invoke asms(1,3)
                 by (simp add: Effect.app_def xcpt_app_def) arith
               ultimately show ?thesis using False Invoke asms(1-3) wf
                 by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def
                          dest!: sees_wf_mdecl)
             qed
           qed
         next
           case (Invokestatic C M n)
           obtain a b where [simp]: "s = \<lfloor>(a,b)\<rfloor>" using Some asms(1) by blast
           have "(pc', s') \<in> set (norm_eff (Invokestatic C M n) P pc (a, b)) \<or>
             (pc', s') \<in> set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)"
             using Invokestatic asms(4) by (simp add: Effect.eff_def)
           then show ?thesis proof(rule disjE)
             assume "(pc', s') \<in> set (xcpt_eff (Invokestatic C M n) P pc (a, b) xt)"
             then show ?thesis using Invokestatic asms(1-3)
               by (fastforce simp: Effect.app_def xcpt_app_def xcpt_eff_def)
           next
             assume norm: "(pc', s') \<in> set (norm_eff (Invokestatic C M n) P pc (a, b))"
             also have "Suc (length a - Suc n) \<le> mxs" using Invokestatic asms(1,3)
               by (simp add: Effect.app_def xcpt_app_def) arith
             ultimately show ?thesis using Invokestatic asms(1-3) wf
               by (auto simp: Effect.app_def xcpt_app_def norm_eff_def wf_mdecl_def
                        dest!: sees_wf_mdecl)
           qed
         qed (fastforce simp: Effect.app_def xcpt_app_def Effect.eff_def  
                              xcpt_eff_def norm_eff_def)+
       qed
     qed
     then show "\<forall>s\<in>?A. \<forall>p. p < ?n \<longrightarrow> ?app p s \<longrightarrow> (\<forall>(q, s')\<in>set (?step p s). s' \<in> ?A)"
       by clarsimp
   qed
   then show ?thesis by (simp add: JVM_states_unfold)
 qed
 (*>*)
 
 declare is_relevant_entry_def [simp del]
 declare set_drop_subset [simp del]
 
 lemma lesubstep_type_simple:
   "xs [\<sqsubseteq>\<^bsub>Product.le (=) r\<^esub>] ys \<Longrightarrow> set xs {\<sqsubseteq>\<^bsub>r\<^esub>} set ys"
 (*<*)
 proof -
   assume assm: "xs [\<sqsubseteq>\<^bsub>Product.le (=) r\<^esub>] ys"
   have "\<And>a b i y. (a, b) = xs ! i \<Longrightarrow> i < length xs
      \<Longrightarrow> \<exists>\<tau>'. (\<exists>i. (a, \<tau>') = ys ! i \<and> i < length xs) \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>'"
   proof -
     fix a b i assume ith: "(a, b) = xs ! i" and len: "i < length xs"
     obtain \<tau> where "ys ! i = (a, \<tau>) \<and> r b \<tau>"
       using le_listD[OF assm len] ith
       by (clarsimp simp: lesub_def Product.le_def)
     then have "(a, \<tau>) = ys ! i \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>"
       by (clarsimp simp: lesub_def)
     with len show "\<exists>\<tau>'. (\<exists>i. (a, \<tau>') = ys ! i \<and> i < length xs) \<and> b \<sqsubseteq>\<^bsub>r\<^esub> \<tau>'"
       by fastforce
   qed
   then show "set xs {\<sqsubseteq>\<^bsub>r\<^esub>} set ys" using assm
     by (clarsimp simp: lesubstep_type_def set_conv_nth)
 qed
 (*>*)
 
 declare is_relevant_entry_def [simp del]
 
 
 lemma conjI2: "\<lbrakk> A; A \<Longrightarrow> B \<rbrakk> \<Longrightarrow> A \<and> B" by blast
   
 lemma (in JVM_sl) eff_mono:
 assumes wf: "wf_prog p P" and "pc < length is" and
   lesub: "s \<sqsubseteq>\<^bsub>sup_state_opt P\<^esub> t" and app: "app pc t"
 shows "set (eff pc s) {\<sqsubseteq>\<^bsub>sup_state_opt P\<^esub>} set (eff pc t)"
 (*<*)
 proof(cases t)
   case None then show ?thesis using lesub
    by (simp add: Effect.eff_def lesub_def)
 next
   case tSome: (Some a)
   show ?thesis proof(cases s)
     case None then show ?thesis using lesub
      by (simp add: Effect.eff_def lesub_def)
   next
     case (Some b)
     let ?norm = "\<lambda>x. norm_eff (is ! pc) P pc x"
     let ?xcpt = "\<lambda>x. xcpt_eff (is ! pc) P pc x xt"
     let ?r = "Product.le (=) (sup_state_opt P)"
     let ?\<tau>' = "\<lfloor>eff\<^sub>i (is ! pc, P, a)\<rfloor>"
     {
       fix x assume xb: "x \<in> set (succs (is ! pc) b pc)"
       then have appi: "app\<^sub>i (is ! pc, P, pc, mxs, T\<^sub>r, a)" and
                 bia: "P \<turnstile> b \<le>\<^sub>i a" and appa: "app pc \<lfloor>a\<rfloor>"
         using lesub app tSome Some by (auto simp add: lesub_def Effect.app_def)
       have xa: "x \<in> set (succs (is ! pc) a pc)"
         using xb succs_mono[OF wf appi bia] by auto
       then have "(x, ?\<tau>') \<in> (\<lambda>pc'. (pc', ?\<tau>')) ` set (succs (is ! pc) a pc)"
         by (rule imageI)
       moreover have "P \<turnstile> \<lfloor>eff\<^sub>i (is ! pc, P, b)\<rfloor> \<le>' ?\<tau>'"
         using xb xa eff\<^sub>i_mono[OF wf bia] appa by fastforce
       ultimately have "\<exists>\<tau>'. (x, \<tau>') \<in> (\<lambda>pc'. (pc', \<lfloor>eff\<^sub>i (is ! pc, P, a)\<rfloor>)) ` set (succs (is ! pc) a pc) \<and>
               P \<turnstile> \<lfloor>eff\<^sub>i (is ! pc, P, b)\<rfloor> \<le>' \<tau>'" by blast
     }
     then have norm: "set (?norm b) {\<sqsubseteq>\<^bsub>sup_state_opt P\<^esub>} set (?norm a)"
       using tSome Some by (clarsimp simp: norm_eff_def lesubstep_type_def lesub_def)
     obtain a1 b1 a2 b2 where a: "a = (a1, b1)" and b: "b = (a2, b2)"
       using tSome Some by fastforce
     then have a12: "size a2 = size a1" using lesub tSome Some
       by (clarsimp simp: lesub_def list_all2_lengthD)
     have "length (?xcpt b) = length (?xcpt a)"
       by (simp add: xcpt_eff_def split_beta)
     moreover have "\<And>n. n < length (?xcpt b) \<Longrightarrow> (?xcpt b) ! n \<sqsubseteq>\<^bsub>?r\<^esub> (?xcpt a) ! n"
       using lesub tSome Some a b a12
       by (simp add: xcpt_eff_def split_beta fun_of_def) (simp add: lesub_def)
     ultimately have "?xcpt b [\<sqsubseteq>\<^bsub>?r\<^esub>] ?xcpt a"
       by(rule le_listI)
     then have "set (?xcpt b) {\<sqsubseteq>\<^bsub>sup_state_opt P\<^esub>} set (?xcpt a)"
       by (rule lesubstep_type_simple)
     moreover note norm
     ultimately have
      "set (?norm b) \<union> set (?xcpt b) {\<sqsubseteq>\<^bsub>sup_state_opt P\<^esub>} set (?norm a) \<union> set (?xcpt a)"
       by(intro lesubstep_union)
     then show ?thesis using tSome Some by(simp add: Effect.eff_def)
   qed
 qed
 (*>*)
 
 lemma (in JVM_sl) bounded_step: "bounded step (size is)"
 (*<*)
   by (auto simp: bounded_def err_step_def Effect.app_def Effect.eff_def
                  error_def map_snd_def
           split: err.splits option.splits)
 (*>*)
 
 theorem (in JVM_sl) step_mono:
   "wf_prog wf_mb P \<Longrightarrow> mono r step (size is) A"
 (*<*)
+ apply (simp add: JVM_le_Err_conv)  
+  apply (insert bounded_step)
+  apply (unfold JVM_states_unfold)
+  apply (rule mono_lift)    
+  apply (subgoal_tac "b = Static \<or> b = NonStatic") 
+      apply (fastforce split:if_splits)\<comment>\<open> order_sup_state_opt' order_sup_state_opt'' \<close>
+     apply (simp only:staticb)
+     apply (unfold app_mono_def lesub_def)
+    apply clarsimp
+    apply (erule (2) app_mono)
+   apply simp
+  apply clarify
+  apply (drule eff_mono)
+      apply (auto simp add: lesub_def)
+  done
+(*
 proof -
   assume wf: "wf_prog wf_mb P"
   let ?r = "sup_state_opt P" and ?n = "length is" and ?app = app and ?step = eff
   let ?A = "opt (\<Union> {list n (types P) |n. n \<le> mxs} \<times>
                 list ((case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1) + length Ts + mxl\<^sub>0)
                  (err (types P)))"
-  have "order ?r" using wf by simp
+  have "order ?r ?A" using wf by simp
   moreover have "app_mono ?r ?app ?n ?A" using app_mono[OF wf]
     by (clarsimp simp: app_mono_def lesub_def)
   moreover have "bounded (err_step ?n ?app ?step) ?n" using bounded_step
     by simp
   moreover have "\<forall>s p t. s \<in> ?A \<and> p < ?n \<and> s \<sqsubseteq>\<^bsub>?r\<^esub> t \<longrightarrow>
    ?app p t \<longrightarrow> set (?step p s) {\<sqsubseteq>\<^bsub>?r\<^esub>} set (?step p t)"
      using eff_mono[OF wf] by simp
   ultimately have "mono (Err.le ?r) (err_step ?n ?app ?step) ?n (err ?A)"
     by(rule mono_lift)
   then show "mono r step (size is) A" using bounded_step
     by (simp add: JVM_le_Err_conv JVM_states_unfold)
 qed
+*)
 (*>*)
 
 
 lemma (in start_context) first_in_A [iff]: "OK first \<in> A"
   using Ts C by (cases b; force intro!: list_appendI simp add: JVM_states_unfold)
 
 
 lemma (in JVM_sl) wt_method_def2:
   "wt_method P C' b Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s =
   (is \<noteq> [] \<and> 
+   (b = Static \<or> b = NonStatic) \<and>
    size \<tau>s = size is \<and>
    OK ` set \<tau>s \<subseteq> states P mxs mxl \<and>
    wt_start P C' b Ts mxl\<^sub>0 \<tau>s \<and> 
    wt_app_eff (sup_state_opt P) app eff \<tau>s)"
-(*<*)
+(*<*)using staticb
   by (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def
              check_types_def) auto
 (*>*)
 
 
 end
diff --git a/thys/JinjaDCI/Compiler/TypeComp.thy b/thys/JinjaDCI/Compiler/TypeComp.thy
--- a/thys/JinjaDCI/Compiler/TypeComp.thy
+++ b/thys/JinjaDCI/Compiler/TypeComp.thy
@@ -1,1619 +1,1686 @@
 (*  Title:      JinjaDCI/Compiler/TypeComp.thy
 
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   TUM 2003, UIUC 2019-20
 
     Based on the Jinja theory Compiler/TypeComp.thy by Tobias Nipkow
 *)
 
 section \<open> Preservation of Well-Typedness \<close>
 
 theory TypeComp
 imports Compiler "../BV/BVSpec"
 begin
 
 (*<*)
 declare nth_append[simp]
 (*>*)
 
 lemma max_stack1: "P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> 1 \<le> max_stack e"
 (*<*)using max_stack1'[OF WT\<^sub>1_nsub_RI] by simp(*>*)
 
 locale TC0 =
   fixes P :: "J\<^sub>1_prog" and mxl :: nat
 begin
 
 definition "ty E e = (THE T. P,E \<turnstile>\<^sub>1 e :: T)"
 
 definition "ty\<^sub>l E A' = map (\<lambda>i. if i \<in> A' \<and> i < size E then OK(E!i) else Err) [0..<mxl]"
 
 definition "ty\<^sub>i' ST E A = (case A of None \<Rightarrow> None | \<lfloor>A'\<rfloor> \<Rightarrow> Some(ST, ty\<^sub>l E A'))"
 
 definition "after E A ST e = ty\<^sub>i' (ty E e # ST) E (A \<squnion> \<A> e)"
 
 end
 
 lemma (in TC0) ty_def2 [simp]: "P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> ty E e = T"
 (*<*)by(unfold ty_def) (blast intro: the_equality WT\<^sub>1_unique)(*>*)
 
 lemma (in TC0) [simp]: "ty\<^sub>i' ST E None = None"
 (*<*)by (simp add: ty\<^sub>i'_def)(*>*)
 
 lemma (in TC0) ty\<^sub>l_app_diff[simp]:
  "ty\<^sub>l (E@[T]) (A - {size E}) = ty\<^sub>l E A"
 (*<*)by(auto simp add:ty\<^sub>l_def hyperset_defs)(*>*)
 
 
 lemma (in TC0) ty\<^sub>i'_app_diff[simp]:
  "ty\<^sub>i' ST (E @ [T]) (A \<ominus> size E) = ty\<^sub>i' ST E A"
 (*<*)by(auto simp add:ty\<^sub>i'_def hyperset_defs)(*>*)
 
 
 lemma (in TC0) ty\<^sub>l_antimono:
  "A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>l E A' [\<le>\<^sub>\<top>] ty\<^sub>l E A"
 (*<*)by(auto simp:ty\<^sub>l_def list_all2_conv_all_nth)(*>*)
 
 
 lemma (in TC0) ty\<^sub>i'_antimono:
  "A \<subseteq> A' \<Longrightarrow> P \<turnstile> ty\<^sub>i' ST E \<lfloor>A'\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
 (*<*)by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)(*>*)
 
 
 lemma (in TC0) ty\<^sub>l_env_antimono:
  "P \<turnstile> ty\<^sub>l (E@[T]) A [\<le>\<^sub>\<top>] ty\<^sub>l E A" 
 (*<*)by(auto simp:ty\<^sub>l_def list_all2_conv_all_nth)(*>*)
 
 
 lemma (in TC0) ty\<^sub>i'_env_antimono:
  "P \<turnstile> ty\<^sub>i' ST (E@[T]) A \<le>' ty\<^sub>i' ST E A" 
 (*<*)by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)(*>*)
 
 
 lemma (in TC0) ty\<^sub>i'_incr:
  "P \<turnstile> ty\<^sub>i' ST (E @ [T]) \<lfloor>insert (size E) A\<rfloor> \<le>' ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
 (*<*)by(auto simp:ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth)(*>*)
 
 
 lemma (in TC0) ty\<^sub>l_incr:
  "P \<turnstile> ty\<^sub>l (E @ [T]) (insert (size E) A) [\<le>\<^sub>\<top>] ty\<^sub>l E A"
 (*<*)by(auto simp: hyperset_defs ty\<^sub>l_def list_all2_conv_all_nth)(*>*)
 
 
 lemma (in TC0) ty\<^sub>l_in_types:
  "set E \<subseteq> types P \<Longrightarrow> ty\<^sub>l E A \<in> list mxl (err (types P))"
 (*<*)by(auto simp add:ty\<^sub>l_def intro!:listI dest!: nth_mem)(*>*)
 
 locale TC1 = TC0
 begin
 
 primrec compT :: "ty list \<Rightarrow> nat hyperset \<Rightarrow> ty list \<Rightarrow> expr\<^sub>1 \<Rightarrow> ty\<^sub>i' list" and
    compTs :: "ty list \<Rightarrow> nat hyperset \<Rightarrow> ty list \<Rightarrow> expr\<^sub>1 list \<Rightarrow> ty\<^sub>i' list" where
 "compT E A ST (new C) = []"
 | "compT E A ST (Cast C e) =  
    compT E A ST e @ [after E A ST e]"
 | "compT E A ST (Val v) = []"
 | "compT E A ST (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) =
   (let ST\<^sub>1 = ty E e\<^sub>1#ST; A\<^sub>1 = A \<squnion> \<A> e\<^sub>1 in
    compT E A ST e\<^sub>1 @ [after E A ST e\<^sub>1] @
    compT E A\<^sub>1 ST\<^sub>1 e\<^sub>2 @ [after E A\<^sub>1 ST\<^sub>1 e\<^sub>2])"
 | "compT E A ST (Var i) = []"
 | "compT E A ST (i := e) = compT E A ST e @
    [after E A ST e, ty\<^sub>i' ST E (A \<squnion> \<A> e \<squnion> \<lfloor>{i}\<rfloor>)]"
 | "compT E A ST (e\<bullet>F{D}) = 
    compT E A ST e @ [after E A ST e]"
 | "compT E A ST (C\<bullet>\<^sub>sF{D}) = []"
 | "compT E A ST (e\<^sub>1\<bullet>F{D} := e\<^sub>2) =
   (let ST\<^sub>1 = ty   E e\<^sub>1#ST; A\<^sub>1 = A \<squnion> \<A> e\<^sub>1; A\<^sub>2 = A\<^sub>1 \<squnion> \<A> e\<^sub>2 in
    compT E A ST e\<^sub>1 @ [after E A ST e\<^sub>1] @
    compT E A\<^sub>1 ST\<^sub>1 e\<^sub>2 @ [after E A\<^sub>1 ST\<^sub>1 e\<^sub>2] @
    [ty\<^sub>i' ST E A\<^sub>2])"
 | "compT E A ST (C\<bullet>\<^sub>sF{D} := e\<^sub>2) = compT E A ST e\<^sub>2 @ [after E A ST e\<^sub>2] @ [ty\<^sub>i' ST E (A \<squnion> \<A> e\<^sub>2)]"
 | "compT E A ST {i:T; e} = compT (E@[T]) (A\<ominus>i) ST e"
 | "compT E A ST (e\<^sub>1;;e\<^sub>2) =
   (let A\<^sub>1 = A \<squnion> \<A> e\<^sub>1 in
    compT E A ST e\<^sub>1 @ [after E A ST e\<^sub>1, ty\<^sub>i' ST E A\<^sub>1] @
    compT E A\<^sub>1 ST e\<^sub>2)"
 | "compT E A ST (if (e) e\<^sub>1 else e\<^sub>2) =
    (let A\<^sub>0 = A \<squnion> \<A> e; \<tau> = ty\<^sub>i' ST E A\<^sub>0 in
     compT E A ST e @ [after E A ST e, \<tau>] @
     compT E A\<^sub>0 ST e\<^sub>1 @ [after E A\<^sub>0 ST e\<^sub>1, \<tau>] @
     compT E A\<^sub>0 ST e\<^sub>2)"
 | "compT E A ST (while (e) c) =
    (let A\<^sub>0 = A \<squnion> \<A> e;  A\<^sub>1 = A\<^sub>0 \<squnion> \<A> c; \<tau> = ty\<^sub>i' ST E A\<^sub>0 in
     compT E A ST e @ [after E A ST e, \<tau>] @
     compT E A\<^sub>0 ST c @ [after E A\<^sub>0 ST c, ty\<^sub>i' ST E A\<^sub>1, ty\<^sub>i' ST E A\<^sub>0])"
 | "compT E A ST (throw e) = compT E A ST e @ [after E A ST e]"
 | "compT E A ST (e\<bullet>M(es)) =
    compT E A ST e @ [after E A ST e] @
    compTs E (A \<squnion> \<A> e) (ty   E e # ST) es"
 | "compT E A ST (C\<bullet>\<^sub>sM(es)) = compTs E A ST es"
 | "compT E A ST (try e\<^sub>1 catch(C i) e\<^sub>2) =
    compT E A ST e\<^sub>1 @ [after E A ST e\<^sub>1] @
    [ty\<^sub>i' (Class C#ST) E A, ty\<^sub>i' ST (E@[Class C]) (A \<squnion> \<lfloor>{i}\<rfloor>)] @
    compT (E@[Class C]) (A \<squnion> \<lfloor>{i}\<rfloor>) ST e\<^sub>2"
 | "compT E A ST (INIT C (Cs,b) \<leftarrow> e) = []"
 | "compT E A ST (RI(C,e');Cs \<leftarrow> e) = []"
 | "compTs E A ST [] = []"
 | "compTs  E A ST (e#es) = compT E A ST e @ [after E A ST e] @
                             compTs E (A \<squnion> (\<A> e)) (ty E e # ST) es"
 
 definition compT\<^sub>a :: "ty list \<Rightarrow> nat hyperset \<Rightarrow> ty list \<Rightarrow> expr\<^sub>1 \<Rightarrow> ty\<^sub>i' list" where
   "compT\<^sub>a E A ST e = compT E A ST e @ [after E A ST e]"
 
 end
 
 lemma compE\<^sub>2_not_Nil[simp]: "P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> compE\<^sub>2 e \<noteq> []"
 (*<*)by(simp add: compE\<^sub>2_not_Nil' WT\<^sub>1_nsub_RI)(*>*)
 
 lemma (in TC1) compT_sizes':
 shows "\<And>E A ST. \<not>sub_RI e \<Longrightarrow> size(compT E A ST e) = size(compE\<^sub>2 e) - 1"
 and "\<And>E A ST. \<not>sub_RIs es \<Longrightarrow> size(compTs E A ST es) = size(compEs\<^sub>2 es)"
 (*<*)
 by(induct e and es rule: compE\<^sub>2.induct compEs\<^sub>2.induct)
   (auto split:bop.splits nat_diff_split simp: compE\<^sub>2_not_Nil')
 (*>*)
 
 lemma (in TC1) compT_sizes[simp]:
 shows "\<And>E A ST. P,E \<turnstile>\<^sub>1 e :: T \<Longrightarrow> size(compT E A ST e) = size(compE\<^sub>2 e) - 1"
 and "\<And>E A ST. P,E \<turnstile>\<^sub>1 es [::] Ts \<Longrightarrow> size(compTs E A ST es) = size(compEs\<^sub>2 es)"
 (*<*)using compT_sizes' WT\<^sub>1_nsub_RI WTs\<^sub>1_nsub_RIs by auto(*>*)
 
 
 lemma (in TC1) [simp]: "\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compT E None ST e)"
 and [simp]: "\<And>ST E. \<lfloor>\<tau>\<rfloor> \<notin> set (compTs E None ST es)"
 (*<*)by(induct e and es rule: compT.induct compTs.induct) (simp_all add:after_def)(*>*)
 
 
 lemma (in TC0) pair_eq_ty\<^sub>i'_conv:
   "(\<lfloor>(ST, LT)\<rfloor> = ty\<^sub>i' ST\<^sub>0 E A) =
   (case A of None \<Rightarrow> False | Some A \<Rightarrow> (ST = ST\<^sub>0 \<and> LT = ty\<^sub>l E A))"
 (*<*)by(simp add:ty\<^sub>i'_def)(*>*)
 
 
 lemma (in TC0) pair_conv_ty\<^sub>i':
   "\<lfloor>(ST, ty\<^sub>l E A)\<rfloor> = ty\<^sub>i' ST E \<lfloor>A\<rfloor>"
 (*<*)by(simp add:ty\<^sub>i'_def)(*>*)
 
 (*<*)
 declare (in TC0)
   ty\<^sub>i'_antimono [intro!] after_def[simp]
   pair_conv_ty\<^sub>i'[simp] pair_eq_ty\<^sub>i'_conv[simp]
 (*>*)
 
 
 lemma (in TC1) compT_LT_prefix:
  "\<And>E A ST\<^sub>0. \<lbrakk> \<lfloor>(ST,LT)\<rfloor> \<in> set(compT E A ST\<^sub>0 e); \<B> e (size E) \<rbrakk>
                \<Longrightarrow> P \<turnstile> \<lfloor>(ST,LT)\<rfloor> \<le>' ty\<^sub>i' ST E A"
 and
  "\<And>E A ST\<^sub>0. \<lbrakk> \<lfloor>(ST,LT)\<rfloor> \<in> set(compTs E A ST\<^sub>0 es); \<B>s es (size E) \<rbrakk>
                \<Longrightarrow> P \<turnstile> \<lfloor>(ST,LT)\<rfloor> \<le>' ty\<^sub>i' ST E A"
 (*<*)
 proof(induct e and es rule: compT.induct compTs.induct)
   case FAss thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
 next
   case BinOp thus ?case
     by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans split:bop.splits)
 next
   case Seq thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
 next
   case While thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
 next
   case Cond thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
 next
   case Block thus ?case
     by(force simp add:hyperset_defs ty\<^sub>i'_def simp del:pair_conv_ty\<^sub>i'
              elim!:sup_state_opt_trans)
 next
   case Call thus ?case by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
 next
   case Cons_exp thus ?case
     by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
 next
   case TryCatch thus ?case
     by(fastforce simp:hyperset_defs intro!: ty\<^sub>i'_incr
                 elim!:sup_state_opt_trans)
 qed (auto simp:hyperset_defs)
 
 declare (in TC0)
   ty\<^sub>i'_antimono [rule del] after_def[simp del]
   pair_conv_ty\<^sub>i'[simp del] pair_eq_ty\<^sub>i'_conv[simp del]
 (*>*)
 
 
 lemma [iff]: "OK None \<in> states P mxs mxl"
 (*<*)by(simp add: JVM_states_unfold)(*>*)
 
 lemma (in TC0) after_in_states:
 assumes wf: "wf_prog p P" and wt: "P,E \<turnstile>\<^sub>1 e :: T"
   and Etypes: "set E \<subseteq> types P" and STtypes: "set ST \<subseteq> types P"
   and stack: "size ST + max_stack e \<le> mxs"
 shows "OK (after E A ST e) \<in> states P mxs mxl"
 (*<*)
 proof -
   have "size ST + 1 \<le> mxs" using max_stack1[where e=e] wt stack
     by fastforce
   then show ?thesis using assms
     by(simp add: after_def ty\<^sub>i'_def JVM_states_unfold ty\<^sub>l_in_types)
       (blast intro!:listI WT\<^sub>1_is_type)
 qed
 (*>*)
 
 
 lemma (in TC0) OK_ty\<^sub>i'_in_statesI[simp]:
   "\<lbrakk> set E \<subseteq> types P; set ST \<subseteq> types P; size ST \<le> mxs \<rbrakk>
   \<Longrightarrow> OK (ty\<^sub>i' ST E A) \<in> states P mxs mxl"
 (*<*)
 by(simp add:ty\<^sub>i'_def JVM_states_unfold ty\<^sub>l_in_types)
   (blast intro!:listI)
 (*>*)
 
 
 lemma is_class_type_aux: "is_class P C \<Longrightarrow> is_type P (Class C)"
 (*<*)by(simp)(*>*)
 
 (*<*)
 declare is_type_simps[simp del] subsetI[rule del]
 (*>*)
 
 theorem (in TC1) compT_states:
 assumes wf: "wf_prog p P"
 shows "\<And>E T A ST.
   \<lbrakk> P,E \<turnstile>\<^sub>1 e :: T; set E \<subseteq> types P; set ST \<subseteq> types P;
     size ST + max_stack e \<le> mxs; size E + max_vars e \<le> mxl \<rbrakk>
   \<Longrightarrow> OK ` set(compT E A ST e) \<subseteq> states P mxs mxl"
 (*<*)(is "\<And>E T A ST. PROP ?P e E T A ST")(*>*)
 
 and "\<And>E Ts A ST.
   \<lbrakk> P,E \<turnstile>\<^sub>1 es[::]Ts;  set E \<subseteq> types P; set ST \<subseteq> types P;
     size ST + max_stacks es \<le> mxs; size E + max_varss es \<le> mxl \<rbrakk>
   \<Longrightarrow> OK ` set(compTs E A ST es) \<subseteq> states P mxs mxl"
 (*<*)(is "\<And>E Ts A ST. PROP ?Ps es E Ts A ST")
 proof(induct e and es rule: compT.induct compTs.induct)
   case new thus ?case by(simp)
 next
   case (Cast C e) thus ?case by (auto simp:after_in_states[OF wf])
 next
   case Val thus  ?case by(simp)
 next
   case Var thus ?case by(simp)
 next
   case LAss thus ?case  by(auto simp:after_in_states[OF wf])
 next
   case FAcc thus ?case by(auto simp:after_in_states[OF wf])
 next
   case SFAcc thus ?case by(auto simp:after_in_states[OF wf])
 next
   case FAss thus ?case
     by(auto simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case SFAss thus ?case
     by(auto simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case Seq thus ?case
     by(auto simp:image_Un after_in_states[OF wf])
 next
   case BinOp thus ?case
     by(auto simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case Cond thus ?case
     by(force simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case While thus ?case
     by(auto simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case Block thus ?case by(auto)
 next
   case (TryCatch e\<^sub>1 C i e\<^sub>2)
   moreover have "size ST + 1 \<le> mxs"
    using TryCatch.prems max_stack1[where e=e\<^sub>1] by fastforce
   ultimately show ?case  
     by(auto simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf]
                   is_class_type_aux)
 next
   case Nil_exp thus ?case by simp
 next
   case Cons_exp thus ?case
     by(auto simp:image_Un  WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case throw thus ?case
     by(auto simp: WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case Call thus ?case
     by(auto simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case SCall thus ?case
     by(auto simp:image_Un WT\<^sub>1_is_type[OF wf] after_in_states[OF wf])
 next
   case INIT thus ?case by simp
 next
   case RI thus ?case by simp
 qed
 
 declare is_type_simps[simp] subsetI[intro!]
 (*>*)
 
 
 definition shift :: "nat \<Rightarrow> ex_table \<Rightarrow> ex_table"
 where
   "shift n xt \<equiv> map (\<lambda>(from,to,C,handler,depth). (from+n,to+n,C,handler+n,depth)) xt"
 
 
 lemma [simp]: "shift 0 xt = xt"
 (*<*)by(induct xt)(auto simp:shift_def)(*>*)
 
 lemma [simp]: "shift n [] = []"
 (*<*)by(simp add:shift_def)(*>*)
 
 lemma [simp]: "shift n (xt\<^sub>1 @ xt\<^sub>2) = shift n xt\<^sub>1 @ shift n xt\<^sub>2"
 (*<*)by(simp add:shift_def)(*>*)
 
 lemma [simp]: "shift m (shift n xt) = shift (m+n) xt"
 (*<*)by(induct xt)(auto simp:shift_def)(*>*)
 
 lemma [simp]: "pcs (shift n xt) = {pc+n|pc. pc \<in> pcs xt}"
 (*<*)
 proof -
   { fix x f t C h d
     assume "(f,t,C,h,d) \<in> set xt" and "f + n \<le> x"
       and "x < t + n"
     then have "\<exists>pc. x = pc + n \<and> (\<exists>x\<in>set xt. pc \<in> (case x of (f, t, C, h, d) \<Rightarrow> {f..<t}))"
       by(rule_tac x = "x-n" in exI) (force split:nat_diff_split)
   }
   then show ?thesis by(auto simp:shift_def pcs_def) fast
 qed
 (*>*)
 
 
 lemma shift_compxE\<^sub>2:
 shows "\<And>pc pc' d. shift pc (compxE\<^sub>2 e pc' d) = compxE\<^sub>2 e (pc' + pc) d"
 and  "\<And>pc pc' d. shift pc (compxEs\<^sub>2 es pc' d) = compxEs\<^sub>2 es (pc' + pc) d"
 (*<*)
 by(induct e and es rule: compxE\<^sub>2.induct compxEs\<^sub>2.induct)
   (auto simp:shift_def ac_simps)
 (*>*)
 
 
 lemma compxE\<^sub>2_size_convs[simp]:
 shows "n \<noteq> 0 \<Longrightarrow> compxE\<^sub>2 e n d = shift n (compxE\<^sub>2 e 0 d)"
 and "n \<noteq> 0 \<Longrightarrow> compxEs\<^sub>2 es n d = shift n (compxEs\<^sub>2 es 0 d)"
 (*<*)by(simp_all add:shift_compxE\<^sub>2)(*>*)
 
 locale TC2 = TC1 +
   fixes T\<^sub>r :: ty and mxs :: pc
 begin
 
 definition
   wt_instrs :: "instr list \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i' list \<Rightarrow> bool"
     ("(\<turnstile> _, _ /[::]/ _)" [0,0,51] 50) where
   "\<turnstile> is,xt [::] \<tau>s \<longleftrightarrow> size is < size \<tau>s \<and> pcs xt \<subseteq> {0..<size is} \<and>
   (\<forall>pc< size is. P,T\<^sub>r,mxs,size \<tau>s,xt \<turnstile> is!pc,pc :: \<tau>s)"
 
 end
 
 notation TC2.wt_instrs ("(_,_,_ \<turnstile>/ _, _ /[::]/ _)" [50,50,50,50,50,51] 50)
 
 (*<*)
 lemmas (in TC2) wt_defs =
   wt_instrs_def wt_instr_def app_def eff_def norm_eff_def
 (*>*)
 
 lemma (in TC2) [simp]: "\<tau>s \<noteq> [] \<Longrightarrow> \<turnstile> [],[] [::] \<tau>s"
 (*<*) by (simp add: wt_defs) (*>*)
 
 lemma [simp]: "eff i P pc et None = []"
 (*<*)by (simp add: Effect.eff_def)(*>*)
 
 (*<*)
 declare split_comp_eq[simp del]
 (*>*)
 
 lemma wt_instr_appR:
  "\<lbrakk> P,T,m,mpc,xt \<turnstile> is!pc,pc :: \<tau>s;
     pc < size is; size is < size \<tau>s; mpc \<le> size \<tau>s; mpc \<le> mpc' \<rbrakk>
   \<Longrightarrow> P,T,m,mpc',xt \<turnstile> is!pc,pc :: \<tau>s@\<tau>s'"
 (*<*)by (fastforce simp:wt_instr_def app_def)(*>*)
 
 
 lemma relevant_entries_shift [simp]:
   "relevant_entries P i (pc+n) (shift n xt) = shift n (relevant_entries P i pc xt)"
 (*<*)
 proof(induct xt)
   case Nil
   then show ?case by (simp add: relevant_entries_def shift_def)
 next
   case (Cons a xt)
   then show ?case 
     by (auto simp add: relevant_entries_def shift_def is_relevant_entry_def)
 qed
 (*>*)
 
 
 lemma [simp]:
   "xcpt_eff i P (pc+n) \<tau> (shift n xt) =
    map (\<lambda>(pc,\<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)"
 (*<*)
 proof -
   obtain ST LT where "\<tau> = (ST, LT)" by(cases \<tau>) simp
   then show ?thesis by(simp add: xcpt_eff_def) (auto simp add: shift_def)
 qed
 (*>*)
 
 
 lemma  [simp]:
   "app\<^sub>i (i, P, pc, m, T, \<tau>) \<Longrightarrow>
    eff i P (pc+n) (shift n xt) (Some \<tau>) =
    map (\<lambda>(pc,\<tau>). (pc+n,\<tau>)) (eff i P pc xt (Some \<tau>))"
 (*<*)by(cases "i") (auto simp add:eff_def norm_eff_def)(*>*)
 
 
 lemma [simp]:
   "xcpt_app i P (pc+n) mxs (shift n xt) \<tau> = xcpt_app i P pc mxs xt \<tau>"
 (*<*)by (simp add: xcpt_app_def) (auto simp add: shift_def)(*>*)
 
 
 lemma wt_instr_appL:
 assumes "P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s" and "pc < size \<tau>s" and "mpc \<le> size \<tau>s"
 shows "P,T,m,mpc + size \<tau>s',shift (size \<tau>s') xt \<turnstile> i,pc+size \<tau>s' :: \<tau>s'@\<tau>s"
 (*<*)
 proof -
   let ?t = "(\<tau>s'@\<tau>s)!(pc+size \<tau>s')"
   show ?thesis
   proof(cases ?t)
     case (Some \<tau>)
     obtain ST LT where [simp]: "\<tau> = (ST, LT)" by(cases \<tau>) simp
     have "app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)"
       using Some assms by(cases "i") (auto simp:wt_instr_def app_def)
     moreover {
       fix pc' \<tau>' assume "(pc',\<tau>') \<in> set (eff i P pc xt ?t)"
       then have "P \<turnstile> \<tau>' \<le>' \<tau>s!pc'" and "pc' < mpc"
         using Some assms by(auto simp:wt_instr_def app_def)
     }
     ultimately show ?thesis using Some assms
       by(fastforce simp:wt_instr_def app_def)
   qed (auto simp:wt_instr_def app_def)
 qed
 (*>*)
 
 
 lemma wt_instr_Cons:
 assumes wti: "P,T,m,mpc - 1,[] \<turnstile> i,pc - 1 :: \<tau>s"
   and pcl: "0 < pc" and mpcl: "0 < mpc"
   and pcu: "pc < size \<tau>s + 1" and mpcu: "mpc \<le> size \<tau>s + 1"
 shows "P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>#\<tau>s"
 (*<*)
 proof -
   have "pc - 1 < length \<tau>s" using pcl pcu by arith
   moreover have "mpc - 1 \<le> length \<tau>s" using mpcl mpcu by arith
   ultimately have
     "P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s"
     by(rule wt_instr_appL[where \<tau>s' = "[\<tau>]", OF wti])
   then show ?thesis using pcl mpcl by (simp split:nat_diff_split_asm)
 qed
 (*>*)
 
 
 lemma wt_instr_append:
 assumes wti: "P,T,m,mpc - size \<tau>s',[] \<turnstile> i,pc - size \<tau>s' :: \<tau>s"
   and pcl: "size \<tau>s' \<le> pc" and mpcl: "size \<tau>s' \<le> mpc"
   and pcu: "pc < size \<tau>s + size \<tau>s'" and mpcu: "mpc \<le> size \<tau>s + size \<tau>s'"
 shows "P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s'@\<tau>s"
 (*<*)
 proof -
   have "pc - length \<tau>s' < length \<tau>s" using pcl pcu by arith
   moreover have "mpc - length \<tau>s' \<le> length \<tau>s" using mpcl mpcu by arith
 thm wt_instr_appL[where \<tau>s' = "\<tau>s'", OF wti]
   ultimately have "P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') []
                      \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s"
     by(rule wt_instr_appL[where \<tau>s' = "\<tau>s'", OF wti])
   then show ?thesis using pcl mpcl by (simp split:nat_diff_split_asm)
 qed
 (*>*)
 
 
 lemma xcpt_app_pcs:
   "pc \<notin> pcs xt \<Longrightarrow> xcpt_app i P pc mxs xt \<tau>"
 (*<*)
 by (auto simp add: xcpt_app_def relevant_entries_def is_relevant_entry_def pcs_def)
 (*>*)
 
 
 lemma xcpt_eff_pcs:
   "pc \<notin> pcs xt \<Longrightarrow> xcpt_eff i P pc \<tau> xt = []"
 (*<*)
 by (cases \<tau>)
    (auto simp add: is_relevant_entry_def xcpt_eff_def relevant_entries_def pcs_def
            intro!: filter_False)
 (*>*)
 
 
 lemma pcs_shift:
   "pc < n \<Longrightarrow> pc \<notin> pcs (shift n xt)" 
 (*<*)by (auto simp add: shift_def pcs_def)(*>*)
 
 
 lemma wt_instr_appRx:
   "\<lbrakk> P,T,m,mpc,xt \<turnstile> is!pc,pc :: \<tau>s; pc < size is; size is < size \<tau>s; mpc \<le> size \<tau>s \<rbrakk>
   \<Longrightarrow> P,T,m,mpc,xt @ shift (size is) xt' \<turnstile> is!pc,pc :: \<tau>s"
 (*<*)by (auto simp:wt_instr_def eff_def app_def xcpt_app_pcs xcpt_eff_pcs)(*>*)
 
 
 lemma wt_instr_appLx: 
   "\<lbrakk> P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc \<notin> pcs xt' \<rbrakk>
   \<Longrightarrow> P,T,m,mpc,xt'@xt \<turnstile> i,pc :: \<tau>s"
 (*<*)by (auto simp:wt_instr_def app_def eff_def xcpt_app_pcs xcpt_eff_pcs)(*>*)
 
 
 lemma (in TC2) wt_instrs_extR:
   "\<turnstile> is,xt [::] \<tau>s \<Longrightarrow> \<turnstile> is,xt [::] \<tau>s @ \<tau>s'"
 (*<*)by(auto simp add:wt_instrs_def wt_instr_appR)(*>*)
 
 
 lemma (in TC2) wt_instrs_ext:
 assumes wt\<^sub>1: "\<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2" and wt\<^sub>2: "\<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>s\<^sub>2"
   and \<tau>s_size: "size \<tau>s\<^sub>1 = size is\<^sub>1"
  shows "\<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2"
 (*<*)
 proof -
   let ?is = "is\<^sub>1@is\<^sub>2" and ?xt = "xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2"
     and ?\<tau>s = "\<tau>s\<^sub>1@\<tau>s\<^sub>2"
   have "size ?is < size ?\<tau>s" using wt\<^sub>2 \<tau>s_size by(fastforce simp:wt_instrs_def)
   moreover have "pcs ?xt \<subseteq> {0..<size ?is}" using wt\<^sub>1 wt\<^sub>2
     by(fastforce simp:wt_instrs_def)
   moreover {
     fix pc assume pc: "pc<size ?is"
     have "P,T\<^sub>r,mxs,size ?\<tau>s,?xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
     proof(cases "pc < length is\<^sub>1")
       case True then show ?thesis using wt\<^sub>1 pc
         by(fastforce simp: wt_instrs_def wt_instr_appRx)
     next
       case False
       then have "pc - length is\<^sub>1 < length is\<^sub>2" using pc by fastforce
       then have "P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2"
         using wt\<^sub>2 by(clarsimp simp: wt_instrs_def)
       moreover have "pc - length is\<^sub>1 < length \<tau>s\<^sub>2" using pc wt\<^sub>2
         by(clarsimp simp: wt_instrs_def) arith
       moreover have "length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2" by simp
       moreover have "pc - length is\<^sub>1 + length \<tau>s\<^sub>1 \<notin> pcs xt\<^sub>1" using wt\<^sub>1 \<tau>s_size
         by(fastforce simp: wt_instrs_def)
       ultimately have "P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,xt\<^sub>1 @ shift (length \<tau>s\<^sub>1) xt\<^sub>2
                          \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2"
         by(rule wt_instr_appLx[OF wt_instr_appL[where \<tau>s' = "\<tau>s\<^sub>1"]])
       then show ?thesis using False \<tau>s_size by(simp add:add.commute)
     qed
   }
   ultimately show ?thesis by(clarsimp simp:wt_instrs_def)
 qed
 (*>*)
 
 corollary (in TC2) wt_instrs_ext2:
   "\<lbrakk> \<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>s\<^sub>2; \<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2; size \<tau>s\<^sub>1 = size is\<^sub>1 \<rbrakk>
   \<Longrightarrow> \<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2"
 (*<*)by(rule wt_instrs_ext)(*>*)
 
 
 corollary (in TC2) wt_instrs_ext_prefix [trans]:
   "\<lbrakk> \<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2; \<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>s\<^sub>3;
      size \<tau>s\<^sub>1 = size is\<^sub>1; prefix \<tau>s\<^sub>3 \<tau>s\<^sub>2 \<rbrakk>
   \<Longrightarrow> \<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2"
 (*<*)by(bestsimp simp:prefix_def elim: wt_instrs_ext dest:wt_instrs_extR)(*>*)
 
 
 corollary (in TC2) wt_instrs_app:
   assumes is\<^sub>1: "\<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1@[\<tau>]"
   assumes is\<^sub>2: "\<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>#\<tau>s\<^sub>2"
   assumes s: "size \<tau>s\<^sub>1 = size is\<^sub>1"
   shows "\<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1@shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1@\<tau>#\<tau>s\<^sub>2"
 (*<*)
 proof -
   from is\<^sub>1 have "\<turnstile> is\<^sub>1,xt\<^sub>1 [::] (\<tau>s\<^sub>1@[\<tau>])@\<tau>s\<^sub>2"
     by (rule wt_instrs_extR)
   hence "\<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1@\<tau>#\<tau>s\<^sub>2" by simp
   from this is\<^sub>2 s show ?thesis by (rule wt_instrs_ext) 
 qed
 (*>*)
 
 
 corollary (in TC2) wt_instrs_app_last[trans]:
 assumes "\<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>#\<tau>s\<^sub>2" "\<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1"
   "last \<tau>s\<^sub>1 = \<tau>" "size \<tau>s\<^sub>1 = size is\<^sub>1+1"
 shows "\<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1@shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2"
 (*<*)
 using assms proof(cases \<tau>s\<^sub>1 rule:rev_cases)
   case (snoc ys y)
   then show ?thesis using assms by(simp add:wt_instrs_app)
 qed simp
 (*>*)
 
 
 corollary (in TC2) wt_instrs_append_last[trans]:
 assumes wtis: "\<turnstile> is,xt [::] \<tau>s" and wti: "P,T\<^sub>r,mxs,mpc,[] \<turnstile> i,pc :: \<tau>s"
   and pc: "pc = size is" and mpc: "mpc = size \<tau>s" and is_\<tau>s: "size is + 1 < size \<tau>s"
 shows "\<turnstile> is@[i],xt [::] \<tau>s"
 (*<*)
 proof -
   have pc_xt: "pc \<notin> pcs xt" using wtis pc by (fastforce simp:wt_instrs_def)
   have "pcs xt \<subseteq> {..<Suc (length is)}" using wtis by (fastforce simp:wt_instrs_def)
   moreover {
     fix pc' assume pc': "\<not> pc' < length is" "pc' < Suc (length is)"
     have "P,T\<^sub>r,mxs,length \<tau>s,xt \<turnstile> i,pc' :: \<tau>s"
       using wt_instr_appLx[where xt = "[]",simplified,OF wti pc_xt]
             less_antisym[OF pc'] pc mpc by simp
   }
   ultimately show ?thesis using wtis is_\<tau>s by(clarsimp simp add:wt_instrs_def)
 qed
 (*>*)
 
 
 corollary (in TC2) wt_instrs_app2:
   "\<lbrakk> \<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>'#\<tau>s\<^sub>2;  \<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>#\<tau>s\<^sub>1@[\<tau>'];
      xt' = xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2;  size \<tau>s\<^sub>1+1 = size is\<^sub>1 \<rbrakk>
   \<Longrightarrow> \<turnstile> is\<^sub>1@is\<^sub>2,xt' [::] \<tau>#\<tau>s\<^sub>1@\<tau>'#\<tau>s\<^sub>2"
 (*<*)using wt_instrs_app[where ?\<tau>s\<^sub>1.0 = "\<tau> # \<tau>s\<^sub>1"] by simp (*>*)
 
 
 corollary (in TC2) wt_instrs_app2_simp[trans,simp]:
   "\<lbrakk> \<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>'#\<tau>s\<^sub>2;  \<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>#\<tau>s\<^sub>1@[\<tau>']; size \<tau>s\<^sub>1+1 = size is\<^sub>1 \<rbrakk>
   \<Longrightarrow> \<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1@shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>#\<tau>s\<^sub>1@\<tau>'#\<tau>s\<^sub>2"
 (*<*)using wt_instrs_app[where ?\<tau>s\<^sub>1.0 = "\<tau> # \<tau>s\<^sub>1"] by simp(*>*)
 
 
 corollary (in TC2) wt_instrs_Cons[simp]:
   "\<lbrakk> \<tau>s \<noteq> []; \<turnstile> [i],[] [::] [\<tau>,\<tau>']; \<turnstile> is,xt [::] \<tau>'#\<tau>s \<rbrakk>
   \<Longrightarrow> \<turnstile> i#is,shift 1 xt [::] \<tau>#\<tau>'#\<tau>s"
 (*<*)
 using wt_instrs_app2[where ?is\<^sub>1.0 = "[i]" and ?\<tau>s\<^sub>1.0 = "[]" and ?is\<^sub>2.0 = "is"
                       and ?xt\<^sub>1.0 = "[]"]
 by simp
 
 
 corollary (in TC2) wt_instrs_Cons2[trans]:
   assumes \<tau>s: "\<turnstile> is,xt [::] \<tau>s"
   assumes i: "P,T\<^sub>r,mxs,mpc,[] \<turnstile> i,0 :: \<tau>#\<tau>s"
   assumes mpc: "mpc = size \<tau>s + 1"
   shows "\<turnstile> i#is,shift 1 xt [::] \<tau>#\<tau>s"
 (*<*)
 proof -
   from \<tau>s have "\<tau>s \<noteq> []" by (auto simp: wt_instrs_def)
   with mpc i have "\<turnstile> [i],[] [::] [\<tau>]@\<tau>s" by (simp add: wt_instrs_def)
   with \<tau>s show ?thesis by (fastforce dest: wt_instrs_ext)
 qed
 (*>*)
 
 
 lemma (in TC2) wt_instrs_last_incr[trans]:
 assumes wtis: "\<turnstile> is,xt [::] \<tau>s@[\<tau>]" and ss: "P \<turnstile> \<tau> \<le>' \<tau>'"
 shows "\<turnstile> is,xt [::] \<tau>s@[\<tau>']"
 (*<*)
 proof -
   let ?\<tau>s = "\<tau>s@[\<tau>]" and ?\<tau>s' = "\<tau>s@[\<tau>']"
   { fix pc assume pc: "pc< size is"
     let ?i = "is!pc"
     have app_pc: "app (is ! pc) P mxs T\<^sub>r pc (length ?\<tau>s) xt (\<tau>s ! pc)"
       using wtis pc by(clarsimp simp add:wt_instrs_def wt_instr_def)
     then have Apc\<tau>': "\<And>pc' \<tau>'. (pc',\<tau>') \<in> set (eff ?i P pc xt (?\<tau>s!pc))
      \<Longrightarrow> pc' < length ?\<tau>s"
       using wtis pc by(fastforce simp add:wt_instrs_def app_def)
     have Aepc\<tau>': "\<And>pc' \<tau>'. (pc',\<tau>') \<in> set (eff ?i P pc xt (?\<tau>s!pc))
      \<Longrightarrow> P \<turnstile> \<tau>' \<le>' ?\<tau>s!pc'"
       using wtis pc by(fastforce simp add:wt_instrs_def wt_instr_def)
     { fix pc1 \<tau>1 assume pc\<tau>1: "(pc1,\<tau>1) \<in> set (eff ?i P pc xt (?\<tau>s'!pc))"
       then have epc\<tau>': "(pc1,\<tau>1) \<in> set (eff ?i P pc xt (?\<tau>s!pc))"
           using wtis pc by(simp add:wt_instrs_def)
       have "P \<turnstile> \<tau>1 \<le>' ?\<tau>s'!pc1"
       proof(cases "pc1 < length \<tau>s")
         case True
         then show ?thesis using wtis pc pc\<tau>1
           by(fastforce simp add:wt_instrs_def wt_instr_def)
       next
         case False
         then have "pc1 < length ?\<tau>s" using Apc\<tau>'[OF epc\<tau>'] by simp
         then have [simp]: "pc1 = size \<tau>s" using False by clarsimp
         have "P \<turnstile> \<tau>1 \<le>' \<tau>" using Aepc\<tau>'[OF epc\<tau>'] by simp
         then have "P \<turnstile> \<tau>1 \<le>' \<tau>'" by(rule sup_state_opt_trans[OF _ ss])
         then show ?thesis by simp
       qed
     }
     then have "P,T\<^sub>r,mxs,size ?\<tau>s',xt \<turnstile> is!pc,pc :: ?\<tau>s'" using wtis pc
       by(clarsimp simp add:wt_instrs_def wt_instr_def)
   }
   then show ?thesis using wtis by(simp add:wt_instrs_def)
 qed
 (*>*)
 
 
 lemma [iff]: "xcpt_app i P pc mxs [] \<tau>"
 (*<*)by (simp add: xcpt_app_def relevant_entries_def)(*>*)
 
 
 lemma [simp]: "xcpt_eff i P pc \<tau> [] = []"
 (*<*)by (simp add: xcpt_eff_def relevant_entries_def)(*>*)
 
 
 lemma (in TC2) wt_New:
   "\<lbrakk> is_class P C; size ST < mxs \<rbrakk> \<Longrightarrow>
    \<turnstile> [New C],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (Class C#ST) E A]"
 (*<*)by(simp add:wt_defs ty\<^sub>i'_def)(*>*)
 
 
 lemma (in TC2) wt_Cast:
   "is_class P C \<Longrightarrow>
    \<turnstile> [Checkcast C],[] [::] [ty\<^sub>i' (Class D # ST) E A, ty\<^sub>i' (Class C # ST) E A]"
 (*<*)by(simp add: ty\<^sub>i'_def wt_defs)(*>*)
 
 
 lemma (in TC2) wt_Push:
   "\<lbrakk> size ST < mxs; typeof v = Some T \<rbrakk>
   \<Longrightarrow> \<turnstile> [Push v],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T#ST) E A]"
 (*<*)by(simp add: ty\<^sub>i'_def wt_defs)(*>*)
 
 
 lemma (in TC2) wt_Pop:
  "\<turnstile> [Pop],[] [::] (ty\<^sub>i' (T#ST) E A # ty\<^sub>i' ST E A # \<tau>s)"
 (*<*)by(simp add: ty\<^sub>i'_def wt_defs)(*>*)
 
 
 lemma (in TC2) wt_CmpEq:
   "\<lbrakk> P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<or> P \<turnstile> T\<^sub>2 \<le> T\<^sub>1\<rbrakk>
   \<Longrightarrow> \<turnstile> [CmpEq],[] [::] [ty\<^sub>i' (T\<^sub>2 # T\<^sub>1 # ST) E A, ty\<^sub>i' (Boolean # ST) E A]"
 (*<*) by(auto simp:ty\<^sub>i'_def wt_defs elim!: refTE not_refTE) (*>*)
 
 
 lemma (in TC2) wt_IAdd:
   "\<turnstile> [IAdd],[] [::] [ty\<^sub>i' (Integer#Integer#ST) E A, ty\<^sub>i' (Integer#ST) E A]"
 (*<*)by(simp add:ty\<^sub>i'_def wt_defs)(*>*)
 
 
 lemma (in TC2) wt_Load:
   "\<lbrakk> size ST < mxs; size E \<le> mxl; i \<in>\<in> A; i < size E \<rbrakk>
   \<Longrightarrow> \<turnstile> [Load i],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (E!i # ST) E A]"
 (*<*)by(auto simp add:ty\<^sub>i'_def wt_defs ty\<^sub>l_def hyperset_defs)(*>*)
 
 
 lemma (in TC2) wt_Store:
  "\<lbrakk> P \<turnstile> T \<le> E!i; i < size E; size E \<le> mxl \<rbrakk> \<Longrightarrow>
   \<turnstile> [Store i],[] [::] [ty\<^sub>i' (T#ST) E A, ty\<^sub>i' ST E (\<lfloor>{i}\<rfloor> \<squnion> A)]"
 (*<*)
 by(auto simp:hyperset_defs nth_list_update ty\<^sub>i'_def wt_defs ty\<^sub>l_def
         intro:list_all2_all_nthI)
 (*>*)
 
 
 lemma (in TC2) wt_Get:
  "\<lbrakk> P \<turnstile> C sees F,NonStatic:T in D \<rbrakk> \<Longrightarrow>
   \<turnstile> [Getfield F D],[] [::] [ty\<^sub>i' (Class C # ST) E A, ty\<^sub>i' (T # ST) E A]"
 (*<*)by(auto simp: ty\<^sub>i'_def wt_defs dest: sees_field_idemp sees_field_decl_above)(*>*)
 
 lemma (in TC2) wt_GetS:
  "\<lbrakk> size ST < mxs; P \<turnstile> C sees F,Static:T in D \<rbrakk> \<Longrightarrow>
   \<turnstile> [Getstatic C F D],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T # ST) E A]"
 (*<*)by(auto simp: ty\<^sub>i'_def wt_defs dest: sees_field_idemp sees_field_decl_above)(*>*)
 
 lemma (in TC2) wt_Put:
   "\<lbrakk> P \<turnstile> C sees F,NonStatic:T in D; P \<turnstile> T' \<le> T \<rbrakk> \<Longrightarrow>
   \<turnstile> [Putfield F D],[] [::] [ty\<^sub>i' (T' # Class C # ST) E A, ty\<^sub>i' ST E A]"
 (*<*)by(auto intro: sees_field_idemp sees_field_decl_above simp: ty\<^sub>i'_def wt_defs)(*>*)
 
 lemma (in TC2) wt_PutS:
   "\<lbrakk> P \<turnstile> C sees F,Static:T in D; P \<turnstile> T' \<le> T \<rbrakk> \<Longrightarrow>
   \<turnstile> [Putstatic C F D],[] [::] [ty\<^sub>i' (T' # ST) E A, ty\<^sub>i' ST E A]"
 (*<*)by(auto intro: sees_field_idemp sees_field_decl_above simp: ty\<^sub>i'_def wt_defs)(*>*)
 
 
 lemma (in TC2) wt_Throw:
   "\<turnstile> [Throw],[] [::] [ty\<^sub>i' (Class C # ST) E A, \<tau>']"
 (*<*)by(auto simp: ty\<^sub>i'_def wt_defs)(*>*)
 
 
 lemma (in TC2) wt_IfFalse:
   "\<lbrakk> 2 \<le> i; nat i < size \<tau>s + 2; P \<turnstile> ty\<^sub>i' ST E A \<le>' \<tau>s ! nat(i - 2) \<rbrakk>
   \<Longrightarrow> \<turnstile> [IfFalse i],[] [::] ty\<^sub>i' (Boolean # ST) E A # ty\<^sub>i' ST E A # \<tau>s"
 (*<*)
 by(simp add: ty\<^sub>i'_def wt_defs eval_nat_numeral nat_diff_distrib)
 (*>*)
 
 
 lemma wt_Goto:
  "\<lbrakk> 0 \<le> int pc + i; nat (int pc + i) < size \<tau>s; size \<tau>s \<le> mpc;
     P \<turnstile> \<tau>s!pc \<le>' \<tau>s ! nat (int pc + i) \<rbrakk>
  \<Longrightarrow> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: \<tau>s"
 (*<*)by(clarsimp simp add: TC2.wt_defs)(*>*)
 
 
 lemma (in TC2) wt_Invoke:
   "\<lbrakk> size es = size Ts'; P \<turnstile> C sees M,NonStatic: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
   \<Longrightarrow> \<turnstile> [Invoke M (size es)],[] [::] [ty\<^sub>i' (rev Ts' @ Class C # ST) E A, ty\<^sub>i' (T#ST) E A]"
 (*<*)by(fastforce simp add: ty\<^sub>i'_def wt_defs)(*>*)
 
 lemma (in TC2) wt_Invokestatic:
   "\<lbrakk> size ST < mxs; size es = size Ts'; M \<noteq> clinit;
      P \<turnstile> C sees M,Static: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
   \<Longrightarrow> \<turnstile> [Invokestatic C M (size es)],[] [::] [ty\<^sub>i' (rev Ts' @ ST) E A, ty\<^sub>i' (T#ST) E A]"
 (*<*)by(fastforce simp add: ty\<^sub>i'_def wt_defs)(*>*)
 
 
 corollary (in TC2) wt_instrs_app3[simp]:
   "\<lbrakk> \<turnstile> is\<^sub>2,[] [::] (\<tau>' # \<tau>s\<^sub>2);  \<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau> # \<tau>s\<^sub>1 @ [\<tau>']; size \<tau>s\<^sub>1+1 = size is\<^sub>1\<rbrakk>
   \<Longrightarrow> \<turnstile> (is\<^sub>1 @ is\<^sub>2),xt\<^sub>1 [::] \<tau> # \<tau>s\<^sub>1 @ \<tau>' # \<tau>s\<^sub>2"
 (*<*)using wt_instrs_app2[where ?xt\<^sub>2.0 = "[]"] by (simp add:shift_def)(*>*)
 
 
 corollary (in TC2) wt_instrs_Cons3[simp]:
   "\<lbrakk> \<tau>s \<noteq> []; \<turnstile> [i],[] [::] [\<tau>,\<tau>']; \<turnstile> is,[] [::] \<tau>'#\<tau>s \<rbrakk>
   \<Longrightarrow> \<turnstile> (i # is),[] [::] \<tau> # \<tau>' # \<tau>s"
 (*<*)
 using wt_instrs_Cons[where ?xt = "[]"]
 by (simp add:shift_def)
 
 (*<*)
 declare nth_append[simp del]
 declare [[simproc del: list_to_set_comprehension]]
 (*>*)
 
 lemma (in TC2) wt_instrs_xapp[trans]:
 assumes wtis: "\<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2"
   and P_\<tau>s\<^sub>1: "\<forall>\<tau> \<in> set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = Some(ST',LT') \<longrightarrow> 
     size ST \<le> size ST' \<and> P \<turnstile> Some (drop (size ST' - size ST) ST',LT') \<le>' ty\<^sub>i' ST E A"
   and is_\<tau>s: "size is\<^sub>1 = size \<tau>s\<^sub>1" and PC: "is_class P C" and ST_mxs: "size ST < mxs"
 shows "\<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0,size is\<^sub>1 - 1,C,size is\<^sub>1,size ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2"
 (*<*)(is "\<turnstile> ?is, xt@[?xte] [::] ?\<tau>s" is "\<turnstile> ?is, ?xt' [::] ?\<tau>s")
 proof -
   have P_\<tau>s\<^sub>1': "\<And>\<tau>. \<tau> \<in> set \<tau>s\<^sub>1 \<Longrightarrow> (\<forall>ST' LT'. \<tau> = Some(ST',LT') \<longrightarrow>
      size ST \<le> size ST' \<and> P \<turnstile> Some (drop (size ST' - size ST) ST',LT') \<le>' ty\<^sub>i' ST E A)"
     using P_\<tau>s\<^sub>1 by fast
   have "size ?is < size ?\<tau>s" and "pcs ?xt' \<subseteq> {0..<size ?is}"
     and P_pc: "\<And>pc. pc< size ?is \<Longrightarrow> P,T\<^sub>r,mxs,size ?\<tau>s,xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
     using wtis by(simp_all add:wt_instrs_def)
   moreover {
     fix pc let ?mpc = "size ?\<tau>s" and ?i = "?is!pc" and ?t = "?\<tau>s!pc"
     assume "pc< size ?is"
     then have wti: "P,T\<^sub>r,mxs,?mpc,xt \<turnstile> ?i,pc :: ?\<tau>s" by(rule P_pc)
     then have app: "app ?i P mxs T\<^sub>r pc ?mpc xt ?t"
        and eff_ss: "\<And>pc' \<tau>'. (pc',\<tau>') \<in> set (eff ?i P pc xt (?\<tau>s!pc))
                            \<Longrightarrow> P \<turnstile> \<tau>' \<le>' ?\<tau>s!pc'"
       by(fastforce simp add: wt_instr_def)+
     have "app ?i P mxs T\<^sub>r pc ?mpc ?xt' ?t
              \<and> (\<forall>(pc',\<tau>') \<in> set (eff ?i P pc ?xt' ?t). P \<turnstile> \<tau>' \<le>' ?\<tau>s!pc')"
     proof (cases ?t)
       case (Some \<tau>)
       obtain ST' LT' where \<tau>: "\<tau> = (ST', LT')" by(cases \<tau>) simp
       have app\<^sub>i: "app\<^sub>i (?i,P,pc,mxs,T\<^sub>r,\<tau>)" and xcpt_app: "xcpt_app ?i P pc mxs xt \<tau>"
          and eff_pc: "\<And>pc' \<tau>'. (pc',\<tau>') \<in> set (eff ?i P pc xt ?t) \<Longrightarrow> pc' < ?mpc"
         using Some app by(fastforce simp add: app_def)+
       have "xcpt_app ?i P pc mxs ?xt' \<tau>"
       proof(cases "pc < length \<tau>s\<^sub>1 - 1")
         case False then show ?thesis using Some \<tau> is_\<tau>s xcpt_app
           by (clarsimp simp: xcpt_app_def relevant_entries_def
                              is_relevant_entry_def)
       next
         case True
         then have True': "pc < length \<tau>s\<^sub>1" by simp
         then have "\<tau>s\<^sub>1 ! pc = ?t" by(fastforce simp: nth_append)
         moreover have \<tau>s\<^sub>1_pc: "\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1" by(rule nth_mem[OF True'])
         ultimately show ?thesis
          using Some \<tau> PC ST_mxs xcpt_app P_\<tau>s\<^sub>1'[OF \<tau>s\<^sub>1_pc]
           by (simp add: xcpt_app_def relevant_entries_def)
       qed
       moreover {
         fix pc' \<tau>' assume efft: "(pc',\<tau>') \<in> set (eff ?i P pc ?xt' ?t)"
         have "pc' < ?mpc \<and> P \<turnstile> \<tau>' \<le>' ?\<tau>s!pc'" (is "?P1 \<and> ?P2")
         proof(cases "(pc',\<tau>') \<in> set (eff ?i P pc xt ?t)")
           case True
           have ?P1 using True by(rule eff_pc)
           moreover have ?P2 using True by(rule eff_ss)
           ultimately show ?thesis by simp
         next
           case False
           then have xte: "(pc',\<tau>') \<in> set (xcpt_eff ?i P pc \<tau> [?xte])"
             using efft Some by(clarsimp simp: eff_def)
           then have ?P1 using Some \<tau> is_\<tau>s
             by(clarsimp simp: xcpt_eff_def relevant_entries_def split: if_split_asm)
           moreover have ?P2
           proof(cases "pc < length \<tau>s\<^sub>1 - 1")
             case False': False
             then show ?thesis using False Some \<tau> xte is_\<tau>s
               by(simp add: xcpt_eff_def relevant_entries_def is_relevant_entry_def)
           next
             case True
             then have True': "pc < length \<tau>s\<^sub>1" by simp
             have \<tau>s\<^sub>1_pc: "\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1" by(rule nth_mem[OF True'])
             have "P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor>
                          \<le>' ty\<^sub>i' (Class C # ST) E A"
                using True' Some \<tau> P_\<tau>s\<^sub>1'[OF \<tau>s\<^sub>1_pc]
               by (fastforce simp: nth_append ty\<^sub>i'_def)
             then show ?thesis using \<tau> xte is_\<tau>s
               by(simp add: xcpt_eff_def relevant_entries_def split: if_split_asm)
           qed
           ultimately show ?thesis by simp
         qed
       }
       ultimately show ?thesis using Some app\<^sub>i by(fastforce simp add: app_def)
     qed simp
     then have "P,T\<^sub>r,mxs,size ?\<tau>s,?xt' \<turnstile> ?is!pc,pc :: ?\<tau>s"
       by(simp add: wt_instr_def)
   }
   ultimately show ?thesis by(simp add:wt_instrs_def)
 qed
 
 declare [[simproc add: list_to_set_comprehension]]
 declare nth_append[simp]
 (*>*)
 
 lemma drop_Cons_Suc:
   "\<And>xs. drop n xs = y#ys \<Longrightarrow> drop (Suc n) xs = ys"
 proof(induct n)
   case (Suc n) then show ?case by(simp add: drop_Suc)
 qed simp
 
 lemma drop_mess:
 assumes "Suc (length xs\<^sub>0) \<le> length xs"
   and "drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0"
 shows "drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0"
 using assms proof(cases xs)
   case (Cons a list) then show ?thesis using assms
   proof(cases "length list - length xs\<^sub>0")
     case Suc then show ?thesis using Cons assms
       by (simp add: Suc_diff_le drop_Cons_Suc)
   qed simp
 qed simp
 
 (*<*)
 declare (in TC0)
   after_def[simp] pair_eq_ty\<^sub>i'_conv[simp]
 (*>*)
 
 lemma (in TC1) compT_ST_prefix:
  "\<And>E A ST\<^sub>0. \<lfloor>(ST,LT)\<rfloor> \<in> set(compT E A ST\<^sub>0 e) \<Longrightarrow> 
   size ST\<^sub>0 \<le> size ST \<and> drop (size ST - size ST\<^sub>0) ST = ST\<^sub>0"
 and
  "\<And>E A ST\<^sub>0. \<lfloor>(ST,LT)\<rfloor> \<in> set(compTs E A ST\<^sub>0 es) \<Longrightarrow> 
   size ST\<^sub>0 \<le> size ST \<and> drop (size ST - size ST\<^sub>0) ST = ST\<^sub>0"
 (*<*)
 proof(induct e and es rule: compT.induct compTs.induct)
   case (FAss e\<^sub>1 F D e\<^sub>2)
   moreover {
     let ?ST\<^sub>0 = "ty E e\<^sub>1 # ST\<^sub>0"
     fix A assume "\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ?ST\<^sub>0 e\<^sub>2)"
     with FAss
     have "length ?ST\<^sub>0 \<le> length ST \<and> drop (size ST - size ?ST\<^sub>0) ST = ?ST\<^sub>0" by blast
     hence ?case  by (clarsimp simp add: drop_mess)
   }
   ultimately show ?case by auto
 next
   case TryCatch thus ?case by auto
 next
   case Block thus ?case by auto
 next
   case Seq thus ?case by auto
 next
   case While thus ?case by auto
 next
   case Cond thus ?case by auto
 next
   case (Call e M es)
   moreover {
     let ?ST\<^sub>0 = "ty E e # ST\<^sub>0"
     fix A assume "\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ?ST\<^sub>0 es)"
     with Call
     have "length ?ST\<^sub>0 \<le> length ST \<and> drop (size ST - size ?ST\<^sub>0) ST = ?ST\<^sub>0" by blast
     hence ?case  by (clarsimp simp add: drop_mess)
   }
   ultimately show ?case by auto
 next
   case (Cons_exp e es)
   moreover {
     let ?ST\<^sub>0 = "ty E e # ST\<^sub>0"
     fix A assume "\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ?ST\<^sub>0 es)"
     with Cons_exp
     have "length ?ST\<^sub>0 \<le> length ST \<and> drop (size ST - size ?ST\<^sub>0) ST = ?ST\<^sub>0" by blast
     hence ?case  by (clarsimp simp add: drop_mess)
   }
   ultimately show ?case by auto
 next
   case (BinOp e\<^sub>1 bop e\<^sub>2)
   moreover {
     let ?ST\<^sub>0 = "ty E e\<^sub>1 # ST\<^sub>0"
     fix A assume "\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ?ST\<^sub>0 e\<^sub>2)"
     with BinOp 
     have "length ?ST\<^sub>0 \<le> length ST \<and> drop (size ST - size ?ST\<^sub>0) ST = ?ST\<^sub>0" by blast
     hence ?case by (clarsimp simp add: drop_mess)
   }
   ultimately show ?case by auto
 next
   case new thus ?case by auto
 next
   case Val thus ?case by auto    
 next
   case Cast thus ?case by auto
 next
   case Var thus ?case by auto
 next
   case LAss thus ?case by auto
 next
   case throw thus ?case by auto
 next
   case FAcc thus ?case by auto
 next
   case SFAcc thus ?case by auto
 next
   case SFAss thus ?case by auto
 next
   case (SCall C M es) thus ?case by auto
 next
   case INIT thus ?case by auto
 next
   case RI thus ?case by auto
 next
   case Nil_exp thus ?case by auto
 qed 
 
 declare (in TC0) 
   after_def[simp del] pair_eq_ty\<^sub>i'_conv[simp del]
 (*>*)
 
 (* FIXME *)
 lemma fun_of_simp [simp]: "fun_of S x y = ((x,y) \<in> S)" 
 (*<*) by (simp add: fun_of_def)(*>*)
 
 theorem (in TC2) compT_wt_instrs: "\<And>E T A ST.
   \<lbrakk> P,E \<turnstile>\<^sub>1 e :: T; \<D> e A; \<B> e (size E); 
     size ST + max_stack e \<le> mxs; size E + max_vars e \<le> mxl \<rbrakk>
   \<Longrightarrow> \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (size ST) [::]
                  ty\<^sub>i' ST E A # compT E A ST e @ [after E A ST e]"
 (*<*)(is "\<And>E T A ST. PROP ?P e E T A ST")(*>*)
 
 and "\<And>E Ts A ST.
   \<lbrakk> P,E \<turnstile>\<^sub>1 es[::]Ts;  \<D>s es A; \<B>s es (size E); 
     size ST + max_stacks es \<le> mxs; size E + max_varss es \<le> mxl \<rbrakk>
   \<Longrightarrow> let \<tau>s = ty\<^sub>i' ST E A # compTs E A ST es in
        \<turnstile> compEs\<^sub>2 es,compxEs\<^sub>2 es 0 (size ST) [::] \<tau>s \<and>
        last \<tau>s = ty\<^sub>i' (rev Ts @ ST) E (A \<squnion> \<A>s es)"
 (*<*)
 (is "\<And>E Ts A ST. PROP ?Ps es E Ts A ST")
 proof(induct e and es rule: compxE\<^sub>2.induct compxEs\<^sub>2.induct)
   case (TryCatch e\<^sub>1 C i e\<^sub>2)
   hence [simp]: "i = size E" by simp
   have wt\<^sub>1: "P,E \<turnstile>\<^sub>1 e\<^sub>1 :: T" and wt\<^sub>2: "P,E@[Class C] \<turnstile>\<^sub>1 e\<^sub>2 :: T"
     and "class": "is_class P C" using TryCatch by auto
   let ?A\<^sub>1 = "A \<squnion> \<A> e\<^sub>1" let ?A\<^sub>i = "A \<squnion> \<lfloor>{i}\<rfloor>" let ?E\<^sub>i = "E @ [Class C]"
   let ?\<tau> = "ty\<^sub>i' ST E A" let ?\<tau>s\<^sub>1 = "compT E A ST e\<^sub>1"
   let ?\<tau>\<^sub>1 = "ty\<^sub>i' (T#ST) E ?A\<^sub>1" let ?\<tau>\<^sub>2 = "ty\<^sub>i' (Class C#ST) E A"
   let ?\<tau>\<^sub>3 = "ty\<^sub>i' ST ?E\<^sub>i ?A\<^sub>i" let ?\<tau>s\<^sub>2 = "compT ?E\<^sub>i ?A\<^sub>i ST e\<^sub>2"
   let ?\<tau>\<^sub>2' = "ty\<^sub>i' (T#ST) ?E\<^sub>i (?A\<^sub>i \<squnion> \<A> e\<^sub>2)"
   let ?\<tau>' = "ty\<^sub>i' (T#ST) E (A \<squnion> \<A> e\<^sub>1 \<sqinter> (\<A> e\<^sub>2 \<ominus> i))"
   let ?go = "Goto (int(size(compE\<^sub>2 e\<^sub>2)) + 2)"
   have "PROP ?P e\<^sub>2 ?E\<^sub>i T ?A\<^sub>i ST" by fact
   hence "\<turnstile> compE\<^sub>2 e\<^sub>2,compxE\<^sub>2 e\<^sub>2 0 (size ST) [::] (?\<tau>\<^sub>3 # ?\<tau>s\<^sub>2) @ [?\<tau>\<^sub>2']"
     using TryCatch.prems by(auto simp:after_def)
   also have "?A\<^sub>i \<squnion> \<A> e\<^sub>2 = (A \<squnion> \<A> e\<^sub>2) \<squnion> \<lfloor>{size E}\<rfloor>"
     by(fastforce simp:hyperset_defs)
   also have "P \<turnstile> ty\<^sub>i' (T#ST) ?E\<^sub>i \<dots> \<le>' ty\<^sub>i' (T#ST) E (A \<squnion> \<A> e\<^sub>2)"
     by(simp add:hyperset_defs ty\<^sub>l_incr ty\<^sub>i'_def)
   also have "P \<turnstile> \<dots> \<le>' ty\<^sub>i' (T#ST) E (A \<squnion> \<A> e\<^sub>1 \<sqinter> (\<A> e\<^sub>2 \<ominus> i))"
     by(auto intro!: ty\<^sub>l_antimono simp:hyperset_defs ty\<^sub>i'_def)
   also have "(?\<tau>\<^sub>3 # ?\<tau>s\<^sub>2) @ [?\<tau>'] = ?\<tau>\<^sub>3 # ?\<tau>s\<^sub>2 @ [?\<tau>']" by simp
   also have "\<turnstile> [Store i],[] [::] ?\<tau>\<^sub>2 # [] @ [?\<tau>\<^sub>3]"
     using TryCatch.prems
     by(auto simp:nth_list_update wt_defs ty\<^sub>i'_def ty\<^sub>l_def
       list_all2_conv_all_nth hyperset_defs)
   also have "[] @ (?\<tau>\<^sub>3 # ?\<tau>s\<^sub>2 @ [?\<tau>']) = (?\<tau>\<^sub>3 # ?\<tau>s\<^sub>2 @ [?\<tau>'])" by simp
   also have "P,T\<^sub>r,mxs,size(compE\<^sub>2 e\<^sub>2)+3,[] \<turnstile> ?go,0 :: ?\<tau>\<^sub>1#?\<tau>\<^sub>2#?\<tau>\<^sub>3#?\<tau>s\<^sub>2 @ [?\<tau>']" using wt\<^sub>2
     by (auto simp: hyperset_defs ty\<^sub>i'_def wt_defs nth_Cons nat_add_distrib
       fun_of_def intro: ty\<^sub>l_antimono list_all2_refl split:nat.split)
   also have "\<turnstile> compE\<^sub>2 e\<^sub>1,compxE\<^sub>2 e\<^sub>1 0 (size ST) [::] ?\<tau> # ?\<tau>s\<^sub>1 @ [?\<tau>\<^sub>1]"
     using TryCatch by(auto simp:after_def)
   also have "?\<tau> # ?\<tau>s\<^sub>1 @ ?\<tau>\<^sub>1 # ?\<tau>\<^sub>2 # ?\<tau>\<^sub>3 # ?\<tau>s\<^sub>2 @ [?\<tau>'] =
              (?\<tau> # ?\<tau>s\<^sub>1 @ [?\<tau>\<^sub>1]) @ ?\<tau>\<^sub>2 # ?\<tau>\<^sub>3 # ?\<tau>s\<^sub>2 @ [?\<tau>']" by simp
   also have "compE\<^sub>2 e\<^sub>1 @ ?go  # [Store i] @ compE\<^sub>2 e\<^sub>2 =
              (compE\<^sub>2 e\<^sub>1 @ [?go]) @ (Store i # compE\<^sub>2 e\<^sub>2)" by simp
   also 
   let "?Q \<tau>" = "\<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> 
     size ST \<le> size ST' \<and> P \<turnstile> Some (drop (size ST' - size ST) ST',LT') \<le>' ty\<^sub>i' ST E A"
   {
     have "?Q (ty\<^sub>i' ST E A)" by (clarsimp simp add: ty\<^sub>i'_def)
     moreover have "?Q (ty\<^sub>i' (T # ST) E ?A\<^sub>1)" 
       by (fastforce simp add: ty\<^sub>i'_def hyperset_defs intro!: ty\<^sub>l_antimono)
     moreover have "\<And>\<tau>. \<tau> \<in> set (compT E A ST e\<^sub>1) \<Longrightarrow> ?Q \<tau>" using TryCatch.prems
       by clarsimp (frule compT_ST_prefix,
                    fastforce dest!: compT_LT_prefix simp add: ty\<^sub>i'_def)
     ultimately
     have "\<forall>\<tau>\<in>set (ty\<^sub>i' ST E A # compT E A ST e\<^sub>1 @ [ty\<^sub>i' (T # ST) E ?A\<^sub>1]). ?Q \<tau>" 
       by auto
   }
   also from TryCatch.prems max_stack1[OF wt\<^sub>1] have "size ST + 1 \<le> mxs" by auto
   ultimately show ?case using wt\<^sub>1 wt\<^sub>2 TryCatch.prems "class"
     by (simp add:after_def)
 next
   case new thus ?case by(auto simp add:after_def wt_New)
 next
   case (BinOp e\<^sub>1 bop e\<^sub>2) 
   let ?op = "case bop of Eq \<Rightarrow> [CmpEq] | Add \<Rightarrow> [IAdd]"
   have T: "P,E \<turnstile>\<^sub>1 e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 :: T" by fact
   then obtain T\<^sub>1 T\<^sub>2 where T\<^sub>1: "P,E \<turnstile>\<^sub>1 e\<^sub>1 :: T\<^sub>1" and T\<^sub>2: "P,E \<turnstile>\<^sub>1 e\<^sub>2 :: T\<^sub>2" and 
     bopT: "case bop of Eq \<Rightarrow> (P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<or> P \<turnstile> T\<^sub>2 \<le> T\<^sub>1) \<and> T = Boolean 
                     | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer" by auto
   let ?A\<^sub>1 = "A \<squnion> \<A> e\<^sub>1" let ?A\<^sub>2 = "?A\<^sub>1 \<squnion> \<A> e\<^sub>2"
   let ?\<tau> = "ty\<^sub>i' ST E A" let ?\<tau>s\<^sub>1 = "compT E A ST e\<^sub>1"
   let ?\<tau>\<^sub>1 = "ty\<^sub>i' (T\<^sub>1#ST) E ?A\<^sub>1" let ?\<tau>s\<^sub>2 = "compT E ?A\<^sub>1 (T\<^sub>1#ST) e\<^sub>2"
   let ?\<tau>\<^sub>2 = "ty\<^sub>i' (T\<^sub>2#T\<^sub>1#ST) E ?A\<^sub>2" let ?\<tau>' = "ty\<^sub>i' (T#ST) E ?A\<^sub>2"
   from bopT have "\<turnstile> ?op,[] [::] [?\<tau>\<^sub>2,?\<tau>']" 
     by (cases bop) (auto simp add: wt_CmpEq wt_IAdd)
   also have "PROP ?P e\<^sub>2 E T\<^sub>2 ?A\<^sub>1 (T\<^sub>1#ST)" by fact
   with BinOp.prems T\<^sub>2 
   have "\<turnstile> compE\<^sub>2 e\<^sub>2, compxE\<^sub>2 e\<^sub>2 0 (size (T\<^sub>1#ST)) [::] ?\<tau>\<^sub>1#?\<tau>s\<^sub>2@[?\<tau>\<^sub>2]" 
     by (auto simp: after_def)
   also from BinOp T\<^sub>1 have "\<turnstile> compE\<^sub>2 e\<^sub>1, compxE\<^sub>2 e\<^sub>1 0 (size ST) [::] ?\<tau>#?\<tau>s\<^sub>1@[?\<tau>\<^sub>1]" 
     by (auto simp: after_def)
   finally show ?case using T T\<^sub>1 T\<^sub>2 by (simp add: after_def hyperUn_assoc)
 next
   case (Cons_exp e es)
   have "P,E \<turnstile>\<^sub>1 e # es [::] Ts" by fact
   then obtain T\<^sub>e Ts' where 
     T\<^sub>e: "P,E \<turnstile>\<^sub>1 e :: T\<^sub>e" and Ts': "P,E \<turnstile>\<^sub>1 es [::] Ts'" and
     Ts: "Ts = T\<^sub>e#Ts'" by auto
   let ?A\<^sub>e = "A \<squnion> \<A> e"  
   let ?\<tau> = "ty\<^sub>i' ST E A" let ?\<tau>s\<^sub>e = "compT E A ST e"  
   let ?\<tau>\<^sub>e = "ty\<^sub>i' (T\<^sub>e#ST) E ?A\<^sub>e" let ?\<tau>s' = "compTs E ?A\<^sub>e (T\<^sub>e#ST) es"
   let ?\<tau>s = "?\<tau> # ?\<tau>s\<^sub>e @ (?\<tau>\<^sub>e # ?\<tau>s')"
   have Ps: "PROP ?Ps es E Ts' ?A\<^sub>e (T\<^sub>e#ST)" by fact
   with Cons_exp.prems T\<^sub>e Ts'
   have "\<turnstile> compEs\<^sub>2 es, compxEs\<^sub>2 es 0 (size (T\<^sub>e#ST)) [::] ?\<tau>\<^sub>e#?\<tau>s'" by (simp add: after_def)
   also from Cons_exp T\<^sub>e have "\<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (size ST) [::] ?\<tau>#?\<tau>s\<^sub>e@[?\<tau>\<^sub>e]" 
     by (auto simp: after_def)
   moreover
   from Ps Cons_exp.prems T\<^sub>e Ts' Ts
   have "last ?\<tau>s = ty\<^sub>i' (rev Ts@ST) E (?A\<^sub>e \<squnion> \<A>s es)" by simp
   ultimately show ?case using T\<^sub>e by (simp add: after_def hyperUn_assoc)
 next
   case (FAss e\<^sub>1 F D e\<^sub>2)
   hence Void: "P,E \<turnstile>\<^sub>1 e\<^sub>1\<bullet>F{D} := e\<^sub>2 :: Void" by auto
   then obtain C T T' where    
     C: "P,E \<turnstile>\<^sub>1 e\<^sub>1 :: Class C" and sees: "P \<turnstile> C sees F,NonStatic:T in D" and
     T': "P,E \<turnstile>\<^sub>1 e\<^sub>2 :: T'" and T'_T: "P \<turnstile> T' \<le> T" by auto
   let ?A\<^sub>1 = "A \<squnion> \<A> e\<^sub>1" let ?A\<^sub>2 = "?A\<^sub>1 \<squnion> \<A> e\<^sub>2"  
   let ?\<tau> = "ty\<^sub>i' ST E A" let ?\<tau>s\<^sub>1 = "compT E A ST e\<^sub>1"
   let ?\<tau>\<^sub>1 = "ty\<^sub>i' (Class C#ST) E ?A\<^sub>1" let ?\<tau>s\<^sub>2 = "compT E ?A\<^sub>1 (Class C#ST) e\<^sub>2"
   let ?\<tau>\<^sub>2 = "ty\<^sub>i' (T'#Class C#ST) E ?A\<^sub>2" let ?\<tau>\<^sub>3 = "ty\<^sub>i' ST E ?A\<^sub>2"
   let ?\<tau>' = "ty\<^sub>i' (Void#ST) E ?A\<^sub>2"
   from FAss.prems sees T'_T 
   have "\<turnstile> [Putfield F D,Push Unit],[] [::] [?\<tau>\<^sub>2,?\<tau>\<^sub>3,?\<tau>']"
     by (fastforce simp add: wt_Push wt_Put)
   also have "PROP ?P e\<^sub>2 E T' ?A\<^sub>1 (Class C#ST)" by fact
   with FAss.prems T' 
   have "\<turnstile> compE\<^sub>2 e\<^sub>2, compxE\<^sub>2 e\<^sub>2 0 (size ST+1) [::] ?\<tau>\<^sub>1#?\<tau>s\<^sub>2@[?\<tau>\<^sub>2]"
     by (auto simp add: after_def hyperUn_assoc) 
   also from FAss C have "\<turnstile> compE\<^sub>2 e\<^sub>1, compxE\<^sub>2 e\<^sub>1 0 (size ST) [::] ?\<tau>#?\<tau>s\<^sub>1@[?\<tau>\<^sub>1]" 
     by (auto simp add: after_def)
   finally show ?case using Void C T' by (simp add: after_def hyperUn_assoc) 
 next
   case (SFAss C F D e\<^sub>2)
   hence Void: "P,E \<turnstile>\<^sub>1 C\<bullet>\<^sub>sF{D} := e\<^sub>2 :: Void" by auto
   then obtain T T' where    
     sees: "P \<turnstile> C sees F,Static:T in D" and
     T': "P,E \<turnstile>\<^sub>1 e\<^sub>2 :: T'" and T'_T: "P \<turnstile> T' \<le> T" by auto
   let ?A\<^sub>2 = "A \<squnion> \<A> e\<^sub>2"  
   let ?\<tau> = "ty\<^sub>i' ST E A" let ?\<tau>s\<^sub>2 = "compT E A ST e\<^sub>2"
   let ?\<tau>\<^sub>2 = "ty\<^sub>i' (T'#ST) E ?A\<^sub>2" let ?\<tau>\<^sub>3 = "ty\<^sub>i' ST E ?A\<^sub>2"
   let ?\<tau>' = "ty\<^sub>i' (Void#ST) E ?A\<^sub>2"
   from SFAss.prems sees T'_T max_stack1[OF T']
   have "\<turnstile> [Putstatic C F D,Push Unit],[] [::] [?\<tau>\<^sub>2,?\<tau>\<^sub>3,?\<tau>']"
     by (fastforce simp add: wt_Push wt_PutS)
   also have "PROP ?P e\<^sub>2 E T' A ST" by fact
   with SFAss.prems T' 
   have "\<turnstile> compE\<^sub>2 e\<^sub>2, compxE\<^sub>2 e\<^sub>2 0 (size ST) [::] ?\<tau>#?\<tau>s\<^sub>2@[?\<tau>\<^sub>2]"
     by (auto simp add: after_def hyperUn_assoc)
   finally show ?case using Void T' by (simp add: after_def hyperUn_assoc) 
 next
   case Val thus ?case by(auto simp:after_def wt_Push)
 next
   case Cast thus ?case by (auto simp:after_def wt_Cast)
 next
   case (Block i T\<^sub>i e)
   let ?\<tau>s = "ty\<^sub>i' ST E A # compT (E @ [T\<^sub>i]) (A\<ominus>i) ST e"
   have IH: "PROP ?P e (E@[T\<^sub>i]) T (A\<ominus>i) ST" by fact
   hence "\<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (size ST) [::]
          ?\<tau>s @ [ty\<^sub>i' (T#ST) (E@[T\<^sub>i]) (A\<ominus>(size E) \<squnion> \<A> e)]"
     using Block.prems by (auto simp add: after_def)
   also have "P \<turnstile> ty\<^sub>i' (T # ST) (E@[T\<^sub>i]) (A \<ominus> size E \<squnion> \<A> e) \<le>'
                  ty\<^sub>i' (T # ST) (E@[T\<^sub>i]) ((A \<squnion> \<A> e) \<ominus> size E)"
      by(auto simp add:hyperset_defs intro: ty\<^sub>i'_antimono)
   also have "\<dots> = ty\<^sub>i' (T # ST) E (A \<squnion> \<A> e)" by simp
   also have "P \<turnstile> \<dots> \<le>' ty\<^sub>i' (T # ST) E (A \<squnion> (\<A> e \<ominus> i))"
      by(auto simp add:hyperset_defs intro: ty\<^sub>i'_antimono)
   finally show ?case using Block.prems by(simp add: after_def)
 next
   case Var thus ?case by(auto simp:after_def wt_Load)
 next
   case FAcc thus ?case by(auto simp:after_def wt_Get)
 next
   case SFAcc thus ?case by(auto simp: after_def wt_GetS)
 next
   case (LAss i e)
   then obtain T' where wt: "P,E \<turnstile>\<^sub>1 e :: T'" by auto
   show ?case using max_stack1[OF wt] LAss
     by(auto simp: hyper_insert_comm after_def wt_Store wt_Push)
 next
   case Nil_exp thus ?case by auto
 next
   case throw thus ?case by(auto simp add: after_def wt_Throw)
 next
   case (While e c)
   obtain Tc where wte: "P,E \<turnstile>\<^sub>1 e :: Boolean" and wtc: "P,E \<turnstile>\<^sub>1 c :: Tc"
     and [simp]: "T = Void" using While by auto
   have [simp]: "ty E (while (e) c) = Void" using While by simp
   let ?A\<^sub>0 = "A \<squnion> \<A> e" let ?A\<^sub>1 = "?A\<^sub>0 \<squnion> \<A> c"
   let ?\<tau> = "ty\<^sub>i' ST E A" let ?\<tau>s\<^sub>e = "compT E A ST e"
   let ?\<tau>\<^sub>e = "ty\<^sub>i' (Boolean#ST) E ?A\<^sub>0" let ?\<tau>\<^sub>1 = "ty\<^sub>i' ST E ?A\<^sub>0"
   let ?\<tau>s\<^sub>c = "compT E ?A\<^sub>0 ST c" let ?\<tau>\<^sub>c = "ty\<^sub>i' (Tc#ST) E ?A\<^sub>1"
   let ?\<tau>\<^sub>2 = "ty\<^sub>i' ST E ?A\<^sub>1" let ?\<tau>' = "ty\<^sub>i' (Void#ST) E ?A\<^sub>0"
   let ?\<tau>s = "(?\<tau> # ?\<tau>s\<^sub>e @ [?\<tau>\<^sub>e]) @ ?\<tau>\<^sub>1 # ?\<tau>s\<^sub>c @ [?\<tau>\<^sub>c, ?\<tau>\<^sub>2, ?\<tau>\<^sub>1, ?\<tau>']"
   have "\<turnstile> [],[] [::] [] @ ?\<tau>s" by(simp add:wt_instrs_def)
   also
   have "PROP ?P e E Boolean A ST" by fact
   hence "\<turnstile> compE\<^sub>2 e,compxE\<^sub>2 e 0 (size ST) [::] ?\<tau> # ?\<tau>s\<^sub>e @ [?\<tau>\<^sub>e]"
     using While.prems by (auto simp:after_def)
   also
   have "[] @ ?\<tau>s = (?\<tau> # ?\<tau>s\<^sub>e) @ ?\<tau>\<^sub>e # ?\<tau>\<^sub>1 # ?\<tau>s\<^sub>c @ [?\<tau>\<^sub>c,?\<tau>\<^sub>2,?\<tau>\<^sub>1,?\<tau>']" by simp
   also
   let ?n\<^sub>e = "size(compE\<^sub>2 e)"  let ?n\<^sub>c = "size(compE\<^sub>2 c)"
+  thm compT_sizes(1)
   let ?if = "IfFalse (int ?n\<^sub>c + 3)"
-  have "\<turnstile> [?if],[] [::] ?\<tau>\<^sub>e # ?\<tau>\<^sub>1 # ?\<tau>s\<^sub>c @ [?\<tau>\<^sub>c, ?\<tau>\<^sub>2, ?\<tau>\<^sub>1, ?\<tau>']" using wtc
-    by(simp add: wt_instr_Cons wt_instr_append wt_IfFalse
-                 nat_add_distrib split: nat_diff_split)
+  from wtc wte have "compE\<^sub>2 c \<noteq> []" and "compE\<^sub>2 e \<noteq> []" using WT\<^sub>1_nsub_RI by auto
+  then have compe2c: "length (compE\<^sub>2 c) > 0" and compe2e: "length (compE\<^sub>2 e) > 0" by auto 
+  have Suc_pred'_auxi: "\<And>n. 0 < n \<Longrightarrow> n = Suc (n - Suc 0)" using Suc_pred'[OF compe2c] by auto
+  have "\<turnstile> [?if],[] [::] ?\<tau>\<^sub>e # ?\<tau>\<^sub>1 # ?\<tau>s\<^sub>c @ [?\<tau>\<^sub>c, ?\<tau>\<^sub>2, ?\<tau>\<^sub>1, ?\<tau>']" 
+   proof-{
+      show ?thesis
+        apply (rule wt_IfFalse)
+          apply simp
+         apply simp
+        apply (subgoal_tac "length (compE\<^sub>2 c) = length (compT E (A \<squnion> \<A> e) ST c) + 1" 
+                           "nat (int (length (compE\<^sub>2 c)) + 3 - 2) > length (compT E (A \<squnion> \<A> e) ST c)")
+           apply (insert Suc_pred'_auxi[OF compe2c])
+           apply (simp add:compT_sizes(1)[OF wtc] )+          
+        done
+    }
+  qed
   also
   have "(?\<tau> # ?\<tau>s\<^sub>e) @ (?\<tau>\<^sub>e # ?\<tau>\<^sub>1 # ?\<tau>s\<^sub>c @ [?\<tau>\<^sub>c, ?\<tau>\<^sub>2, ?\<tau>\<^sub>1, ?\<tau>']) = ?\<tau>s" by simp
   also
   have "PROP ?P c E Tc ?A\<^sub>0 ST" by fact
   hence "\<turnstile> compE\<^sub>2 c,compxE\<^sub>2 c 0 (size ST) [::] ?\<tau>\<^sub>1 # ?\<tau>s\<^sub>c @ [?\<tau>\<^sub>c]"
     using While.prems wtc by (auto simp:after_def)
   also have "?\<tau>s = (?\<tau> # ?\<tau>s\<^sub>e @ [?\<tau>\<^sub>e,?\<tau>\<^sub>1] @ ?\<tau>s\<^sub>c) @ [?\<tau>\<^sub>c,?\<tau>\<^sub>2,?\<tau>\<^sub>1,?\<tau>']" by simp
   also have "\<turnstile> [Pop],[] [::] [?\<tau>\<^sub>c, ?\<tau>\<^sub>2]"  by(simp add:wt_Pop)
   also have "(?\<tau> # ?\<tau>s\<^sub>e @ [?\<tau>\<^sub>e,?\<tau>\<^sub>1] @ ?\<tau>s\<^sub>c) @ [?\<tau>\<^sub>c,?\<tau>\<^sub>2,?\<tau>\<^sub>1,?\<tau>'] = ?\<tau>s" by simp
   also let ?go = "Goto (-int(?n\<^sub>c+?n\<^sub>e+2))"
   have "P \<turnstile> ?\<tau>\<^sub>2 \<le>' ?\<tau>" by(fastforce intro: ty\<^sub>i'_antimono simp: hyperset_defs)
   hence "P,T\<^sub>r,mxs,size ?\<tau>s,[] \<turnstile> ?go,?n\<^sub>e+?n\<^sub>c+2 :: ?\<tau>s" using wte wtc
-    by(simp add: wt_Goto split: nat_diff_split)
+    proof-{
+      let ?t1 = "ty\<^sub>i' ST E A" let ?t2 = "ty\<^sub>i' (Boolean # ST) E (A \<squnion> \<A> e)" let ?t3 = "ty\<^sub>i' ST E (A \<squnion> \<A> e)"
+      let ?t4 = "[ty\<^sub>i' (Tc # ST) E (A \<squnion> \<A> e \<squnion> \<A> c), ty\<^sub>i' ST E (A \<squnion> \<A> e \<squnion> \<A> c), ty\<^sub>i' ST E (A \<squnion> \<A> e), ty\<^sub>i' (Void # ST) E (A \<squnion> \<A> e)]"
+      let ?c = " compT E (A \<squnion> \<A> e) ST c" let ?e = "compT E A ST e"     
+      
+      assume ass: "P \<turnstile> ty\<^sub>i' ST E (A \<squnion> \<A> e \<squnion> \<A> c) \<le>' ?t1"      
+      show ?thesis
+        apply (rule wt_Goto)
+        apply simp
+          apply simp
+         apply simp
+      proof-{
+          let ?s1 = "((?t1 # ?e @ [?t2]) @ ?t3 # ?c)"  
+          have len1: "length ?c = length (compE\<^sub>2 c) - 1" using compT_sizes(1)[OF wtc] by simp 
+          have len2: "length ?e = length (compE\<^sub>2 e) - 1" using compT_sizes(1)[OF wte] by simp 
+          hence "length (compE\<^sub>2 e) + length (compE\<^sub>2 c) + 2 > length ?s1" 
+            using len1 compe2c compe2e by auto
+          hence "(?s1 @ ?t4) ! (length (compE\<^sub>2 e) + length (compE\<^sub>2 c) + 2) =
+                     ?t4 ! (length (compE\<^sub>2 e) + length (compE\<^sub>2 c) + 2 - length ?s1)" 
+            by (auto simp only:nth_append split: if_splits)
+          hence "(?s1 @ ?t4) ! (length (compE\<^sub>2 e) + length (compE\<^sub>2 c) + 2) = ty\<^sub>i' ST E (A \<squnion> \<A> e \<squnion> \<A> c)" 
+            using len1 len2 compe2c compe2e by auto 
+          hence "P \<turnstile> (?s1 @ ?t4) ! (length (compE\<^sub>2 e) + length (compE\<^sub>2 c) + 2) \<le>' ty\<^sub>i' ST E A" 
+            using ass by simp
+          thus "P \<turnstile> ((?t1 # ?e @ [?t2]) @ ?t3 # ?c @ ?t4) ! (length (compE\<^sub>2 e) + length (compE\<^sub>2 c) + 2) \<le>'
+                    ((?t1 # ?e @ [?t2]) @ ?t3 # ?c @ ?t4) ! nat (int (length (compE\<^sub>2 e) + length (compE\<^sub>2 c) + 2) +
+                      - int (length (compE\<^sub>2 c) + length (compE\<^sub>2 e) + 2))"
+            by simp
+        }qed
+    }qed
   also have "?\<tau>s = (?\<tau> # ?\<tau>s\<^sub>e @ [?\<tau>\<^sub>e,?\<tau>\<^sub>1] @ ?\<tau>s\<^sub>c @ [?\<tau>\<^sub>c, ?\<tau>\<^sub>2]) @ [?\<tau>\<^sub>1, ?\<tau>']"
     by simp
   also have "\<turnstile> [Push Unit],[] [::] [?\<tau>\<^sub>1,?\<tau>']"
     using While.prems max_stack1[OF wtc] by(auto simp add:wt_Push)
   finally show ?case using wtc wte
     by (simp add:after_def)
 next
   case (Cond e e\<^sub>1 e\<^sub>2)
   obtain T\<^sub>1 T\<^sub>2 where wte: "P,E \<turnstile>\<^sub>1 e :: Boolean"
     and wt\<^sub>1: "P,E \<turnstile>\<^sub>1 e\<^sub>1 :: T\<^sub>1" and wt\<^sub>2: "P,E \<turnstile>\<^sub>1 e\<^sub>2 :: T\<^sub>2"
     and sub\<^sub>1: "P \<turnstile> T\<^sub>1 \<le> T" and sub\<^sub>2: "P \<turnstile> T\<^sub>2 \<le> T"
     using Cond by auto
+  from wte wt\<^sub>1  wt\<^sub>2 have "compE\<^sub>2 e\<^sub>1 \<noteq> []" and "compE\<^sub>2 e\<^sub>2 \<noteq> []" and "compE\<^sub>2 e \<noteq> []" using WT\<^sub>1_nsub_RI by auto
+  then have compe: "length (compE\<^sub>2 e) > 0"  
+        and compe1: "length (compE\<^sub>2 e\<^sub>1) > 0" 
+        and compe2: "length (compE\<^sub>2 e\<^sub>2) > 0" by auto 
+
+
   have [simp]: "ty E (if (e) e\<^sub>1 else e\<^sub>2) = T" using Cond by simp
   let ?A\<^sub>0 = "A \<squnion> \<A> e" let ?A\<^sub>2 = "?A\<^sub>0 \<squnion> \<A> e\<^sub>2" let ?A\<^sub>1 = "?A\<^sub>0 \<squnion> \<A> e\<^sub>1"
   let ?A' = "?A\<^sub>0 \<squnion> \<A> e\<^sub>1 \<sqinter> \<A> e\<^sub>2"
   let ?\<tau>\<^sub>2 = "ty\<^sub>i' ST E ?A\<^sub>0" let ?\<tau>' = "ty\<^sub>i' (T#ST) E ?A'"
   let ?\<tau>s\<^sub>2 = "compT E ?A\<^sub>0 ST e\<^sub>2"
   have "PROP ?P e\<^sub>2 E T\<^sub>2 ?A\<^sub>0 ST" by fact
   hence "\<turnstile> compE\<^sub>2 e\<^sub>2, compxE\<^sub>2 e\<^sub>2 0 (size ST) [::] (?\<tau>\<^sub>2#?\<tau>s\<^sub>2) @ [ty\<^sub>i' (T\<^sub>2#ST) E ?A\<^sub>2]"
     using Cond.prems wt\<^sub>2 by(auto simp add:after_def)
   also have "P \<turnstile> ty\<^sub>i' (T\<^sub>2#ST) E ?A\<^sub>2 \<le>' ?\<tau>'" using sub\<^sub>2
     by(auto simp add: hyperset_defs ty\<^sub>i'_def intro!: ty\<^sub>l_antimono)
   also
   let ?\<tau>\<^sub>3 = "ty\<^sub>i' (T\<^sub>1 # ST) E ?A\<^sub>1"
   let ?g\<^sub>2 = "Goto(int (size (compE\<^sub>2 e\<^sub>2) + 1))"
   from sub\<^sub>1 have "P,T\<^sub>r,mxs,size(compE\<^sub>2 e\<^sub>2)+2,[] \<turnstile> ?g\<^sub>2,0 :: ?\<tau>\<^sub>3#(?\<tau>\<^sub>2#?\<tau>s\<^sub>2)@[?\<tau>']" using wt\<^sub>2
     by(auto simp: hyperset_defs wt_defs nth_Cons ty\<^sub>i'_def
              split:nat.split intro!: ty\<^sub>l_antimono)
   also
   let ?\<tau>s\<^sub>1 = "compT E ?A\<^sub>0 ST e\<^sub>1"
   have "PROP ?P e\<^sub>1 E T\<^sub>1 ?A\<^sub>0 ST" by fact
   hence "\<turnstile> compE\<^sub>2 e\<^sub>1,compxE\<^sub>2 e\<^sub>1 0 (size ST) [::] ?\<tau>\<^sub>2 # ?\<tau>s\<^sub>1 @ [?\<tau>\<^sub>3]"
     using Cond.prems wt\<^sub>1 by(auto simp add:after_def)
   also
   let ?\<tau>s\<^sub>1\<^sub>2 = "?\<tau>\<^sub>2 # ?\<tau>s\<^sub>1 @ ?\<tau>\<^sub>3 # (?\<tau>\<^sub>2 # ?\<tau>s\<^sub>2) @ [?\<tau>']"
   let ?\<tau>\<^sub>1 = "ty\<^sub>i' (Boolean#ST) E ?A\<^sub>0"
   let ?g\<^sub>1 = "IfFalse(int (size (compE\<^sub>2 e\<^sub>1) + 2))"
   let ?code = "compE\<^sub>2 e\<^sub>1 @ ?g\<^sub>2 # compE\<^sub>2 e\<^sub>2"
-  have "\<turnstile> [?g\<^sub>1],[] [::] [?\<tau>\<^sub>1] @ ?\<tau>s\<^sub>1\<^sub>2" using wt\<^sub>1
-    by(simp add: wt_IfFalse nat_add_distrib split:nat_diff_split)
+
+  have len1: "length ?\<tau>s\<^sub>1 = length (compE\<^sub>2 e\<^sub>1) - 1" using compT_sizes(1)[OF wt\<^sub>1] by simp 
+  have len2: "length ?\<tau>s\<^sub>2 = length (compE\<^sub>2 e\<^sub>2) - 1" using compT_sizes(1)[OF wt\<^sub>2] by simp 
+  have len_auxi: "length (compE\<^sub>2 e\<^sub>1) - (length (compE\<^sub>2 e\<^sub>1) - Suc 0) = Suc 0" using compe1 
+    by (simp add:diff_Suc split:nat.split)
+  have "\<turnstile> [?g\<^sub>1],[] [::] [?\<tau>\<^sub>1] @ ?\<tau>s\<^sub>1\<^sub>2" 
+    proof-{
+    show ?thesis 
+      apply clarsimp
+      apply (rule wt_IfFalse)
+        apply (simp only:nat_add_distrib)
+       apply simp
+      apply (auto simp only:nth_append split:if_splits)     
+        apply (simp add:len1)
+       apply (simp only: len1 compe1)
+      apply (simp add:len1 len2 compe1 compe2 )
+      apply (insert len_auxi)
+      apply simp
+      done
+  }qed
   also (wt_instrs_ext2) have "[?\<tau>\<^sub>1] @ ?\<tau>s\<^sub>1\<^sub>2 = ?\<tau>\<^sub>1 # ?\<tau>s\<^sub>1\<^sub>2" by simp also
   let ?\<tau> = "ty\<^sub>i' ST E A"
   have "PROP ?P e E Boolean A ST" by fact
   hence "\<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (size ST) [::] ?\<tau> # compT E A ST e @ [?\<tau>\<^sub>1]"
     using Cond.prems wte by(auto simp add:after_def)
   finally show ?case using wte wt\<^sub>1 wt\<^sub>2 by(simp add:after_def hyperUn_assoc)
 next
   case (Call e M es)
   obtain C D Ts m Ts' where C: "P,E \<turnstile>\<^sub>1 e :: Class C"
     and "method": "P \<turnstile> C sees M,NonStatic:Ts \<rightarrow> T = m in D"
     and wtes: "P,E \<turnstile>\<^sub>1 es [::] Ts'" and subs: "P \<turnstile> Ts' [\<le>] Ts"
     using Call.prems by auto
   from wtes have same_size: "size es = size Ts'" by(rule WTs\<^sub>1_same_size)
   let ?A\<^sub>0 = "A \<squnion> \<A> e" let ?A\<^sub>1 = "?A\<^sub>0 \<squnion> \<A>s es"
   let ?\<tau> = "ty\<^sub>i' ST E A" let ?\<tau>s\<^sub>e = "compT E A ST e"
   let ?\<tau>\<^sub>e = "ty\<^sub>i' (Class C # ST) E ?A\<^sub>0"
   let ?\<tau>s\<^sub>e\<^sub>s = "compTs E ?A\<^sub>0 (Class C # ST) es"
   let ?\<tau>\<^sub>1 = "ty\<^sub>i' (rev Ts' @ Class C # ST) E ?A\<^sub>1"
   let ?\<tau>' = "ty\<^sub>i' (T # ST) E ?A\<^sub>1"
   have "\<turnstile> [Invoke M (size es)],[] [::] [?\<tau>\<^sub>1,?\<tau>']"
     by(rule wt_Invoke[OF same_size "method" subs])
   also
   have "PROP ?Ps es E Ts' ?A\<^sub>0 (Class C # ST)" by fact
   hence "\<turnstile> compEs\<^sub>2 es,compxEs\<^sub>2 es 0 (size ST+1) [::] ?\<tau>\<^sub>e # ?\<tau>s\<^sub>e\<^sub>s"
         "last (?\<tau>\<^sub>e # ?\<tau>s\<^sub>e\<^sub>s) = ?\<tau>\<^sub>1"
     using Call.prems wtes by(auto simp add:after_def)
   also have "(?\<tau>\<^sub>e # ?\<tau>s\<^sub>e\<^sub>s) @ [?\<tau>'] = ?\<tau>\<^sub>e # ?\<tau>s\<^sub>e\<^sub>s @ [?\<tau>']" by simp
   also have "\<turnstile> compE\<^sub>2 e,compxE\<^sub>2 e 0 (size ST) [::] ?\<tau> # ?\<tau>s\<^sub>e @ [?\<tau>\<^sub>e]"
     using Call C by(auto simp add:after_def)
   finally show ?case using Call.prems C wtes by(simp add:after_def hyperUn_assoc)
 next
   case (SCall C M es)
   obtain D Ts m Ts' where "method": "P \<turnstile> C sees M,Static:Ts \<rightarrow> T = m in D"
     and wtes: "P,E \<turnstile>\<^sub>1 es [::] Ts'" and subs: "P \<turnstile> Ts' [\<le>] Ts"
     using SCall.prems by auto
   from SCall.prems(1) have nclinit: "M \<noteq> clinit" by auto
   from wtes have same_size: "size es = size Ts'" by(rule WTs\<^sub>1_same_size)
   have mxs: "length ST < mxs" using WT\<^sub>1_nsub_RI[OF SCall.prems(1)] SCall.prems(4) by simp
   let ?A\<^sub>1 = "A \<squnion> \<A>s es"
   let ?\<tau> = "ty\<^sub>i' ST E A"
   let ?\<tau>s\<^sub>e\<^sub>s = "compTs E A ST es"
   let ?\<tau>\<^sub>1 = "ty\<^sub>i' (rev Ts' @ ST) E ?A\<^sub>1"
   let ?\<tau>' = "ty\<^sub>i' (T # ST) E ?A\<^sub>1"
   have "\<turnstile> [Invokestatic C M (size es)],[] [::] [?\<tau>\<^sub>1,?\<tau>']"
     by(rule wt_Invokestatic[OF mxs same_size nclinit "method" subs])
   also
   have "PROP ?Ps es E Ts' A ST" by fact
   hence "\<turnstile> compEs\<^sub>2 es,compxEs\<^sub>2 es 0 (size ST) [::] ?\<tau> # ?\<tau>s\<^sub>e\<^sub>s"
         "last (?\<tau> # ?\<tau>s\<^sub>e\<^sub>s) = ?\<tau>\<^sub>1"
     using SCall.prems wtes by(auto simp add:after_def)
   also have "(?\<tau> # ?\<tau>s\<^sub>e\<^sub>s) @ [?\<tau>'] = ?\<tau> # ?\<tau>s\<^sub>e\<^sub>s @ [?\<tau>']" by simp
   finally show ?case using SCall.prems wtes by(simp add:after_def hyperUn_assoc)
 next
   case Seq thus ?case
     by(auto simp:after_def)
       (fastforce simp:wt_Push wt_Pop hyperUn_assoc
                 intro:wt_instrs_app2 wt_instrs_Cons)
 next
   case (INIT C Cs b e)
   have "P,E \<turnstile>\<^sub>1 INIT C (Cs,b) \<leftarrow> e :: T" by fact
   thus ?case using WT\<^sub>1_nsub_RI by simp
 next
   case (RI C e' Cs e)
   have "P,E \<turnstile>\<^sub>1 RI (C,e') ; Cs \<leftarrow> e :: T" by fact
   thus ?case using WT\<^sub>1_nsub_RI by simp
 qed
 (*>*)
 
 
 lemma [simp]: "types (compP f P) = types P"
 (*<*)by auto(*>*)
 
 lemma [simp]: "states (compP f P) mxs mxl = states P mxs mxl"
 (*<*)by (simp add: JVM_states_unfold)(*>*)
 
 lemma [simp]: "app\<^sub>i (i, compP f P, pc, mpc, T, \<tau>) = app\<^sub>i (i, P, pc, mpc, T, \<tau>)"
 (*<*)(is "?A = ?B")
 proof -
   obtain ST LT where \<tau>: "\<tau> = (ST, LT)" by(cases \<tau>) simp
   then show ?thesis proof(cases i)
     case Invoke show ?thesis
     proof(rule iffI)
       assume ?A then show ?B using Invoke \<tau>
         by auto (fastforce dest!: sees_method_compPD)
     next
       assume ?B then show ?A using Invoke \<tau>
         by auto (force dest: sees_method_compP)
     qed
   next
     case (Invokestatic x111 x112 x113) show ?thesis
     proof(rule iffI)
       assume ?A then show ?B using Invokestatic \<tau>
         by auto (fastforce dest!: sees_method_compPD)
     next
       assume ?B then show ?A using Invokestatic \<tau>
         by auto (force dest: sees_method_compP)
     qed
   qed auto
 qed
 (*>*)
   
 lemma [simp]: "is_relevant_entry (compP f P) i = is_relevant_entry P i"
 (*<*)
 proof -
   { fix pc e
     have "is_relevant_entry (compP f P) i pc e = is_relevant_entry P i pc e"
       by(cases i) (auto simp: is_relevant_entry_def)
   }
   then show ?thesis by fast
 qed
 (*>*)
 
 lemma [simp]: "relevant_entries (compP f P) i pc xt = relevant_entries P i pc xt"
 (*<*) by (simp add: relevant_entries_def)(*>*)
 
 lemma [simp]: "app i (compP f P) mpc T pc mxl xt \<tau> = app i P mpc T pc mxl xt \<tau>"
 (*<*)
 by (simp add: app_def xcpt_app_def eff_def xcpt_eff_def norm_eff_def)
    (fastforce simp add: image_def)
 (*>*)
 
 lemma [simp]:
 assumes "app i P mpc T pc mxl xt \<tau>"
 shows "eff i (compP f P) pc xt \<tau> = eff i P pc xt \<tau>"
 (*<*)
 using assms
 proof(clarsimp simp: eff_def norm_eff_def xcpt_eff_def app_def, cases i)
 qed auto
 (*>*)
 
 lemma [simp]: "subtype (compP f P) = subtype P"
 (*<*)by (rule ext)+ simp(*>*)
   
 lemma [simp]: "compP f P \<turnstile> \<tau> \<le>' \<tau>' = P \<turnstile> \<tau> \<le>' \<tau>'"
 (*<*) by (simp add: sup_state_opt_def sup_state_def sup_ty_opt_def)(*>*)
 
 lemma [simp]: "compP f P,T,mpc,mxl,xt \<turnstile> i,pc :: \<tau>s = P,T,mpc,mxl,xt \<turnstile> i,pc :: \<tau>s"
 (*<*)by (simp add: wt_instr_def cong: conj_cong)(*>*)
 
 declare TC1.compT_sizes[simp]  TC0.ty_def2[simp]
 
 context TC2
 begin
 
 lemma compT_method_NonStatic:
   fixes e and A and C and Ts and mxl\<^sub>0
   defines [simp]: "E \<equiv> Class C # Ts"
     and [simp]: "A \<equiv> \<lfloor>{..size Ts}\<rfloor>"
     and [simp]: "A' \<equiv> A \<squnion> \<A> e"
     and [simp]: "mxl\<^sub>0 \<equiv> max_vars e"
   assumes mxs: "max_stack e = mxs"
     and mxl: "Suc (length Ts + max_vars e) = mxl"
   assumes wf: "wf_prog p P" and wte: "P,E \<turnstile>\<^sub>1 e :: T" and \<D>: "\<D> e A"
     and \<B>: "\<B> e (size E)" and E_P: "set E \<subseteq> types P" and wid: "P \<turnstile> T \<le> T\<^sub>r"
   shows "wt_method (compP\<^sub>2 P) C NonStatic Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return])
     (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)"
 (*<*)(is "wt_method ?P C ?b Ts T\<^sub>r mxs mxl\<^sub>0 ?is ?xt ?\<tau>s")
 proof -
   let ?n = "length E + mxl\<^sub>0"
   have wt_compE: "P,T\<^sub>r,mxs \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::]
         TC0.ty\<^sub>i' ?n [] E A # TC1.compT P ?n E A [] e @[TC0.after P ?n E A [] e]"
     using mxs TC2.compT_wt_instrs [OF wte \<D> \<B>, of "[]" mxs ?n T\<^sub>r] by simp
 
   have "OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl"
     using mxs WT\<^sub>1_is_type[OF wf wte E_P] max_stack1[OF wte] OK_ty\<^sub>i'_in_statesI[OF E_P]
       by simp
   moreover have "OK ` set (compT E A [] e) \<subseteq> states P mxs mxl"
     using mxs mxl wid compT_states(1)[OF wf wte E_P] by simp
   ultimately have "check_types ?P mxs ?n (map OK ?\<tau>s)"
     using mxl wte E_P by (simp add: compT\<^sub>a_def after_def check_types_def)
   moreover have "wt_start ?P C ?b Ts mxl\<^sub>0 ?\<tau>s" using mxl
     by (auto simp: wt_start_def ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth nth_Cons
              split: nat.split)
   moreover {
     fix pc assume pc: "pc < size ?is"
     then have "?P,T\<^sub>r,mxs,size ?is,?xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
     proof(cases "pc < length (compE\<^sub>2 e)")
       case True
       then show ?thesis using mxs wte wt_compE
         by (clarsimp simp: compT\<^sub>a_def mxl after_def wt_instrs_def)
     next
       case False
       have "length (compE\<^sub>2 e) = pc" using less_antisym[OF False] pc by simp
       then show ?thesis using mxl wte E_P wid
         by (clarsimp simp: compT\<^sub>a_def after_def wt_defs xcpt_app_pcs xcpt_eff_pcs ty\<^sub>i'_def)
     qed
   }
   moreover have "0 < size ?is" and "size ?\<tau>s = size ?is"
     using wte by (simp_all add: compT\<^sub>a_def)
   ultimately show ?thesis by(simp add: wt_method_def)
 qed
 (*>*)
 
 lemma compT_method_Static:
   fixes e and A and C and Ts and mxl\<^sub>0
   defines [simp]: "E \<equiv> Ts"
     and [simp]: "A \<equiv> \<lfloor>{..<size Ts}\<rfloor>"
     and [simp]: "A' \<equiv> A \<squnion> \<A> e"
     and [simp]: "mxl\<^sub>0 \<equiv> max_vars e"
   assumes mxs: "max_stack e = mxs"
     and mxl: "length Ts + max_vars e = mxl"
   assumes wf: "wf_prog p P" and wte: "P,E \<turnstile>\<^sub>1 e :: T" and \<D>: "\<D> e A"
     and \<B>: "\<B> e (size E)" and E_P: "set E \<subseteq> types P" and wid: "P \<turnstile> T \<le> T\<^sub>r"
   shows "wt_method (compP\<^sub>2 P) C Static Ts T\<^sub>r mxs mxl\<^sub>0 (compE\<^sub>2 e @ [Return])
     (compxE\<^sub>2 e 0 0) (ty\<^sub>i' [] E A # compT\<^sub>a E A [] e)"
 (*<*)(is "wt_method ?P C ?b Ts T\<^sub>r mxs mxl\<^sub>0 ?is ?xt ?\<tau>s")
 proof -
   let ?n = "length E + mxl\<^sub>0"
   have wt_compE: "P,T\<^sub>r,mxs \<turnstile> compE\<^sub>2 e, compxE\<^sub>2 e 0 (length []) [::]
         TC0.ty\<^sub>i' ?n [] E A # TC1.compT P ?n E A [] e @[TC0.after P ?n E A [] e]"
     using mxs TC2.compT_wt_instrs [OF wte \<D> \<B>, of "[]" mxs ?n T\<^sub>r] by simp
 
   have "OK (ty\<^sub>i' [T] E A') \<in> states P mxs mxl"
     using mxs WT\<^sub>1_is_type[OF wf wte E_P] max_stack1[OF wte] OK_ty\<^sub>i'_in_statesI[OF E_P]
       by simp
   moreover have "OK ` set (compT E A [] e) \<subseteq> states P mxs mxl"
     using mxs mxl wid compT_states(1)[OF wf wte E_P] by simp
   ultimately have "check_types ?P mxs ?n (map OK ?\<tau>s)"
     using mxl wte E_P by (simp add: compT\<^sub>a_def after_def check_types_def)
   moreover have "wt_start ?P C ?b Ts mxl\<^sub>0 ?\<tau>s" using mxl
     by (auto simp: wt_start_def ty\<^sub>i'_def ty\<^sub>l_def list_all2_conv_all_nth nth_Cons
              split: nat.split)
   moreover {
     fix pc assume pc: "pc < size ?is"
     then have "?P,T\<^sub>r,mxs,size ?is,?xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
     proof(cases "pc < length (compE\<^sub>2 e)")
       case True
       then show ?thesis using mxs wte wt_compE
         by (clarsimp simp: compT\<^sub>a_def mxl after_def wt_instrs_def)
     next
       case False
       have "length (compE\<^sub>2 e) = pc" using less_antisym[OF False] pc by simp
       then show ?thesis using mxl wte E_P wid
         by (clarsimp simp: compT\<^sub>a_def after_def wt_defs xcpt_app_pcs xcpt_eff_pcs ty\<^sub>i'_def)
     qed
   }
   moreover have "0 < size ?is" and "size ?\<tau>s = size ?is"
     using wte by (simp_all add: compT\<^sub>a_def)
   ultimately show ?thesis by(simp add: wt_method_def)
 qed
 (*>*)
 
 end
 
 definition compTP :: "J\<^sub>1_prog \<Rightarrow> ty\<^sub>P" where
   "compTP P C M = (
   let (D,b,Ts,T,e) = method P C M;
        E = case b of Static \<Rightarrow> Ts | NonStatic \<Rightarrow> Class C # Ts;
        A = case b of Static \<Rightarrow> \<lfloor>{..<size Ts}\<rfloor> | NonStatic \<Rightarrow> \<lfloor>{..size Ts}\<rfloor>;
        mxl = (case b of Static \<Rightarrow> 0 | NonStatic \<Rightarrow> 1) + size Ts + max_vars e
   in  (TC0.ty\<^sub>i' mxl [] E A # TC1.compT\<^sub>a P mxl E A [] e))"
 
 theorem wt_compP\<^sub>2:
 assumes wf: "wf_J\<^sub>1_prog P" shows "wf_jvm_prog (compP\<^sub>2 P)"
 (*<*)
 proof -
   let ?\<Phi> = "compTP P" and ?f = compMb\<^sub>2
   let ?wf\<^sub>2 = "\<lambda>P C (M, b, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
               wt_method P C b Ts T\<^sub>r mxs mxl\<^sub>0 is xt (?\<Phi> C M)"
     and ?P = "compP ?f P"
   { fix C M b Ts T m let ?md = "(M,b,Ts,T,m)::expr\<^sub>1 mdecl"
     assume cM: "P \<turnstile> C sees M, b :  Ts\<rightarrow>T = m in C"
       and wfm: "wf_mdecl wf_J\<^sub>1_mdecl P C ?md"
     then have Ts_types: "\<forall>T'\<in>set Ts. is_type P T'"
      and T_type: "is_type P T" and wfm\<^sub>1: "wf_J\<^sub>1_mdecl P C ?md"
       by(simp_all add: wf_mdecl_def)
     have Ts_P: "set Ts \<subseteq> types P"  using sees_wf_mdecl[OF wf cM]
       by (clarsimp simp: wf_mdecl_def)
     then have CTs_P: "is_class P C \<and> set Ts \<subseteq> types P"
       using sees_method_is_class[OF cM] by simp
 
     have "?wf\<^sub>2 ?P C (M,b,Ts,T,?f b m)"
     proof(cases b)
       case Static
       then obtain T' where wte: "P,Ts \<turnstile>\<^sub>1 m :: T'" and wid: "P \<turnstile> T' \<le> T"
          and \<D>: "\<D> m \<lfloor>{..<size Ts}\<rfloor>" and \<B>: "\<B> m (size Ts)"
         using wfm\<^sub>1 by(auto simp: wf_mdecl_def)
       show ?thesis using Static cM TC2.compT_method_Static [OF _ _ wf wte \<D> \<B> Ts_P wid]
         by(simp add: compTP_def)
     next
       case NonStatic
       then obtain T' where wte: "P,Class C#Ts \<turnstile>\<^sub>1 m :: T'" and wid: "P \<turnstile> T' \<le> T"
          and \<D>: "\<D> m \<lfloor>{..size Ts}\<rfloor>" and \<B>: "\<B> m (Suc (size Ts))"
         using wfm\<^sub>1 by(auto simp: wf_mdecl_def)
       have Ts_P: "set Ts \<subseteq> types P"  using sees_wf_mdecl[OF wf cM]
         by (fastforce simp: wf_mdecl_def intro: sees_method_is_class)
       show ?thesis using NonStatic cM
           TC2.compT_method_NonStatic [simplified, OF _ _ wf wte \<D> \<B> CTs_P wid]
         by(simp add: compTP_def)
     qed
     then have "wf_mdecl ?wf\<^sub>2 ?P C (M, b, Ts, T, ?f b m)"
       using Ts_types T_type by(simp add: wf_mdecl_def)
   }
   then have "wf_prog ?wf\<^sub>2 (compP ?f P)" by(rule wf_prog_compPI[OF _ wf])
   then show ?thesis by (simp add: wf_jvm_prog_def wf_jvm_prog_phi_def) fast
 qed
 (*>*)
 
 theorem wt_J2JVM:
   "wf_J_prog P \<Longrightarrow> wf_jvm_prog (J2JVM P)"
 (*<*)
 by(simp only:o_def J2JVM_def)
   (blast intro:wt_compP\<^sub>2 compP\<^sub>1_pres_wf)
 
 end