diff --git a/thys/Jinja/BV/BVExec.thy b/thys/Jinja/BV/BVExec.thy
--- a/thys/Jinja/BV/BVExec.thy
+++ b/thys/Jinja/BV/BVExec.thy
@@ -1,233 +1,247 @@
 (*  Title:      HOL/MicroJava/BV/JVM.thy
 
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
 
 section \<open>Kildall for the JVM \label{sec:JVM}\<close>
 
 theory BVExec
 imports "../DFA/Abstract_BV" TF_JVM
 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> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
                  instr list \<Rightarrow> ex_table \<Rightarrow> bool"
 where
   "wt_kildall P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<equiv>
    0 < size is \<and> 
    (let first  = Some ([],[OK (Class C')]@(map OK Ts)@(replicate mxl\<^sub>0 Err));
         start  = OK first#(replicate (size is - 1) (OK None));
         result = kiljvm P mxs (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,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). wt_kildall P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt) P"
 
 
 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)
-  apply (rule is_bcv_kildall)
-       apply simp apply (rule Semilat.intro)
-       apply (fold sl_def2)
-       apply (erule semilat_JVM)
-      apply simp
-      apply blast
-     apply (simp add: JVM_le_unfold)
-    apply (rule exec_pres_type)
-   apply (rule bounded_step)
-  apply (erule step_mono)
-  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
 (*<*)
-  apply (simp add: JVM_states_unfold) 
-  apply (force intro!: listI list_appendI dest!: in_set_replicate)
-  done   
+ by (force simp add: JVM_states_unfold intro!: listI list_appendI
+           dest!: in_set_replicate)
 (*>*)
 
 
 theorem (in start_context) wt_kil_correct:
   assumes wtk: "wt_kildall P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
   shows "\<exists>\<tau>s. wt_method P C 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" 
     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 Ts mxl\<^sub>0 (map ok_val \<tau>s')" using l instrs
       by (unfold wt_start_def) 
          (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 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)
   thus ?thesis by blast
 qed
 (*>*)
 
 
 theorem (in start_context) wt_kil_complete:
   assumes wtm: "wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
   shows "wt_kildall P C 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 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)
 
   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 (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 Ts T\<^sub>r mxs mxl\<^sub>0 is xt" by (unfold wt_kildall_def) simp
 qed
 (*>*)
 
 
 theorem jvm_kildall_correct:
   "wf_jvm_prog\<^sub>k P = wf_jvm_prog P"
 (*<*)
-proof 
+proof -
   let ?\<Phi> = "\<lambda>C M. let (C,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)) = method P C M in 
               SOME \<tau>s. wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
+  let ?A = "\<lambda>P C' (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt). wt_kildall P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
+  let ?B\<^sub>\<Phi> = "\<lambda>\<Phi>. (\<lambda>P C (M,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
+                wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M))"
 
-  \<comment> \<open>soundness\<close>
-  assume wt: "wf_jvm_prog\<^sub>k P"
-  hence "wf_jvm_prog\<^bsub>?\<Phi>\<^esub> P"
-    apply (unfold wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def)    
-    apply (erule wf_prog_lift)
-    apply (auto dest!: start_context.wt_kil_correct [OF start_context.intro] 
-                intro: someI)
-    apply (erule sees_method_is_class)
-    done
-  thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
-next
-  \<comment> \<open>completeness\<close>
-  assume wt: "wf_jvm_prog P"
-  thus "wf_jvm_prog\<^sub>k P"
-    apply (unfold wf_jvm_prog_def wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def)
-    apply (clarify)
-    apply (erule wf_prog_lift)
-    apply (auto intro!: start_context.wt_kil_complete start_context.intro)
-    apply (erule sees_method_is_class)
-    done
+  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)
+    moreover {
+      fix wf_md C M Ts Ca T m bd
+      assume "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M :  Ts\<rightarrow>T = m in Ca" and
+             "set Ts \<subseteq> types P" and "bd = (M, 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] 
+                 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"
+    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:  Ts\<rightarrow>T = m in Ca" and
+             "set Ts \<subseteq> types P" and "bd = (M, 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)
+    }
+    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/Jinja/BV/BVSpec.thy b/thys/Jinja/BV/BVSpec.thy
--- a/thys/Jinja/BV/BVSpec.thy
+++ b/thys/Jinja/BV/BVSpec.thy
@@ -1,93 +1,102 @@
 (*  Title:      HOL/MicroJava/BV/BVSpec.thy
 
     Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 
 *)
 
 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,ty list,nat,ty\<^sub>m] \<Rightarrow> bool"
 where
   "wt_start P C Ts mxl\<^sub>0 \<tau>s \<equiv>
   P \<turnstile> Some ([],OK (Class C)#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,ty list,ty,nat,nat,instr list,
                  ex_table,ty\<^sub>m] \<Rightarrow> bool"
 where
   "wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s \<equiv>
   0 < size is \<and> size \<tau>s = size is \<and>
   check_types P mxs (1+size Ts+mxl\<^sub>0) (map OK \<tau>s) \<and>
   wt_start P C 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,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
       wt_method P C 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:
-  "\<lbrakk> wf_jvm_prog\<^bsub>\<Phi>\<^esub> P; 
-      P \<turnstile> C sees M:Ts \<rightarrow> T = (mxs,mxl\<^sub>0,ins,xt) in C; pc < size ins \<rbrakk> 
-  \<Longrightarrow> P,T,mxs,size ins,xt \<turnstile> ins!pc,pc :: \<Phi> C M"
+assumes wf: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P" and
+      sees: "P \<turnstile> C sees M: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"
 (*<*)
-  apply (unfold wf_jvm_prog_phi_def)
-  apply (drule (1) sees_wf_mdecl)
-  apply (simp add: wf_mdecl_def wt_method_def)
-  done
+proof -
+  have wfm: "wf_prog
+     (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
+         wt_method P C 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:
-  "\<lbrakk> wf_jvm_prog\<^bsub>\<Phi>\<^esub> P; 
-     P \<turnstile> C sees M:Ts \<rightarrow> T = (mxs,mxl\<^sub>0,ins,xt) in C \<rbrakk> \<Longrightarrow> 
-  0 < size ins \<and> wt_start P C Ts mxl\<^sub>0 (\<Phi> C M)"
+assumes wf: "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P" and
+      sees: "P \<turnstile> C sees M:Ts \<rightarrow> T = (mxs,mxl\<^sub>0,ins,xt) in C"
+shows "0 < size ins \<and> wt_start P C Ts mxl\<^sub>0 (\<Phi> C M)"
 (*<*)
-  apply (unfold wf_jvm_prog_phi_def)
-  apply (drule (1) sees_wf_mdecl)
-  apply (simp add: wf_mdecl_def wt_method_def)
-  done
+proof -
+  have wfm: "wf_prog
+     (\<lambda>P C (M, Ts, T\<^sub>r, mxs, mxl\<^sub>0, is, xt).
+         wt_method P C 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
 (*>*)
 
 end
diff --git a/thys/Jinja/BV/Effect.thy b/thys/Jinja/BV/Effect.thy
--- a/thys/Jinja/BV/Effect.thy
+++ b/thys/Jinja/BV/Effect.thy
@@ -1,393 +1,395 @@
 (*  Title:      HOL/MicroJava/BV/Effect.thy
     Author:     Gerwin Klein
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
 section \<open>Effect of Instructions on the State Type\<close>
 
 theory Effect
 imports JVM_SemiType "../JVM/JVMExceptions"
 begin
 
 \<comment> \<open>FIXME\<close>
 locale prog =
   fixes P :: "'a prog"
 
 locale jvm_method = prog +
   fixes mxs :: nat  
   fixes mxl\<^sub>0 :: nat   
   fixes Ts :: "ty list" 
   fixes T\<^sub>r :: ty
   fixes "is" :: "instr list" 
   fixes xt :: ex_table
 
   fixes mxl :: nat
   defines mxl_def: "mxl \<equiv> 1+size Ts+mxl\<^sub>0"
 
 text \<open>Program counter of successor instructions:\<close>
 primrec succs :: "instr \<Rightarrow> ty\<^sub>i \<Rightarrow> pc \<Rightarrow> pc list" where
   "succs (Load idx) \<tau> pc     = [pc+1]"
 | "succs (Store idx) \<tau> pc    = [pc+1]"
 | "succs (Push v) \<tau> pc       = [pc+1]"
 | "succs (Getfield F C) \<tau> pc = [pc+1]"
 | "succs (Putfield F C) \<tau> pc = [pc+1]"
 | "succs (New C) \<tau> pc        = [pc+1]"
 | "succs (Checkcast C) \<tau> pc  = [pc+1]"
 | "succs Pop \<tau> pc            = [pc+1]"
 | "succs IAdd \<tau> pc           = [pc+1]"
 | "succs CmpEq \<tau> pc          = [pc+1]"
 | succs_IfFalse:
     "succs (IfFalse b) \<tau> pc    = [pc+1, nat (int pc + b)]"
 | succs_Goto:
     "succs (Goto b) \<tau> pc       = [nat (int pc + b)]"
 | succs_Return:
     "succs Return \<tau> pc         = []"  
 | succs_Invoke:
     "succs (Invoke M n) \<tau> pc   = (if (fst \<tau>)!n = NT then [] else [pc+1])"
 | succs_Throw:
     "succs Throw \<tau> pc          = []"
 
 text "Effect of instruction on the state type:"
 
 fun the_class:: "ty \<Rightarrow> cname" where
   "the_class (Class C) = C"
 
 fun eff\<^sub>i :: "instr \<times> 'm prog \<times> ty\<^sub>i \<Rightarrow> ty\<^sub>i" where
   eff\<^sub>i_Load:
     "eff\<^sub>i (Load n,  P, (ST, LT))          = (ok_val (LT ! n) # ST, LT)"
 | eff\<^sub>i_Store:
     "eff\<^sub>i (Store n, P, (T#ST, LT))        = (ST, LT[n:= OK T])"
 | eff\<^sub>i_Push:
     "eff\<^sub>i (Push v, P, (ST, LT))             = (the (typeof v) # ST, LT)"
 | eff\<^sub>i_Getfield:
     "eff\<^sub>i (Getfield F C, P, (T#ST, LT))    = (snd (field P C F) # ST, LT)"
 | eff\<^sub>i_Putfield:
    "eff\<^sub>i (Putfield F C, P, (T\<^sub>1#T\<^sub>2#ST, LT)) = (ST,LT)"
 | eff\<^sub>i_New:
    "eff\<^sub>i (New C, P, (ST,LT))               = (Class C # ST, LT)"
 | eff\<^sub>i_Checkcast:
    "eff\<^sub>i (Checkcast C, P, (T#ST,LT))       = (Class C # ST,LT)"
 | eff\<^sub>i_Pop:
    "eff\<^sub>i (Pop, P, (T#ST,LT))               = (ST,LT)"
 | eff\<^sub>i_IAdd:
    "eff\<^sub>i (IAdd, P,(T\<^sub>1#T\<^sub>2#ST,LT))           = (Integer#ST,LT)"
 | eff\<^sub>i_CmpEq:
    "eff\<^sub>i (CmpEq, P, (T\<^sub>1#T\<^sub>2#ST,LT))         = (Boolean#ST,LT)"
 | eff\<^sub>i_IfFalse:
    "eff\<^sub>i (IfFalse b, P, (T\<^sub>1#ST,LT))        = (ST,LT)"
 | eff\<^sub>i_Invoke:
    "eff\<^sub>i (Invoke M n, P, (ST,LT))          =
     (let C = the_class (ST!n); (D,Ts,T\<^sub>r,b) = method P C M
      in (T\<^sub>r # drop (n+1) ST, LT))"
 | eff\<^sub>i_Goto:
    "eff\<^sub>i (Goto n, P, s)                    = s"
 
 fun is_relevant_class :: "instr \<Rightarrow> 'm prog \<Rightarrow> cname \<Rightarrow> bool" where
   rel_Getfield:
     "is_relevant_class (Getfield F D) = (\<lambda>P C. P \<turnstile> NullPointer \<preceq>\<^sup>* C)" 
 | rel_Putfield:
     "is_relevant_class (Putfield F D) = (\<lambda>P C. P \<turnstile> NullPointer \<preceq>\<^sup>* C)" 
 | rel_Checcast:
     "is_relevant_class (Checkcast D)  = (\<lambda>P C. P \<turnstile> ClassCast \<preceq>\<^sup>* C)" 
 | rel_New:
     "is_relevant_class (New D)        = (\<lambda>P C. P \<turnstile> OutOfMemory \<preceq>\<^sup>* C)" 
 | rel_Throw:
     "is_relevant_class Throw          = (\<lambda>P C. True)"
 | rel_Invoke:
     "is_relevant_class (Invoke M n)   = (\<lambda>P C. True)"
 | rel_default:
     "is_relevant_class i              = (\<lambda>P C. False)"
 
 definition is_relevant_entry :: "'m prog \<Rightarrow> instr \<Rightarrow> pc \<Rightarrow> ex_entry \<Rightarrow> bool" where
   "is_relevant_entry P i pc e \<longleftrightarrow> (let (f,t,C,h,d) = e in is_relevant_class i P C \<and> pc \<in> {f..<t})"
 
 definition relevant_entries :: "'m prog \<Rightarrow> instr \<Rightarrow> pc \<Rightarrow> ex_table \<Rightarrow> ex_table" where
   "relevant_entries P i pc = filter (is_relevant_entry P i pc)"
 
 definition xcpt_eff :: "instr \<Rightarrow> 'm prog \<Rightarrow> pc \<Rightarrow> ty\<^sub>i 
                \<Rightarrow> ex_table \<Rightarrow> (pc \<times> ty\<^sub>i') list" where    
   "xcpt_eff i P pc \<tau> et = (let (ST,LT) = \<tau> in 
   map (\<lambda>(f,t,C,h,d). (h, Some (Class C#drop (size ST - d) ST, LT))) (relevant_entries P i pc et))"
 
 definition norm_eff :: "instr \<Rightarrow> 'm prog \<Rightarrow> nat \<Rightarrow> ty\<^sub>i \<Rightarrow> (pc \<times> ty\<^sub>i') list" where
   "norm_eff i P pc \<tau> = map (\<lambda>pc'. (pc',Some (eff\<^sub>i (i,P,\<tau>)))) (succs i \<tau> pc)"
 
 definition eff :: "instr \<Rightarrow> 'm prog \<Rightarrow> pc \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i' \<Rightarrow> (pc \<times> ty\<^sub>i') list" where
   "eff i P pc et t = (case t of           
     None \<Rightarrow> []          
   | Some \<tau> \<Rightarrow> (norm_eff i P pc \<tau>) @ (xcpt_eff i P pc \<tau> et))"
 
 
 lemma eff_None:
   "eff i P pc xt None = []"
 by (simp add: eff_def)
 
 lemma eff_Some:
   "eff i P pc xt (Some \<tau>) = norm_eff i P pc \<tau> @ xcpt_eff i P pc \<tau> xt"
 by (simp add: eff_def)
 
 (* FIXME: getfield, \<exists>T D. P \<turnstile> C sees F:T in D \<and> .. *)
 
 text "Conditions under which eff is applicable:"
 
 fun app\<^sub>i :: "instr \<times> 'm prog \<times> pc \<times> nat \<times> ty \<times> ty\<^sub>i \<Rightarrow> bool" where
   app\<^sub>i_Load:
     "app\<^sub>i (Load n, P, pc, mxs, T\<^sub>r, (ST,LT)) = 
     (n < length LT \<and> LT ! n \<noteq> Err \<and> length ST < mxs)"
 | app\<^sub>i_Store:
     "app\<^sub>i (Store n, P, pc, mxs, T\<^sub>r, (T#ST, LT)) = 
     (n < length LT)"
 | app\<^sub>i_Push:
     "app\<^sub>i (Push v, P, pc, mxs, T\<^sub>r, (ST,LT)) = 
      (length ST < mxs \<and> typeof v \<noteq> None)"
 | app\<^sub>i_Getfield:
     "app\<^sub>i (Getfield F C, P, pc, mxs, T\<^sub>r, (T#ST, LT)) = 
     (\<exists>T\<^sub>f. P \<turnstile> C sees F:T\<^sub>f in C \<and> P \<turnstile> T \<le> Class C)"
 | app\<^sub>i_Putfield:
     "app\<^sub>i (Putfield F C, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST, LT)) = 
     (\<exists>T\<^sub>f. P \<turnstile> C sees F:T\<^sub>f in C \<and> P \<turnstile> T\<^sub>2 \<le> (Class C) \<and> P \<turnstile> T\<^sub>1 \<le> T\<^sub>f)" 
 | app\<^sub>i_New:
     "app\<^sub>i (New C, P, pc, mxs, T\<^sub>r, (ST,LT)) = 
     (is_class P C \<and> length ST < mxs)"
 | app\<^sub>i_Checkcast:
     "app\<^sub>i (Checkcast C, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = 
     (is_class P C \<and> is_refT T)"
 | app\<^sub>i_Pop:
     "app\<^sub>i (Pop, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = 
     True"
 | app\<^sub>i_IAdd:
     "app\<^sub>i (IAdd, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST,LT)) = (T\<^sub>1 = T\<^sub>2 \<and> T\<^sub>1 = Integer)"
 | app\<^sub>i_CmpEq:
     "app\<^sub>i (CmpEq, P, pc, mxs, T\<^sub>r, (T\<^sub>1#T\<^sub>2#ST,LT)) =
     (T\<^sub>1 = T\<^sub>2 \<or> is_refT T\<^sub>1 \<and> is_refT T\<^sub>2)"
 | app\<^sub>i_IfFalse:
     "app\<^sub>i (IfFalse b, P, pc, mxs, T\<^sub>r, (Boolean#ST,LT)) = 
     (0 \<le> int pc + b)"
 | app\<^sub>i_Goto:
     "app\<^sub>i (Goto b, P, pc, mxs, T\<^sub>r, s) = 
     (0 \<le> int pc + b)"
 | app\<^sub>i_Return:
     "app\<^sub>i (Return, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = 
     (P \<turnstile> T \<le> T\<^sub>r)"
 | app\<^sub>i_Throw:
     "app\<^sub>i (Throw, P, pc, mxs, T\<^sub>r, (T#ST,LT)) = 
     is_refT T"
 | app\<^sub>i_Invoke:
     "app\<^sub>i (Invoke M n, P, pc, mxs, T\<^sub>r, (ST,LT)) =
     (n < length ST \<and> 
     (ST!n \<noteq> NT \<longrightarrow>
       (\<exists>C D Ts T m. ST!n = Class C \<and> P \<turnstile> C sees M:Ts \<rightarrow> T = m in D \<and>
                     P \<turnstile> rev (take n ST) [\<le>] Ts)))"
   
 | app\<^sub>i_default:
     "app\<^sub>i (i,P, pc,mxs,T\<^sub>r,s) = False"
 
 
 definition xcpt_app :: "instr \<Rightarrow> 'm prog \<Rightarrow> pc \<Rightarrow> nat \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i \<Rightarrow> bool" where
   "xcpt_app i P pc mxs xt \<tau> \<longleftrightarrow> (\<forall>(f,t,C,h,d) \<in> set (relevant_entries P i pc xt). is_class P C \<and> d \<le> size (fst \<tau>) \<and> d < mxs)"
 
 definition app :: "instr \<Rightarrow> 'm prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i' \<Rightarrow> bool" where
   "app i P mxs T\<^sub>r pc mpc xt t = (case t of None \<Rightarrow> True | Some \<tau> \<Rightarrow> 
   app\<^sub>i (i,P,pc,mxs,T\<^sub>r,\<tau>) \<and> xcpt_app i P pc mxs xt \<tau> \<and> 
   (\<forall>(pc',\<tau>') \<in> set (eff i P pc xt t). pc' < mpc))"
 
 
 lemma app_Some:
   "app i P mxs T\<^sub>r pc mpc xt (Some \<tau>) = 
   (app\<^sub>i (i,P,pc,mxs,T\<^sub>r,\<tau>) \<and> xcpt_app i P pc mxs xt \<tau> \<and> 
   (\<forall>(pc',s') \<in> set (eff i P pc xt (Some \<tau>)). pc' < mpc))"
 by (simp add: app_def)
 
 locale eff = jvm_method +
   fixes eff\<^sub>i and app\<^sub>i and eff and app 
   fixes norm_eff and xcpt_app and xcpt_eff
 
   fixes mpc
   defines "mpc \<equiv> size is"
 
   defines "eff\<^sub>i i \<tau> \<equiv> Effect.eff\<^sub>i (i,P,\<tau>)"
   notes eff\<^sub>i_simps [simp] = Effect.eff\<^sub>i.simps [where P = P, folded eff\<^sub>i_def]
 
   defines "app\<^sub>i i pc \<tau> \<equiv> Effect.app\<^sub>i (i, P, pc, mxs, T\<^sub>r, \<tau>)"
   notes app\<^sub>i_simps [simp] = Effect.app\<^sub>i.simps [where P=P and mxs=mxs and T\<^sub>r=T\<^sub>r, folded app\<^sub>i_def]
 
   defines "xcpt_eff i pc \<tau> \<equiv> Effect.xcpt_eff i P pc \<tau> xt"
   notes xcpt_eff = Effect.xcpt_eff_def [of _ P _ _ xt, folded xcpt_eff_def]
 
   defines "norm_eff i pc \<tau> \<equiv> Effect.norm_eff i P pc \<tau>"
   notes norm_eff = Effect.norm_eff_def [of _ P, folded norm_eff_def eff\<^sub>i_def]
 
   defines "eff i pc \<equiv> Effect.eff i P pc xt"
   notes eff = Effect.eff_def [of _ P  _ xt, folded eff_def norm_eff_def xcpt_eff_def]
 
   defines "xcpt_app i pc \<tau> \<equiv> Effect.xcpt_app i P pc mxs xt \<tau>"
   notes xcpt_app = Effect.xcpt_app_def [of _ P _ mxs xt, folded xcpt_app_def]
 
   defines "app i pc \<equiv> Effect.app i P mxs T\<^sub>r pc mpc xt"
   notes app = Effect.app_def [of _ P mxs T\<^sub>r _ mpc xt, folded app_def xcpt_app_def app\<^sub>i_def eff_def]
 
 
 lemma length_cases2:
   assumes "\<And>LT. P ([],LT)"
   assumes "\<And>l ST LT. P (l#ST,LT)"
   shows "P s"
   by (cases s, cases "fst s") (auto intro!: assms)
 
 
 lemma length_cases3:
   assumes "\<And>LT. P ([],LT)"
   assumes "\<And>l LT. P ([l],LT)"
   assumes "\<And>l ST LT. P (l#ST,LT)"
   shows "P s"
 (*<*)
 proof -
   obtain xs LT where s: "s = (xs,LT)" by (cases s)
   show ?thesis
   proof (cases xs)
     case Nil with assms s show ?thesis by simp
   next
     fix l xs' assume "xs = l#xs'"
     with assms s show ?thesis by simp
   qed
 qed
 (*>*)
 
 lemma length_cases4:
   assumes "\<And>LT. P ([],LT)"
   assumes "\<And>l LT. P ([l],LT)"
   assumes "\<And>l l' LT. P ([l,l'],LT)"
   assumes "\<And>l l' ST LT. P (l#l'#ST,LT)"
   shows "P s"
 (*<*)
 proof -
   obtain xs LT where s: "s = (xs,LT)" by (cases s)
   show ?thesis
   proof (cases xs)
     case Nil with assms s show ?thesis by simp
   next
     fix l xs' assume xs: "xs = l#xs'"
     thus ?thesis
     proof (cases xs')
       case Nil with assms s xs show ?thesis by simp
     next
       fix l' ST assume "xs' = l'#ST"
      with assms s xs show ?thesis by simp
     qed
   qed
 qed
 (*>*)
 
 text \<open>
 \medskip
 simp rules for @{term app}
 \<close>
 lemma appNone[simp]: "app i P mxs T\<^sub>r pc mpc et None = True" 
   by (simp add: app_def)
 
 
 lemma appLoad[simp]:
 "app\<^sub>i (Load idx, P, T\<^sub>r, mxs, pc, s) = (\<exists>ST LT. s = (ST,LT) \<and> idx < length LT \<and> LT!idx \<noteq> Err \<and> length ST < mxs)"
   by (cases s, simp)
 
 lemma appStore[simp]:
 "app\<^sub>i (Store idx,P,pc,mxs,T\<^sub>r,s) = (\<exists>ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
   by (rule length_cases2, auto)
 
 lemma appPush[simp]:
 "app\<^sub>i (Push v,P,pc,mxs,T\<^sub>r,s) =
  (\<exists>ST LT. s = (ST,LT) \<and> length ST < mxs \<and> typeof v \<noteq> None)"
   by (cases s, simp)
 
 lemma appGetField[simp]:
 "app\<^sub>i (Getfield F C,P,pc,mxs,T\<^sub>r,s) = 
  (\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> 
   P \<turnstile> C sees F:vT in C \<and> P \<turnstile> oT \<le> (Class C))"
   by (rule length_cases2 [of _ s]) auto
 
 lemma appPutField[simp]:
 "app\<^sub>i (Putfield F C,P,pc,mxs,T\<^sub>r,s) = 
  (\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and>
   P \<turnstile> C sees F:vT' in C \<and> P \<turnstile> oT \<le> (Class C) \<and> P \<turnstile> vT \<le> vT')"
   by (rule length_cases4 [of _ s], auto)
 
 lemma appNew[simp]:
   "app\<^sub>i (New C,P,pc,mxs,T\<^sub>r,s) = 
   (\<exists>ST LT. s=(ST,LT) \<and> is_class P C \<and> length ST < mxs)"
   by (cases s, simp)
 
 lemma appCheckcast[simp]: 
   "app\<^sub>i (Checkcast C,P,pc,mxs,T\<^sub>r,s) =  
   (\<exists>T ST LT. s = (T#ST,LT) \<and> is_class P C \<and> is_refT T)"
   by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
 
 lemma app\<^sub>iPop[simp]: 
 "app\<^sub>i (Pop,P,pc,mxs,T\<^sub>r,s) = (\<exists>ts ST LT. s = (ts#ST,LT))"
   by (rule length_cases2, auto)
 
 lemma appIAdd[simp]:
 "app\<^sub>i (IAdd,P,pc,mxs,T\<^sub>r,s) = (\<exists>ST LT. s = (Integer#Integer#ST,LT))"
 (*<*)
 proof -
   obtain ST LT where [simp]: "s = (ST,LT)" by (cases s)
   have "ST = [] \<or> (\<exists>T. ST = [T]) \<or> (\<exists>T\<^sub>1 T\<^sub>2 ST'. ST = T\<^sub>1#T\<^sub>2#ST')"
     by (cases ST, auto, case_tac list, auto)
   moreover
   { assume "ST = []" hence ?thesis by simp }
   moreover
   { fix T assume "ST = [T]" hence ?thesis by (cases T, auto) }
   moreover
   { fix T\<^sub>1 T\<^sub>2 ST' assume "ST = T\<^sub>1#T\<^sub>2#ST'"
     hence ?thesis by (cases T\<^sub>1, auto)
   }
   ultimately show ?thesis by blast
 qed
 (*>*)
 
 
 lemma appIfFalse [simp]:
 "app\<^sub>i (IfFalse b,P,pc,mxs,T\<^sub>r,s) = 
   (\<exists>ST LT. s = (Boolean#ST,LT) \<and> 0 \<le> int pc + b)"
 (*<*)
-  apply (rule length_cases2)
-  apply simp
-  apply (case_tac l) 
-  apply auto
-  done
+ (is "?P s")
+proof(rule length_cases2)
+  fix LT show "?P ([],LT)" by simp
+next
+  fix l ST LT show "?P (l#ST,LT)"
+    by (case_tac l) auto
+qed
 (*>*)
 
 lemma appCmpEq[simp]:
 "app\<^sub>i (CmpEq,P,pc,mxs,T\<^sub>r,s) = 
   (\<exists>T\<^sub>1 T\<^sub>2 ST LT. s = (T\<^sub>1#T\<^sub>2#ST,LT) \<and> (\<not>is_refT T\<^sub>1 \<and> T\<^sub>2 = T\<^sub>1 \<or> is_refT T\<^sub>1 \<and> is_refT T\<^sub>2))"
   by (rule length_cases4, auto)
 
 lemma appReturn[simp]:
 "app\<^sub>i (Return,P,pc,mxs,T\<^sub>r,s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> P \<turnstile> T \<le> T\<^sub>r)" 
   by (rule length_cases2, auto)
 
 lemma appThrow[simp]:
   "app\<^sub>i (Throw,P,pc,mxs,T\<^sub>r,s) = (\<exists>T ST LT. s=(T#ST,LT) \<and> is_refT T)"
   by (rule length_cases2, auto)  
 
 lemma effNone: 
   "(pc', s') \<in> set (eff i P pc et None) \<Longrightarrow> s' = None"
   by (auto simp add: eff_def xcpt_eff_def norm_eff_def)
 
 
 text \<open>some helpers to make the specification directly executable:\<close>
 lemma relevant_entries_append [simp]:
   "relevant_entries P i pc (xt @ xt') = relevant_entries P i pc xt @ relevant_entries P i pc xt'"
   by (unfold relevant_entries_def) simp
 
 lemma xcpt_app_append [iff]:
   "xcpt_app i P pc mxs (xt@xt') \<tau> = (xcpt_app i P pc mxs xt \<tau> \<and> xcpt_app i P pc mxs xt' \<tau>)"
   by (unfold xcpt_app_def) fastforce
 
 lemma xcpt_eff_append [simp]:
   "xcpt_eff i P pc \<tau> (xt@xt') = xcpt_eff i P pc \<tau> xt @ xcpt_eff i P pc \<tau> xt'"
  by (unfold xcpt_eff_def, cases \<tau>) simp
 
 lemma app_append [simp]:
   "app i P pc T mxs mpc (xt@xt') \<tau> = (app i P pc T mxs mpc xt \<tau> \<and> app i P pc T mxs mpc xt' \<tau>)"
   by (unfold app_def eff_def) auto
 
 end
diff --git a/thys/Jinja/BV/LBVJVM.thy b/thys/Jinja/BV/LBVJVM.thy
--- a/thys/Jinja/BV/LBVJVM.thy
+++ b/thys/Jinja/BV/LBVJVM.thy
@@ -1,223 +1,242 @@
 (*  Title:      HOL/MicroJava/BV/JVM.thy
 
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
 
 section \<open>LBV for the JVM \label{sec:JVM}\<close>
 
 theory LBVJVM
 imports "../DFA/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> 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 Ts T\<^sub>r mxs mxl\<^sub>0 et cert ins \<equiv>
    check_cert P mxs (1+size Ts+mxl\<^sub>0) (size ins) cert \<and>
    0 < size ins \<and> 
    (let start  = Some ([],(OK (Class C))#((map OK Ts))@(replicate mxl\<^sub>0 Err));
         result = lbvjvm P mxs (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,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,b,et)). wt_lbv P C Ts T\<^sub>r mxs mxl\<^sub>0 et (cert C mn) b) 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,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 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 (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 Ts T\<^sub>r mxs mxl\<^sub>0 xt cert is"  
   shows "\<exists>\<tau>s. wt_method P C 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)
   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 Ts mxl\<^sub>0 (map ok_val \<tau>s)"
     by (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 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 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 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 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 (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"
-    apply (auto simp add: make_cert_def check_types_def JVM_states_unfold)
-    apply (subst Ok_in_err [symmetric])
-    apply (drule nth_mem)
-    apply auto
-    done
+    by (fastforce simp: make_cert_def check_types_def JVM_states_unfold
+                  dest!: nth_mem)
   moreover note 0 size
   ultimately show ?thesis 
     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,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)) = method P C mn in 
               SOME \<tau>s. wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
-    
+  
+  let ?A = "\<lambda>P C (mn,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)). wt_lbv P C Ts T\<^sub>r mxs mxl\<^sub>0 et (Cert C mn) ins"
+  let ?B = "\<lambda>P C (M,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
+                wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (?\<Phi> C M)"
+
   assume wt: "wt_jvm_prog_lbv P Cert"
-  hence "wf_jvm_prog\<^bsub>?\<Phi>\<^esub> P"
-    apply (unfold wf_jvm_prog_phi_def wt_jvm_prog_lbv_def) 
-    apply (erule wf_prog_lift)
-    apply (auto dest!: start_context.wt_lbv_wt_method [OF start_context.intro] 
-                intro: someI)
-    apply (erule sees_method_is_class)
-    done
+  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:  Ts\<rightarrow>T = m in Ca" and
+           "set Ts \<subseteq> types P" and "bd = (M, 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)
+  }
+  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>)"
 (*<*)
-  using wt
-  apply (unfold wf_jvm_prog_phi_def wt_jvm_prog_lbv_def)
-  apply (erule wf_prog_lift)
-  apply (auto simp add: prg_cert_def 
-              intro!: start_context.wt_method_wt_lbv start_context.intro)
-  apply (erule sees_method_is_class)                                     
-  done
+proof -
+  let ?cert = "prg_cert P \<Phi>"
+  let ?A = "\<lambda>P C (M,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). 
+                wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (\<Phi> C M)"
+  let ?B = "\<lambda>P C (mn,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,ins,et)).
+                wt_lbv P C 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 Ts Ca T m bd
+    assume "wf_prog wf_md P" and sees: "P \<turnstile> Ca sees M:  Ts\<rightarrow>T = m in Ca" and
+           "set Ts \<subseteq> types P" and "bd = (M, Ts, T, m)" and
+           "?A P Ca bd"
+    then 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)
+  }
+  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  
+end
diff --git a/thys/Jinja/BV/TF_JVM.thy b/thys/Jinja/BV/TF_JVM.thy
--- a/thys/Jinja/BV/TF_JVM.thy
+++ b/thys/Jinja/BV/TF_JVM.thy
@@ -1,275 +1,292 @@
 (*  Title:      HOL/MicroJava/BV/JVM.thy
 
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
 
 section \<open>The Typing Framework for the JVM \label{sec:JVM}\<close>
 
 theory TF_JVM
 imports "../DFA/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 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> 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"
 
 
 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 ([],OK (Class C) # map OK Ts @ replicate mxl\<^sub>0 Err)"
   defines [simp]:
   "start \<equiv> OK first # replicate (size is - 1) (OK None)"
 
 
 
 subsection \<open>Connecting JVM and Framework\<close>
 
 
 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"
 (*<*)
-  apply (insert wf)
-  apply simp
-  apply (unfold JVM_states_unfold)
-  apply (rule pres_type_lift)
-  apply clarify
-  apply (rename_tac s pc pc' s')
-  apply (case_tac s)
-   apply simp
-   apply (drule effNone)
-   apply simp  
-  apply (simp add: Effect.app_def xcpt_app_def Effect.eff_def  
-                   xcpt_eff_def norm_eff_def relevant_entries_def)
-  apply (case_tac "is!pc")
-
-  \<comment> \<open>Load\<close>
-  apply clarsimp
-  apply (frule listE_nth_in, assumption)
-  apply fastforce
-
-  \<comment> \<open>Store\<close>
-  apply fastforce
-
-  \<comment> \<open>Push\<close>
-  apply (fastforce simp add: typeof_lit_is_type)
-
-  \<comment> \<open>New\<close>
-  apply fastforce
-
-  \<comment> \<open>Getfield\<close>
-  apply (fastforce dest: sees_field_is_type)
-
-  \<comment> \<open>Putfield\<close>
-  apply fastforce
-
-  \<comment> \<open>Checkcast\<close>
-  apply fastforce
-
-  defer 
-  
-  \<comment> \<open>Return\<close>
-  apply fastforce
-
-  \<comment> \<open>Pop\<close>
-  apply fastforce
-
-  \<comment> \<open>IAdd\<close>
-  apply fastforce
-  
-  \<comment> \<open>Goto\<close>
-  apply fastforce
-
-  \<comment> \<open>CmpEq\<close>
-  apply fastforce
-
-  \<comment> \<open>IfFalse\<close>
-  apply fastforce
-
-  \<comment> \<open>Throw\<close>
-  apply fastforce
-
-  \<comment> \<open>Invoke\<close>
-  apply (clarsimp split!: if_splits)
-   apply fastforce
-  apply (erule disjE)
-   prefer 2
-   apply fastforce
-  apply clarsimp
-  apply (rule conjI)
-   apply (drule (1) sees_wf_mdecl)
-   apply (clarsimp simp add: wf_mdecl_def)
-  apply arith
-  done
+proof -
+  let ?n = "size is" and ?app = app and ?step = eff
+  let ?mxl = "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 (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
+        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"
 (*<*)
-  apply (unfold lesubstep_type_def)
-  apply clarify
-  apply (simp add: set_conv_nth)
-  apply clarify
-  apply (drule le_listD, assumption)
-  apply (clarsimp simp add: lesub_def Product.le_def)
-  apply (rule exI)
-  apply (rule conjI)
-   apply (rule exI)
-   apply (rule conjI)
-    apply (rule sym)
-    apply assumption
-   apply assumption
-  apply assumption
-  done
+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:
-  "\<lbrakk>wf_prog p P; pc < length is; s \<sqsubseteq>\<^bsub>sup_state_opt P\<^esub> t; app pc t\<rbrakk>
-  \<Longrightarrow> set (eff pc s) {\<sqsubseteq>\<^bsub>sup_state_opt P\<^esub>} set (eff pc t)"
+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)"
 (*<*)
-  apply simp
-  apply (unfold Effect.eff_def)  
-  apply (cases t)
-   apply (simp add: lesub_def)
-  apply (rename_tac a)
-  apply (cases s)
-   apply simp
-  apply (rename_tac b)
-  apply simp
-  apply (rule lesubstep_union)
-   prefer 2
-   apply (rule lesubstep_type_simple)
-   apply (simp add: xcpt_eff_def)
-   apply (rule le_listI)
-    apply (simp add: split_beta)
-   apply (simp add: split_beta)
-   apply (simp add: lesub_def fun_of_def)
-   apply (case_tac a)
-   apply (case_tac b)
-   apply simp   
-   apply (subgoal_tac "size ab = size aa")
-     prefer 2
-     apply (clarsimp simp add: list_all2_lengthD)
-   apply simp
-  apply (clarsimp simp add: norm_eff_def lesubstep_type_def lesub_def iff del: sup_state_conv)
-  apply (rule exI)
-  apply (rule conjI2)
-   apply (rule imageI)
-   apply (clarsimp simp add: Effect.app_def iff del: sup_state_conv)
-   apply (drule (2) succs_mono)
-   apply blast
-  apply simp
-  apply (erule eff\<^sub>i_mono)
-     apply simp
-    apply assumption   
-   apply clarsimp
-  apply clarsimp  
-  done
+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)"
 (*<*)
-  apply simp
-  apply (unfold bounded_def err_step_def Effect.app_def Effect.eff_def)
-  apply (auto simp add: error_def map_snd_def split: err.splits option.splits)
-  done
+  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 blast
-    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 (1 + length Ts + mxl\<^sub>0) (err (types P)))"
+  have "order ?r" 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 (force intro!: list_appendI simp add: JVM_states_unfold)
 
 
 lemma (in JVM_sl) wt_method_def2:
   "wt_method P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s =
   (is \<noteq> [] \<and> 
    size \<tau>s = size is \<and>
    OK ` set \<tau>s \<subseteq> states P mxs mxl \<and>
    wt_start P C' Ts mxl\<^sub>0 \<tau>s \<and> 
    wt_app_eff (sup_state_opt P) app eff \<tau>s)"
 (*<*)
-  apply (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def check_types_def)
-  apply auto
-  done
+  by (unfold wt_method_def wt_app_eff_def wt_instr_def lesub_def
+             check_types_def) auto
 (*>*)
 
 
 end
diff --git a/thys/Jinja/Common/Auxiliary.thy b/thys/Jinja/Common/Auxiliary.thy
--- a/thys/Jinja/Common/Auxiliary.thy
+++ b/thys/Jinja/Common/Auxiliary.thy
@@ -1,125 +1,121 @@
 (*  Title:      Jinja/Common/Basis.thy
 
     Author:     David von Oheimb, Tobias Nipkow
     Copyright   1999 TU Muenchen
 *)
 
 chapter \<open>Jinja Source Language \label{cha:j}\<close>
 
 section \<open>Auxiliary Definitions\<close>
 
 theory Auxiliary imports Main begin
 (* FIXME move and possibly turn into a general simproc *)
 lemma nat_add_max_le[simp]:
   "((n::nat) + max i j \<le> m) = (n + i \<le> m \<and> n + j \<le> m)"
  (*<*)by arith(*>*)
 
 lemma Suc_add_max_le[simp]:
   "(Suc(n + max i j) \<le> m) = (Suc(n + i) \<le> m \<and> Suc(n + j) \<le> m)"
 (*<*)by arith(*>*)
 
 
 notation Some  ("(\<lfloor>_\<rfloor>)")
 
 (*<*)
 declare
  option.splits[split]
  Let_def[simp]
  subset_insertI2 [simp]
  Cons_eq_map_conv [iff]
 (*>*)
 
 
 subsection \<open>\<open>distinct_fst\<close>\<close>
  
 definition distinct_fst  :: "('a \<times> 'b) list \<Rightarrow> bool"
 where
   "distinct_fst  \<equiv>  distinct \<circ> map fst"
 
 lemma distinct_fst_Nil [simp]:
   "distinct_fst []"
  (*<*)
-apply (unfold distinct_fst_def)
-apply (simp (no_asm))
-done
+by (unfold distinct_fst_def) (simp (no_asm))
 (*>*)
 
 lemma distinct_fst_Cons [simp]:
   "distinct_fst ((k,x)#kxs) = (distinct_fst kxs \<and> (\<forall>y. (k,y) \<notin> set kxs))"
 (*<*)
-apply (unfold distinct_fst_def)
-apply (auto simp:image_def)
-done
+by (unfold distinct_fst_def) (auto simp:image_def)
 (*>*)
 (*
 lemma distinct_fst_append:
  "\<lbrakk> distinct_fst kxs'; distinct_fst kxs; \<forall>(k,x) \<in> set kxs. \<forall>(k',x') \<in> set kxs'. k' \<noteq> k \<rbrakk>
   \<Longrightarrow> distinct_fst(kxs @ kxs')"
 by (induct kxs) (auto dest: fst_in_set_lemma)
 
 lemma distinct_fst_map_inj:
   "\<lbrakk> distinct_fst kxs; inj f \<rbrakk> \<Longrightarrow> distinct_fst (map (\<lambda>(k,x). (f k, g k x)) kxs)"
 by (induct kxs) (auto dest: fst_in_set_lemma simp: inj_eq)
 *)
 
 lemma map_of_SomeI:
   "\<lbrakk> distinct_fst kxs; (k,x) \<in> set kxs \<rbrakk> \<Longrightarrow> map_of kxs k = Some x"
 (*<*)by (induct kxs) (auto simp:fun_upd_apply)(*>*)
 
 
 subsection \<open>Using @{term list_all2} for relations\<close>
 
 definition fun_of :: "('a \<times> 'b) set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
 where
   "fun_of S \<equiv> \<lambda>x y. (x,y) \<in> S"
 
 text \<open>Convenience lemmas\<close>
 (*<*)
 declare fun_of_def [simp]
 (*>*)
 lemma rel_list_all2_Cons [iff]:
   "list_all2 (fun_of S) (x#xs) (y#ys) = 
    ((x,y) \<in> S \<and> list_all2 (fun_of S) xs ys)"
   (*<*)by simp(*>*)
 
 lemma rel_list_all2_Cons1:
   "list_all2 (fun_of S) (x#xs) ys = 
   (\<exists>z zs. ys = z#zs \<and> (x,z) \<in> S \<and> list_all2 (fun_of S) xs zs)"
   (*<*)by (cases ys) auto(*>*)
 
 lemma rel_list_all2_Cons2:
   "list_all2 (fun_of S) xs (y#ys) = 
   (\<exists>z zs. xs = z#zs \<and> (z,y) \<in> S \<and> list_all2 (fun_of S) zs ys)"
   (*<*)by (cases xs) auto(*>*)
 
 lemma rel_list_all2_refl:
   "(\<And>x. (x,x) \<in> S) \<Longrightarrow> list_all2 (fun_of S) xs xs"
   (*<*)by (simp add: list_all2_refl)(*>*)
 
 lemma rel_list_all2_antisym:
   "\<lbrakk> (\<And>x y. \<lbrakk>(x,y) \<in> S; (y,x) \<in> T\<rbrakk> \<Longrightarrow> x = y); 
      list_all2 (fun_of S) xs ys; list_all2 (fun_of T) ys xs \<rbrakk> \<Longrightarrow> xs = ys"
   (*<*)by (rule list_all2_antisym) auto(*>*)
 
 lemma rel_list_all2_trans: 
   "\<lbrakk> \<And>a b c. \<lbrakk>(a,b) \<in> R; (b,c) \<in> S\<rbrakk> \<Longrightarrow> (a,c) \<in> T;
     list_all2 (fun_of R) as bs; list_all2 (fun_of S) bs cs\<rbrakk> 
   \<Longrightarrow> list_all2 (fun_of T) as cs"
   (*<*)by (rule list_all2_trans) auto(*>*)
 
 lemma rel_list_all2_update_cong:
   "\<lbrakk> i<size xs; list_all2 (fun_of S) xs ys; (x,y) \<in> S \<rbrakk> 
   \<Longrightarrow> list_all2 (fun_of S) (xs[i:=x]) (ys[i:=y])"
   (*<*)by (simp add: list_all2_update_cong)(*>*)
 
 lemma rel_list_all2_nthD:
   "\<lbrakk> list_all2 (fun_of S) xs ys; p < size xs \<rbrakk> \<Longrightarrow> (xs!p,ys!p) \<in> S"
   (*<*)by (drule list_all2_nthD) auto(*>*)
 
 lemma rel_list_all2I:
   "\<lbrakk> length a = length b; \<And>n. n < length a \<Longrightarrow> (a!n,b!n) \<in> S \<rbrakk> \<Longrightarrow> list_all2 (fun_of S) a b"
   (*<*)by (erule list_all2_all_nthI) simp(*>*)
 
 (*<*)declare fun_of_def [simp del](*>*)
 
 end
diff --git a/thys/Jinja/Common/Conform.thy b/thys/Jinja/Common/Conform.thy
--- a/thys/Jinja/Common/Conform.thy
+++ b/thys/Jinja/Common/Conform.thy
@@ -1,221 +1,147 @@
 (*  Title:      Jinja/J/Conform.thy
 
     Author:     David von Oheimb, Tobias Nipkow
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 section \<open>Conformance Relations for Type Soundness Proofs\<close>
 
 theory Conform
 imports Exceptions
 begin
 
 definition conf :: "'m prog \<Rightarrow> heap \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"   ("_,_ \<turnstile> _ :\<le> _"  [51,51,51,51] 50)
 where
   "P,h \<turnstile> v :\<le> T  \<equiv>
   \<exists>T'. typeof\<^bsub>h\<^esub> v = Some T' \<and> P \<turnstile> T' \<le> T"
 
 definition oconf :: "'m prog \<Rightarrow> heap \<Rightarrow> obj \<Rightarrow> bool"   ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
 where
   "P,h \<turnstile> obj \<surd>  \<equiv>
   let (C,fs) = obj in \<forall>F D T. P \<turnstile> C has F:T in D \<longrightarrow>
   (\<exists>v. fs(F,D) = Some v \<and> P,h \<turnstile> v :\<le> T)"
 
 definition hconf :: "'m prog \<Rightarrow> heap \<Rightarrow> bool"  ("_ \<turnstile> _ \<surd>" [51,51] 50)
 where
   "P \<turnstile> h \<surd>  \<equiv>
   (\<forall>a obj. h a = Some obj \<longrightarrow> P,h \<turnstile> obj \<surd>) \<and> preallocated h"
 
 definition lconf :: "'m prog \<Rightarrow> heap \<Rightarrow> (vname \<rightharpoonup> val) \<Rightarrow> (vname \<rightharpoonup> ty) \<Rightarrow> bool"   ("_,_ \<turnstile> _ '(:\<le>') _" [51,51,51,51] 50)
 where
   "P,h \<turnstile> l (:\<le>) E  \<equiv>
   \<forall>V v. l V = Some v \<longrightarrow> (\<exists>T. E V = Some T \<and> P,h \<turnstile> v :\<le> T)"
 
 abbreviation
   confs :: "'m prog \<Rightarrow> heap \<Rightarrow> val list \<Rightarrow> ty list \<Rightarrow> bool" 
              ("_,_ \<turnstile> _ [:\<le>] _" [51,51,51,51] 50) where
   "P,h \<turnstile> vs [:\<le>] Ts \<equiv> list_all2 (conf P h) vs Ts"
 
 
 subsection\<open>Value conformance \<open>:\<le>\<close>\<close>
 
 lemma conf_Null [simp]: "P,h \<turnstile> Null :\<le> T  =  P \<turnstile> NT \<le> T"
-(*<*)
-apply (unfold conf_def)
-apply (simp (no_asm))
-done
-(*>*)
+(*<*)by (simp (no_asm) add: conf_def)(*>*)
 
 lemma typeof_conf[simp]: "typeof\<^bsub>h\<^esub> v = Some T \<Longrightarrow> P,h \<turnstile> v :\<le> T"
-(*<*)
-apply (unfold conf_def)
-apply (induct v)
-apply auto
-done
-(*>*)
+(*<*)by (induct v) (auto simp: conf_def)(*>*)
 
 lemma typeof_lit_conf[simp]: "typeof v = Some T \<Longrightarrow> P,h \<turnstile> v :\<le> T"
 (*<*)by (rule typeof_conf[OF typeof_lit_typeof])(*>*)
 
 lemma defval_conf[simp]: "P,h \<turnstile> default_val T :\<le> T"
-(*<*)
-apply (unfold conf_def)
-apply (cases T)
-apply auto
-done
-(*>*)
+(*<*)by (cases T) (auto simp: conf_def)(*>*)
 
 lemma conf_upd_obj: "h a = Some(C,fs) \<Longrightarrow> (P,h(a\<mapsto>(C,fs')) \<turnstile> x :\<le> T) = (P,h \<turnstile> x :\<le> T)"
-(*<*)
-apply (unfold conf_def)
-apply (rule val.induct)
-apply (auto simp:fun_upd_apply)
-done
-(*>*)
+(*<*)by (rule val.induct) (auto simp:conf_def fun_upd_apply)(*>*)
 
 lemma conf_widen: "P,h \<turnstile> v :\<le> T \<Longrightarrow> P \<turnstile> T \<le> T' \<Longrightarrow> P,h \<turnstile> v :\<le> T'"
-(*<*)
-apply (unfold conf_def)
-apply (induct v)
-apply (auto intro: widen_trans)
-done
-(*>*)
+(*<*)by (induct v) (auto intro: widen_trans simp: conf_def)(*>*)
 
 lemma conf_hext: "h \<unlhd> h' \<Longrightarrow> P,h \<turnstile> v :\<le> T \<Longrightarrow> P,h' \<turnstile> v :\<le> T"
-(*<*)
-apply (unfold conf_def)
-apply (induct v)
-apply (auto dest: hext_objD)
-done
-(*>*)
+(*<*)by (induct v) (auto dest: hext_objD simp: conf_def)(*>*)
 
 lemma conf_ClassD: "P,h \<turnstile> v :\<le> Class C \<Longrightarrow>
   v = Null \<or> (\<exists>a obj T. v = Addr a \<and>  h a = Some obj \<and> obj_ty obj = T \<and>  P \<turnstile> T \<le> Class C)"
-(*<*)
-apply (unfold conf_def)
-apply(induct "v")
-apply(auto)
-done
-(*>*)
+(*<*)by(induct v) (auto simp: conf_def)(*>*)
 
 lemma conf_NT [iff]: "P,h \<turnstile> v :\<le> NT = (v = Null)"
 (*<*)by (auto simp add: conf_def)(*>*)
 
 lemma non_npD: "\<lbrakk> v \<noteq> Null; P,h \<turnstile> v :\<le> Class C \<rbrakk>
   \<Longrightarrow> \<exists>a C' fs. v = Addr a \<and> h a = Some(C',fs) \<and> P \<turnstile> C' \<preceq>\<^sup>* C"
-(*<*)
-apply (drule conf_ClassD)
-apply auto
-done
-(*>*)
+(*<*)by (auto dest: conf_ClassD)(*>*)
 
 
 subsection\<open>Value list conformance \<open>[:\<le>]\<close>\<close>
 
 lemma confs_widens [trans]: "\<lbrakk>P,h \<turnstile> vs [:\<le>] Ts; P \<turnstile> Ts [\<le>] Ts'\<rbrakk> \<Longrightarrow> P,h \<turnstile> vs [:\<le>] Ts'"
-(*<*)
-  apply (rule list_all2_trans)
-    apply (rule conf_widen, assumption, assumption)
-   apply assumption
-  apply assumption
-  done
-(*>*)
+(*<*)by(auto intro: list_all2_trans conf_widen)(*>*)
 
 lemma confs_rev: "P,h \<turnstile> rev s [:\<le>] t = (P,h \<turnstile> s [:\<le>] rev t)"
-(*<*)
-  apply rule
-  apply (rule subst [OF list_all2_rev])
-  apply simp
-  apply (rule subst [OF list_all2_rev])
-  apply simp
-  done
-(*>*)
+(*<*)by (simp add: list_all2_rev1)(*>*)
 
 lemma confs_conv_map:
   "\<And>Ts'. P,h \<turnstile> vs [:\<le>] Ts' = (\<exists>Ts. map typeof\<^bsub>h\<^esub> vs = map Some Ts \<and> P \<turnstile> Ts [\<le>] Ts')"
 (*<*)
-apply(induct vs)
- apply simp
-apply(case_tac Ts')
-apply(auto simp add:conf_def)
-done
+proof(induct vs)
+  case (Cons a vs)
+  then show ?case by(case_tac Ts') (auto simp add:conf_def)
+qed simp
 (*>*)
 
 lemma confs_hext: "P,h \<turnstile> vs [:\<le>] Ts \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> vs [:\<le>] Ts"
 (*<*)by (erule list_all2_mono, erule conf_hext, assumption)(*>*)
 
 lemma confs_Cons2: "P,h \<turnstile> xs [:\<le>] y#ys = (\<exists>z zs. xs = z#zs \<and> P,h \<turnstile> z :\<le> y \<and> P,h \<turnstile> zs [:\<le>] ys)"
 (*<*)by (rule list_all2_Cons2)(*>*)
 
 
 subsection "Object conformance"
 
 lemma oconf_hext: "P,h \<turnstile> obj \<surd> \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,h' \<turnstile> obj \<surd>"
-(*<*)
-apply (unfold oconf_def)
-apply (fastforce elim:conf_hext)
-done
-(*>*)
+(*<*)by (fastforce elim:conf_hext simp: oconf_def)(*>*)
 
 lemma oconf_init_fields:
  "P \<turnstile> C has_fields FDTs \<Longrightarrow> P,h \<turnstile> (C, init_fields FDTs) \<surd>"
 by(fastforce simp add: has_field_def oconf_def init_fields_def map_of_map
             dest: has_fields_fun)
 
 lemma oconf_fupd [intro?]:
   "\<lbrakk> P \<turnstile> C has F:T in D; P,h \<turnstile> v :\<le> T; P,h \<turnstile> (C,fs) \<surd> \<rbrakk> 
   \<Longrightarrow> P,h \<turnstile> (C, fs((F,D)\<mapsto>v)) \<surd>"
-(*<*)
-  apply (unfold oconf_def has_field_def)
-  apply clarsimp
-  apply (drule (1) has_fields_fun)
-  apply (auto simp add: fun_upd_apply)
-  done                                    
-(*>*)
+(*<*)by (auto dest: has_fields_fun simp add: oconf_def has_field_def fun_upd_apply)(*>*)
 
 (*<*)
 lemmas oconf_new = oconf_hext [OF _ hext_new]
 lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
 (*>*)
 
 subsection "Heap conformance"
 
 lemma hconfD: "\<lbrakk> P \<turnstile> h \<surd>; h a = Some obj \<rbrakk> \<Longrightarrow> P,h \<turnstile> obj \<surd>"
-(*<*)
-apply (unfold hconf_def)
-apply (fast)
-done
-(*>*)
+(*<*)by (unfold hconf_def) fast(*>*)
 
 lemma hconf_new: "\<lbrakk> P \<turnstile> h \<surd>; h a = None; P,h \<turnstile> obj \<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h(a\<mapsto>obj) \<surd>"
 (*<*)by (unfold hconf_def) (auto intro: oconf_new preallocated_new)(*>*)
 
 lemma hconf_upd_obj: "\<lbrakk> P \<turnstile> h\<surd>; h a = Some(C,fs); P,h \<turnstile> (C,fs')\<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h(a\<mapsto>(C,fs'))\<surd>"
 (*<*)by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)(*>*)
 
 
 subsection "Local variable conformance"
 
 lemma lconf_hext: "\<lbrakk> P,h \<turnstile> l (:\<le>) E; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>) E"
-(*<*)
-apply (unfold lconf_def)
-apply  (fast elim: conf_hext)
-done
-(*>*)
+(*<*)by (unfold lconf_def) (fast elim: conf_hext)(*>*)
 
 lemma lconf_upd:
   "\<lbrakk> P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T; E V = Some T \<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>) E"
-(*<*)
-apply (unfold lconf_def)
-apply auto
-done
-(*>*)
+(*<*)by (unfold lconf_def) auto(*>*)
 
 lemma lconf_empty[iff]: "P,h \<turnstile> Map.empty (:\<le>) E"
 (*<*)by(simp add:lconf_def)(*>*)
 
 lemma lconf_upd2: "\<lbrakk>P,h \<turnstile> l (:\<le>) E; P,h \<turnstile> v :\<le> T\<rbrakk> \<Longrightarrow> P,h \<turnstile> l(V\<mapsto>v) (:\<le>) E(V\<mapsto>T)"
 (*<*)by(simp add:lconf_def)(*>*)
 
 
 end
diff --git a/thys/Jinja/Common/Decl.thy b/thys/Jinja/Common/Decl.thy
--- a/thys/Jinja/Common/Decl.thy
+++ b/thys/Jinja/Common/Decl.thy
@@ -1,63 +1,64 @@
 (*  Title:      HOL/MicroJava/J/Decl.thy
 
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 section \<open>Class Declarations and Programs\<close>
 
 theory Decl imports Type begin
 
 type_synonym 
   fdecl    = "vname \<times> ty"        \<comment> \<open>field declaration\<close>
 type_synonym
   'm mdecl = "mname \<times> ty list \<times> ty \<times> 'm"     \<comment> \<open>method = name, arg.\ types, return type, body\<close>
 type_synonym
   'm "class" = "cname \<times> fdecl list \<times> 'm mdecl list"       \<comment> \<open>class = superclass, fields, methods\<close>
 type_synonym
   'm cdecl = "cname \<times> 'm class"  \<comment> \<open>class declaration\<close>
 type_synonym
   'm prog  = "'m cdecl list"     \<comment> \<open>program\<close>
 
 (*<*)
 translations
   (type) "fdecl"   <= (type) "vname \<times> ty"
   (type) "'c mdecl" <= (type) "mname \<times> ty list \<times> ty \<times> 'c"
   (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
   (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
   (type) "'c prog" <= (type) "('c cdecl) list"
 (*>*)
 
 definition "class" :: "'m prog \<Rightarrow> cname \<rightharpoonup> 'm class"
 where
   "class  \<equiv>  map_of"
 
 definition is_class :: "'m prog \<Rightarrow> cname \<Rightarrow> bool"
 where
   "is_class P C  \<equiv>  class P C \<noteq> None"
 
 lemma finite_is_class: "finite {C. is_class P C}"
 
 (*<*)
-apply (unfold is_class_def class_def)
-apply (fold dom_def)
-apply (rule finite_dom_map_of)
-done
+proof -
+  have "{C. is_class P C} = dom (map_of P)"
+   by (simp add: is_class_def class_def dom_def)
+  thus ?thesis by (simp add: finite_dom_map_of)
+qed
 (*>*)
 
 definition is_type :: "'m prog \<Rightarrow> ty \<Rightarrow> bool"
 where
   "is_type P T  \<equiv>
   (case T of Void \<Rightarrow> True | Boolean \<Rightarrow> True | Integer \<Rightarrow> True | NT \<Rightarrow> True
    | Class C \<Rightarrow> is_class P C)"
 
 lemma is_type_simps [simp]:
   "is_type P Void \<and> is_type P Boolean \<and> is_type P Integer \<and>
   is_type P NT \<and> is_type P (Class C) = is_class P C"
 (*<*)by(simp add:is_type_def)(*>*)
 
 
 abbreviation
   "types P == Collect (is_type P)"
 
 end
diff --git a/thys/Jinja/Common/Objects.thy b/thys/Jinja/Common/Objects.thy
--- a/thys/Jinja/Common/Objects.thy
+++ b/thys/Jinja/Common/Objects.thy
@@ -1,183 +1,156 @@
 (*  Title:      HOL/MicroJava/J/State.thy
 
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 section \<open>Objects and the Heap\<close>
 
 theory Objects imports TypeRel Value begin
 
 subsection\<open>Objects\<close>
 
 type_synonym
   fields = "vname \<times> cname \<rightharpoonup> val"  \<comment> \<open>field name, defining class, value\<close>
 type_synonym
   obj = "cname \<times> fields"    \<comment> \<open>class instance with class name and fields\<close>
 
 definition obj_ty  :: "obj \<Rightarrow> ty"
 where
   "obj_ty obj  \<equiv>  Class (fst obj)"
 
 definition init_fields :: "((vname \<times> cname) \<times> ty) list \<Rightarrow> fields"
 where
   "init_fields  \<equiv>  map_of \<circ> map (\<lambda>(F,T). (F,default_val T))"
   
   \<comment> \<open>a new, blank object with default values in all fields:\<close>
 definition blank :: "'m prog \<Rightarrow> cname \<Rightarrow> obj"
 where
   "blank P C  \<equiv>  (C,init_fields (fields P C))" 
 
 lemma [simp]: "obj_ty (C,fs) = Class C"
 (*<*)by (simp add: obj_ty_def)(*>*)
 
 subsection\<open>Heap\<close>
 
 type_synonym heap  = "addr \<rightharpoonup> obj"
 
 abbreviation
   cname_of :: "heap \<Rightarrow> addr \<Rightarrow> cname" where
   "cname_of hp a == fst (the (hp a))"
 
 definition new_Addr  :: "heap \<Rightarrow> addr option"
 where
   "new_Addr h  \<equiv>  if \<exists>a. h a = None then Some(LEAST a. h a = None) else None"
 
 definition cast_ok :: "'m prog \<Rightarrow> cname \<Rightarrow> heap \<Rightarrow> val \<Rightarrow> bool"
 where
   "cast_ok P C h v  \<equiv>  v = Null \<or> P \<turnstile> cname_of h (the_Addr v) \<preceq>\<^sup>* C"
 
 definition hext :: "heap \<Rightarrow> heap \<Rightarrow> bool" ("_ \<unlhd> _" [51,51] 50)
 where
   "h \<unlhd> h'  \<equiv>  \<forall>a C fs. h a = Some(C,fs) \<longrightarrow> (\<exists>fs'. h' a = Some(C,fs'))"
 
 primrec typeof_h :: "heap \<Rightarrow> val \<Rightarrow> ty option"  ("typeof\<^bsub>_\<^esub>")
 where
   "typeof\<^bsub>h\<^esub>  Unit    = Some Void"
 | "typeof\<^bsub>h\<^esub>  Null    = Some NT"
 | "typeof\<^bsub>h\<^esub> (Bool b) = Some Boolean"
 | "typeof\<^bsub>h\<^esub> (Intg i) = Some Integer"
 | "typeof\<^bsub>h\<^esub> (Addr a) = (case h a of None \<Rightarrow> None | Some(C,fs) \<Rightarrow> Some(Class C))"
 
 lemma new_Addr_SomeD:
   "new_Addr h = Some a \<Longrightarrow> h a = None"
  (*<*)by(fastforce simp add:new_Addr_def split:if_splits intro:LeastI)(*>*)
 
 lemma [simp]: "(typeof\<^bsub>h\<^esub> v = Some Boolean) = (\<exists>b. v = Bool b)"
  (*<*)by(induct v) auto(*>*)
 
 lemma [simp]: "(typeof\<^bsub>h\<^esub> v = Some Integer) = (\<exists>i. v = Intg i)"
 (*<*)by(cases v) auto(*>*)
 
 lemma [simp]: "(typeof\<^bsub>h\<^esub> v = Some NT) = (v = Null)"
  (*<*)by(cases v) auto(*>*)
 
 lemma [simp]: "(typeof\<^bsub>h\<^esub> v = Some(Class C)) = (\<exists>a fs. v = Addr a \<and> h a = Some(C,fs))"
  (*<*)by(cases v) auto(*>*)
 
 lemma [simp]: "h a = Some(C,fs) \<Longrightarrow> typeof\<^bsub>(h(a\<mapsto>(C,fs')))\<^esub> v = typeof\<^bsub>h\<^esub> v"
  (*<*)by(induct v) (auto simp:fun_upd_apply)(*>*)
 
 text\<open>For literal values the first parameter of @{term typeof} can be
 set to @{term Map.empty} because they do not contain addresses:\<close>
 
 abbreviation
   typeof :: "val \<Rightarrow> ty option" where
   "typeof v == typeof_h Map.empty v"
 
 lemma typeof_lit_typeof:
   "typeof v = Some T \<Longrightarrow> typeof\<^bsub>h\<^esub> v = Some T"
  (*<*)by(cases v) auto(*>*)
 
 lemma typeof_lit_is_type: 
   "typeof v = Some T \<Longrightarrow> is_type P T"
  (*<*)by (induct v) (auto simp:is_type_def)(*>*)
 
 
 subsection \<open>Heap extension \<open>\<unlhd>\<close>\<close>
 
 lemma hextI: "\<forall>a C fs. h a = Some(C,fs) \<longrightarrow> (\<exists>fs'. h' a = Some(C,fs')) \<Longrightarrow> h \<unlhd> h'"
-(*<*)
-apply (unfold hext_def)
-apply auto
-done
-(*>*)
+(*<*)by(auto simp: hext_def)(*>*)
 
 lemma hext_objD: "\<lbrakk> h \<unlhd> h'; h a = Some(C,fs) \<rbrakk> \<Longrightarrow> \<exists>fs'. h' a = Some(C,fs')"
-(*<*)
-apply (unfold hext_def)
-apply (force)
-done
-(*>*)
+(*<*)by(auto simp: hext_def)(*>*)
 
 lemma hext_refl [iff]: "h \<unlhd> h"
-(*<*)
-apply (rule hextI)
-apply (fast)
-done
-(*>*)
+(*<*)by (rule hextI) fast(*>*)
 
 lemma hext_new [simp]: "h a = None \<Longrightarrow> h \<unlhd> h(a\<mapsto>x)"
-(*<*)
-apply (rule hextI)
-apply (auto simp:fun_upd_apply)
-done
-(*>*)
+(*<*)by (rule hextI) (auto simp:fun_upd_apply)(*>*)
 
 lemma hext_trans: "\<lbrakk> h \<unlhd> h'; h' \<unlhd> h'' \<rbrakk> \<Longrightarrow> h \<unlhd> h''"
-(*<*)
-apply (rule hextI)
-apply (fast dest: hext_objD)
-done
-(*>*)
+(*<*)by (rule hextI) (fast dest: hext_objD)(*>*)
 
 lemma hext_upd_obj: "h a = Some (C,fs) \<Longrightarrow> h \<unlhd> h(a\<mapsto>(C,fs'))"
-(*<*)
-apply (rule hextI)
-apply (auto simp:fun_upd_apply)
-done
-(*>*)
+(*<*)by (rule hextI) (auto simp:fun_upd_apply)(*>*)
 
 lemma hext_typeof_mono: "\<lbrakk> h \<unlhd> h'; typeof\<^bsub>h\<^esub> v = Some T \<rbrakk> \<Longrightarrow> typeof\<^bsub>h'\<^esub> v = Some T"
 (*<*)
-apply(cases v)
-    apply simp
-   apply simp
-  apply simp
- apply simp
-apply(fastforce simp:hext_def)
-done
+proof(cases v)
+  case Addr assume "h \<unlhd> h'" and "typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>"
+  then show ?thesis using Addr by(fastforce simp:hext_def)
+qed simp_all
 (*>*)
 
 text \<open>Code generator setup for @{term "new_Addr"}\<close>
 
 definition gen_new_Addr :: "heap \<Rightarrow> addr \<Rightarrow> addr option"
 where "gen_new_Addr h n \<equiv> if \<exists>a. a \<ge> n \<and> h a = None then Some(LEAST a. a \<ge> n \<and> h a = None) else None"
 
 lemma new_Addr_code_code [code]:
   "new_Addr h = gen_new_Addr h 0"
 by(simp add: new_Addr_def gen_new_Addr_def split del: if_split cong: if_cong)
 
 lemma gen_new_Addr_code [code]:
   "gen_new_Addr h n = (if h n = None then Some n else gen_new_Addr h (Suc n))"
 apply(simp add: gen_new_Addr_def)
 apply(rule impI)
 apply(rule conjI)
  apply safe[1]
   apply(fastforce intro: Least_equality)
  apply(rule arg_cong[where f=Least])
  apply(rule ext)
  apply(case_tac "n = ac")
   apply simp
  apply(auto)[1]
 apply clarify
 apply(subgoal_tac "a = n")
  apply simp
  apply(rule Least_equality)
  apply auto[2]
 apply(rule ccontr)
 apply(erule_tac x="a" in allE)
 apply simp
 done
 
 end
diff --git a/thys/Jinja/Common/TypeRel.thy b/thys/Jinja/Common/TypeRel.thy
--- a/thys/Jinja/Common/TypeRel.thy
+++ b/thys/Jinja/Common/TypeRel.thy
@@ -1,632 +1,679 @@
 (*  Title:      Jinja/Common/TypeRel.thy
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Relations between Jinja Types\<close>
 
 theory TypeRel imports 
   "HOL-Library.Transitive_Closure_Table"
   Decl 
 begin
 
 subsection\<open>The subclass relations\<close>
 
 inductive_set
   subcls1 :: "'m prog \<Rightarrow> (cname \<times> cname) set"
   and subcls1' :: "'m prog \<Rightarrow> [cname, cname] \<Rightarrow> bool" ("_ \<turnstile> _ \<prec>\<^sup>1 _" [71,71,71] 70)
   for P :: "'m prog"
 where
   "P \<turnstile> C  \<prec>\<^sup>1 D \<equiv> (C,D) \<in> subcls1 P"
 | subcls1I: "\<lbrakk>class P C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> P \<turnstile> C \<prec>\<^sup>1 D"
 
 abbreviation
   subcls  :: "'m prog \<Rightarrow> [cname, cname] \<Rightarrow> bool" ("_ \<turnstile> _ \<preceq>\<^sup>* _"  [71,71,71] 70)
   where "P \<turnstile> C  \<preceq>\<^sup>*  D \<equiv> (C,D) \<in> (subcls1 P)\<^sup>*"
 
 lemma subcls1D: "P \<turnstile> C \<prec>\<^sup>1 D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class P C = Some (D,fs,ms))"
 (*<*)by(erule subcls1.induct)(fastforce simp add:is_class_def)(*>*)
 
 lemma [iff]: "\<not> P \<turnstile> Object \<prec>\<^sup>1 C"
 (*<*)by(fastforce dest:subcls1D)(*>*)
 
 lemma [iff]: "(P \<turnstile> Object \<preceq>\<^sup>* C) = (C = Object)"
 (*<*)
-apply(rule iffI)
- apply(erule converse_rtranclE)
-  apply simp_all
-done
+proof(rule iffI)
+ assume "P \<turnstile> Object \<preceq>\<^sup>* C" then show "C = Object"
+  by(auto elim: converse_rtranclE)
+qed simp
 (*>*)
 
 lemma subcls1_def2:
   "subcls1 P =
      (SIGMA C:{C. is_class P C}. {D. C\<noteq>Object \<and> fst (the (class P C))=D})"
 (*<*)
   by (fastforce simp:is_class_def dest: subcls1D elim: subcls1I)
 (*>*)
 
 lemma finite_subcls1: "finite (subcls1 P)"
 (*<*)
-apply (simp add: subcls1_def2)
-apply(rule finite_SigmaI [OF finite_is_class])
-apply(rule_tac B = "{fst (the (class P C))}" in finite_subset)
-apply  auto
-done
+proof -
+  let ?SIG = "SIGMA C:{C. is_class P C}. {D. fst (the (class P C)) = D \<and> C \<noteq> Object}"
+  have "subcls1 P = ?SIG" by(simp add: subcls1_def2)
+  also have "finite ?SIG"
+  proof(rule finite_SigmaI [OF finite_is_class])
+    fix C assume C_in: "C \<in> {C. is_class P C}"
+    then show "finite {D. fst (the (class P C)) = D \<and> C \<noteq> Object}"
+     by(rule_tac finite_subset[where B = "{fst (the (class P C))}"]) auto
+  qed
+  ultimately show ?thesis by simp
+qed
 (*>*)
 (*
 lemma subcls_is_class: "(C,D) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> is_class P C"
 apply (unfold is_class_def)
 apply(erule trancl_trans_induct)
 apply (auto dest!: subcls1D)
 done
 
 lemma subcls_is_class: "P \<turnstile> C \<preceq>\<^sup>* D \<Longrightarrow> is_class P D \<longrightarrow> is_class P C"
 apply (unfold is_class_def)
 apply (erule rtrancl_induct)
 apply  (drule_tac [2] subcls1D)
 apply  auto
 done
 *)
 
 
 subsection\<open>The subtype relations\<close>
 
 inductive
   widen   :: "'m prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ \<le> _"   [71,71,71] 70)
   for P :: "'m prog"
 where
   widen_refl[iff]: "P \<turnstile> T \<le> T"
 | widen_subcls: "P \<turnstile> C \<preceq>\<^sup>* D  \<Longrightarrow>  P \<turnstile> Class C \<le> Class D"
 | widen_null[iff]: "P \<turnstile> NT \<le> Class C"
 
 abbreviation
   widens :: "'m prog \<Rightarrow> ty list \<Rightarrow> ty list \<Rightarrow> bool"
     ("_ \<turnstile> _ [\<le>] _" [71,71,71] 70) where
   "widens P Ts Ts' \<equiv> list_all2 (widen P) Ts Ts'"
 
 lemma [iff]: "(P \<turnstile> T \<le> Void) = (T = Void)"
 (*<*)by (auto elim: widen.cases)(*>*)
 
 lemma [iff]: "(P \<turnstile> T \<le> Boolean) = (T = Boolean)"
 (*<*)by (auto elim: widen.cases)(*>*)
 
 lemma [iff]: "(P \<turnstile> T \<le> Integer) = (T = Integer)"
 (*<*)by (auto elim: widen.cases)(*>*)
 
 lemma [iff]: "(P \<turnstile> Void \<le> T) = (T = Void)"
 (*<*)by (auto elim: widen.cases)(*>*)
 
 lemma [iff]: "(P \<turnstile> Boolean \<le> T) = (T = Boolean)"
 (*<*)by (auto elim: widen.cases)(*>*)
 
 lemma [iff]: "(P \<turnstile> Integer \<le> T) = (T = Integer)"
 (*<*)by (auto elim: widen.cases)(*>*)
 
 
 lemma Class_widen: "P \<turnstile> Class C \<le> T  \<Longrightarrow>  \<exists>D. T = Class D"
 (*<*)
-apply (ind_cases "P \<turnstile> Class C \<le> T")
-apply auto
-done
+by (ind_cases "P \<turnstile> Class C \<le> T") auto
 (*>*)
 
 lemma [iff]: "(P \<turnstile> T \<le> NT) = (T = NT)"
 (*<*)
-apply(cases T)
-apply(auto dest:Class_widen)
-done
+by(cases T) (auto dest:Class_widen)
 (*>*)
 
 lemma Class_widen_Class [iff]: "(P \<turnstile> Class C \<le> Class D) = (P \<turnstile> C \<preceq>\<^sup>* D)"
 (*<*)
-apply (rule iffI)
-apply (ind_cases "P \<turnstile> Class C \<le> Class D")
-apply (auto elim: widen_subcls)
-done
+proof(rule iffI)
+  show "P \<turnstile> Class C \<le> Class D \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* D"
+  proof(ind_cases "P \<turnstile> Class C \<le> Class D") qed(auto)
+qed(auto elim: widen_subcls)
 (*>*)
 
 lemma widen_Class: "(P \<turnstile> T \<le> Class C) = (T = NT \<or> (\<exists>D. T = Class D \<and> P \<turnstile> D \<preceq>\<^sup>* C))"
 (*<*)by(induct T, auto)(*>*)
 
 
 lemma widen_trans[trans]: "\<lbrakk>P \<turnstile> S \<le> U; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> P \<turnstile> S \<le> T"
 (*<*)
 proof -
   assume "P\<turnstile>S \<le> U" thus "\<And>T. P \<turnstile> U \<le> T \<Longrightarrow> P \<turnstile> S \<le> T"
   proof induct
     case (widen_refl T T') thus "P \<turnstile> T \<le> T'" .
   next
     case (widen_subcls C D T)
     then obtain E where "T = Class E" by (blast dest: Class_widen)
     with widen_subcls show "P \<turnstile> Class C \<le> T" by (auto elim: rtrancl_trans)
   next
     case (widen_null C RT)
     then obtain D where "RT = Class D" by (blast dest: Class_widen)
     thus "P \<turnstile> NT \<le> RT" by auto
   qed
 qed
 (*>*)
 
 lemma widens_trans [trans]: "\<lbrakk>P \<turnstile> Ss [\<le>] Ts; P \<turnstile> Ts [\<le>] Us\<rbrakk> \<Longrightarrow> P \<turnstile> Ss [\<le>] Us"
 (*<*)by (rule list_all2_trans, rule widen_trans)(*>*)
 
 
 (*<*)
 lemmas widens_refl [iff] = list_all2_refl [of "widen P", OF widen_refl] for P
 lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P
 (*>*)
 
 
 subsection\<open>Method lookup\<close>
 
 inductive
   Methods :: "['m prog, cname, mname \<rightharpoonup> (ty list \<times> ty \<times> 'm) \<times> cname] \<Rightarrow> bool"
                     ("_ \<turnstile> _ sees'_methods _" [51,51,51] 50)
   for P :: "'m prog"
 where
   sees_methods_Object:
  "\<lbrakk> class P Object = Some(D,fs,ms); Mm = map_option (\<lambda>m. (m,Object)) \<circ> map_of ms \<rbrakk>
   \<Longrightarrow> P \<turnstile> Object sees_methods Mm"
 | sees_methods_rec:
  "\<lbrakk> class P C = Some(D,fs,ms); C \<noteq> Object; P \<turnstile> D sees_methods Mm;
     Mm' = Mm ++ (map_option (\<lambda>m. (m,C)) \<circ> map_of ms) \<rbrakk>
   \<Longrightarrow> P \<turnstile> C sees_methods Mm'"
 
 lemma sees_methods_fun:
 assumes 1: "P \<turnstile> C sees_methods Mm"
 shows "\<And>Mm'. P \<turnstile> C sees_methods Mm' \<Longrightarrow> Mm' = Mm"
  (*<*)
 using 1
 proof induct
   case (sees_methods_rec C D fs ms Dres Cres Cres')
   have "class": "class P C = Some (D, fs, ms)"
    and notObj: "C \<noteq> Object" and Dmethods: "P \<turnstile> D sees_methods Dres"
    and IH: "\<And>Dres'. P \<turnstile> D sees_methods Dres' \<Longrightarrow> Dres' = Dres"
    and Cres: "Cres = Dres ++ (map_option (\<lambda>m. (m,C)) \<circ> map_of ms)"
    and Cmethods': "P \<turnstile> C sees_methods Cres'" by fact+
   from Cmethods' notObj "class" obtain Dres'
     where Dmethods': "P \<turnstile> D sees_methods Dres'"
      and Cres': "Cres' = Dres' ++ (map_option (\<lambda>m. (m,C)) \<circ> map_of ms)"
     by(auto elim: Methods.cases)
   from Cres Cres' IH[OF Dmethods'] show "Cres' = Cres" by simp
 next
   case sees_methods_Object thus ?case by(auto elim: Methods.cases)
 qed
 (*>*)
 
 lemma visible_methods_exist:
   "P \<turnstile> C sees_methods Mm \<Longrightarrow> Mm M = Some(m,D) \<Longrightarrow>
    (\<exists>D' fs ms. class P D = Some(D',fs,ms) \<and> map_of ms M = Some m)"
  (*<*)by(induct rule:Methods.induct) auto(*>*)
 
 lemma sees_methods_decl_above:
 assumes Csees: "P \<turnstile> C sees_methods Mm"
 shows "Mm M = Some(m,D) \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* D"
  (*<*)
 using Csees
 proof induct
   case sees_methods_Object thus ?case by auto
 next
   case sees_methods_rec thus ?case
     by(fastforce simp:map_option_case split:option.splits
                 elim:converse_rtrancl_into_rtrancl[OF subcls1I])
 qed
 (*>*)
 
 lemma sees_methods_idemp:
 assumes Cmethods: "P \<turnstile> C sees_methods Mm"
 shows "\<And>m D. Mm M = Some(m,D) \<Longrightarrow>
               \<exists>Mm'. (P \<turnstile> D sees_methods Mm') \<and> Mm' M = Some(m,D)"
 (*<*)
 using Cmethods
 proof induct
   case sees_methods_Object thus ?case
     by(fastforce dest: Methods.sees_methods_Object)
 next
   case sees_methods_rec thus ?case
     by(fastforce split:option.splits dest: Methods.sees_methods_rec)
 qed
 (*>*)
 
 (*FIXME something wrong with induct: need to attache [consumes 1]
 directly to proof of thm, declare does not work. *)
 
 lemma sees_methods_decl_mono:
 assumes sub: "P \<turnstile> C' \<preceq>\<^sup>* C"
 shows "P \<turnstile> C sees_methods Mm \<Longrightarrow>
        \<exists>Mm' Mm\<^sub>2. P \<turnstile> C' sees_methods Mm' \<and> Mm' = Mm ++ Mm\<^sub>2 \<and>
                  (\<forall>M m D. Mm\<^sub>2 M = Some(m,D) \<longrightarrow> P \<turnstile> D \<preceq>\<^sup>* C)"
 (*<*)
       (is "_ \<Longrightarrow> \<exists>Mm' Mm2. ?Q C' C Mm' Mm2")
 using sub
 proof (induct rule:converse_rtrancl_induct)
   assume "P \<turnstile> C sees_methods Mm"
   hence "?Q C C Mm Map.empty" by simp
   thus "\<exists>Mm' Mm2. ?Q C C Mm' Mm2" by blast
 next
   fix C'' C'
   assume sub1: "P \<turnstile> C'' \<prec>\<^sup>1 C'" and sub: "P \<turnstile> C' \<preceq>\<^sup>* C"
   and IH: "P \<turnstile> C sees_methods Mm \<Longrightarrow>
            \<exists>Mm' Mm2. P \<turnstile> C' sees_methods Mm' \<and>
                 Mm' = Mm ++ Mm2 \<and> (\<forall>M m D. Mm2 M = Some(m,D) \<longrightarrow> P \<turnstile> D \<preceq>\<^sup>* C)"
   and Csees: "P \<turnstile> C sees_methods Mm"
   from IH[OF Csees] obtain Mm' Mm2 where C'sees: "P \<turnstile> C' sees_methods Mm'"
     and Mm': "Mm' = Mm ++ Mm2"
     and subC:"\<forall>M m D. Mm2 M = Some(m,D) \<longrightarrow> P \<turnstile> D \<preceq>\<^sup>* C" by blast
   obtain fs ms where "class": "class P C'' = Some(C',fs,ms)" "C'' \<noteq> Object"
     using subcls1D[OF sub1] by blast
   let ?Mm3 = "map_option (\<lambda>m. (m,C'')) \<circ> map_of ms"
   have "P \<turnstile> C'' sees_methods (Mm ++ Mm2) ++ ?Mm3"
     using sees_methods_rec[OF "class" C'sees refl] Mm' by simp
   hence "?Q C'' C ((Mm ++ Mm2) ++ ?Mm3) (Mm2++?Mm3)"
     using converse_rtrancl_into_rtrancl[OF sub1 sub]
     by simp (simp add:map_add_def subC split:option.split)
   thus "\<exists>Mm' Mm2. ?Q C'' C Mm' Mm2" by blast
 qed
 (*>*)
 
 
 definition Method :: "'m prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> 'm \<Rightarrow> cname \<Rightarrow> bool"
             ("_ \<turnstile> _ sees _: _\<rightarrow>_ = _ in _" [51,51,51,51,51,51,51] 50)
 where
   "P \<turnstile> C sees M: Ts\<rightarrow>T = m in D  \<equiv>
   \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> Mm M = Some((Ts,T,m),D)"
 
 definition has_method :: "'m prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> bool" ("_ \<turnstile> _ has _" [51,0,51] 50)
 where
   "P \<turnstile> C has M \<equiv> \<exists>Ts T m D. P \<turnstile> C sees M:Ts\<rightarrow>T = m in D"
 
 lemma sees_method_fun:
   "\<lbrakk>P \<turnstile> C sees M:TS\<rightarrow>T = m in D; P \<turnstile> C sees M:TS'\<rightarrow>T' = m' in D' \<rbrakk>
    \<Longrightarrow> TS' = TS \<and> T' = T \<and> m' = m \<and> D' = D"
  (*<*)by(fastforce dest: sees_methods_fun simp:Method_def)(*>*)
 
 lemma sees_method_decl_above:
   "P \<turnstile> C sees M:Ts\<rightarrow>T = m in D \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* D"
  (*<*)by(clarsimp simp:Method_def sees_methods_decl_above)(*>*)
 
 lemma visible_method_exists:
   "P \<turnstile> C sees M:Ts\<rightarrow>T = m in D \<Longrightarrow>
   \<exists>D' fs ms. class P D = Some(D',fs,ms) \<and> map_of ms M = Some(Ts,T,m)"
 (*<*)by(fastforce simp:Method_def dest!: visible_methods_exist)(*>*)
 
 
 lemma sees_method_idemp:
   "P \<turnstile> C sees M:Ts\<rightarrow>T=m in D \<Longrightarrow> P \<turnstile> D sees M:Ts\<rightarrow>T=m in D"
  (*<*)by(fastforce simp: Method_def intro:sees_methods_idemp)(*>*)
 
 lemma sees_method_decl_mono:
-  "\<lbrakk> P \<turnstile> C' \<preceq>\<^sup>* C; P \<turnstile> C sees M:Ts\<rightarrow>T = m in D;
-     P \<turnstile> C' sees M:Ts'\<rightarrow>T' = m' in D' \<rbrakk> \<Longrightarrow> P \<turnstile> D' \<preceq>\<^sup>* D"
+assumes sub: "P \<turnstile> C' \<preceq>\<^sup>* C" and
+        C_sees: "P \<turnstile> C sees M:Ts\<rightarrow>T=m in D" and
+        C'_sees: "P \<turnstile> C' sees M:Ts'\<rightarrow>T'=m' in D'"
+shows   "P \<turnstile> D' \<preceq>\<^sup>* D"
  (*<*)
-apply(frule sees_method_decl_above)
-apply(unfold Method_def)
-apply clarsimp
-apply(drule (1) sees_methods_decl_mono)
-apply clarsimp
-apply(drule (1) sees_methods_fun)
-apply clarsimp
-apply(blast intro:rtrancl_trans)
-done
+proof -
+  obtain Ms where Ms: "P \<turnstile> C sees_methods Ms"
+    using C_sees by(auto simp: Method_def)
+  obtain Ms' Ms2 where Ms': "P \<turnstile> C' sees_methods Ms'" and
+     Ms'_def: "Ms' = Ms ++ Ms2" and
+     Ms2_imp: "(\<forall>M m D. Ms2 M = \<lfloor>(m, D)\<rfloor> \<longrightarrow> P \<turnstile> D \<preceq>\<^sup>* C)"
+    using sees_methods_decl_mono[OF sub Ms] by clarsimp
+  have "(Ms ++ Ms2) M = \<lfloor>((Ts', T', m'), D')\<rfloor>"
+    using C'_sees sees_methods_fun[OF Ms'] Ms'_def by(clarsimp simp: Method_def)
+  then have "Ms2 M = \<lfloor>((Ts', T', m'), D')\<rfloor> \<or>
+             Ms2 M = None \<and> Ts = Ts' \<and> T = T' \<and> m = m' \<and> D = D'"
+    using C_sees sees_methods_fun[OF Ms] by(clarsimp simp: Method_def)
+  also have "Ms2 M = \<lfloor>((Ts', T', m'), D')\<rfloor> \<Longrightarrow> P \<turnstile> D' \<preceq>\<^sup>* C"
+    using Ms2_imp by simp
+  ultimately show ?thesis using sub sees_method_decl_above[OF C_sees] by auto
+qed
 (*>*)
 
 lemma sees_method_is_class:
   "\<lbrakk> P \<turnstile> C sees M:Ts\<rightarrow>T = m in D \<rbrakk> \<Longrightarrow> is_class P C"
 (*<*)by (auto simp add: is_class_def Method_def elim: Methods.induct)(*>*)
 
 
 subsection\<open>Field lookup\<close>
 
 inductive
   Fields :: "['m prog, cname, ((vname \<times> cname) \<times> ty) list] \<Rightarrow> bool"
                   ("_ \<turnstile> _ has'_fields _" [51,51,51] 50)
   for P :: "'m prog"
 where
   has_fields_rec:
   "\<lbrakk> class P C = Some(D,fs,ms); C \<noteq> Object; P \<turnstile> D has_fields FDTs;
      FDTs' = map (\<lambda>(F,T). ((F,C),T)) fs @ FDTs \<rbrakk>
    \<Longrightarrow> P \<turnstile> C has_fields FDTs'"
 | has_fields_Object:
   "\<lbrakk> class P Object = Some(D,fs,ms); FDTs = map (\<lambda>(F,T). ((F,Object),T)) fs \<rbrakk>
    \<Longrightarrow> P \<turnstile> Object has_fields FDTs"
 
 lemma has_fields_fun:
 assumes 1: "P \<turnstile> C has_fields FDTs"
 shows "\<And>FDTs'. P \<turnstile> C has_fields FDTs' \<Longrightarrow> FDTs' = FDTs"
  (*<*)
 using 1
 proof induct
   case (has_fields_rec C D fs ms Dres Cres Cres')
   have "class": "class P C = Some (D, fs, ms)"
    and notObj: "C \<noteq> Object" and DFields: "P \<turnstile> D has_fields Dres"
    and IH: "\<And>Dres'. P \<turnstile> D has_fields Dres' \<Longrightarrow> Dres' = Dres"
    and Cres: "Cres = map (\<lambda>(F,T). ((F,C),T)) fs @ Dres"
    and CFields': "P \<turnstile> C has_fields Cres'" by fact+
   from CFields' notObj "class" obtain Dres'
     where DFields': "P \<turnstile> D has_fields Dres'"
      and Cres': "Cres' = map (\<lambda>(F,T). ((F,C),T)) fs @ Dres'"
     by(auto elim: Fields.cases)
   from Cres Cres' IH[OF DFields'] show "Cres' = Cres" by simp
 next
   case has_fields_Object thus ?case by(auto elim: Fields.cases)
 qed
 (*>*)
 
 lemma all_fields_in_has_fields:
 assumes sub: "P \<turnstile> C has_fields FDTs"
 shows "\<lbrakk> P \<turnstile> C \<preceq>\<^sup>* D; class P D = Some(D',fs,ms); (F,T) \<in> set fs \<rbrakk>
        \<Longrightarrow> ((F,D),T) \<in> set FDTs"
 (*<*)
-using sub apply(induct)
- apply(simp add:image_def)
- apply(erule converse_rtranclE)
-  apply(force)
- apply(drule subcls1D)
- apply fastforce
-apply(force simp:image_def)
-done
+using sub proof(induct)
+  case (has_fields_rec C D' fs ms FDTs FDTs')
+  then have C_D: "P \<turnstile> C \<preceq>\<^sup>* D" by simp
+  then show ?case proof(rule converse_rtranclE)
+    assume "C = D"
+    then show ?case using has_fields_rec by force
+  next
+    fix y assume sub1: "P \<turnstile> C \<prec>\<^sup>1 y" and sub2: "P \<turnstile> y \<preceq>\<^sup>* D"
+    then show ?case using has_fields_rec subcls1D[OF sub1] by simp
+  qed
+next
+  case (has_fields_Object D fs ms FDTs)
+  then show ?case by force
+qed
 (*>*)
 
 
 lemma has_fields_decl_above:
 assumes fields: "P \<turnstile> C has_fields FDTs"
 shows "((F,D),T) \<in> set FDTs \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* D"
 (*<*)
-using fields apply(induct)
- prefer 2 apply fastforce
-apply clarsimp
-apply(erule disjE)
- apply(clarsimp simp add:image_def)
-apply simp
-apply(blast dest:subcls1I converse_rtrancl_into_rtrancl)
-done
+using fields proof(induct)
+  case (has_fields_rec C D' fs ms FDTs FDTs')
+  then have "((F, D), T) \<in> (\<lambda>x. case x of (F, x) \<Rightarrow> ((F, C), x)) ` set fs \<or>
+    ((F, D), T) \<in> set FDTs" by clarsimp
+  then show ?case proof(rule disjE)
+    assume "((F, D), T) \<in> (\<lambda>x. case x of (F, x) \<Rightarrow> ((F, C), x)) ` set fs"
+    then show ?case using has_fields_rec by clarsimp
+  next
+    assume "((F, D), T) \<in> set FDTs"
+    then show ?case using has_fields_rec
+     by(blast dest:subcls1I converse_rtrancl_into_rtrancl)
+  qed
+next
+  case (has_fields_Object D fs ms FDTs)
+  then show ?case by fastforce
+qed
 (*>*)
 
 
 lemma subcls_notin_has_fields:
 assumes fields: "P \<turnstile> C has_fields FDTs"
 shows "((F,D),T) \<in> set FDTs \<Longrightarrow> (D,C) \<notin> (subcls1 P)\<^sup>+"
 (*<*)
-using fields apply(induct)
- prefer 2 apply(fastforce dest: tranclD)
-apply clarsimp
-apply(erule disjE)
- apply(clarsimp simp add:image_def)
- apply(drule tranclD)
- apply clarify
- apply(frule subcls1D)
- apply(fastforce dest:all_fields_in_has_fields)
-apply simp
-apply(blast dest:subcls1I trancl_into_trancl)
-done
+using fields proof(induct)
+  case (has_fields_rec C D' fs ms FDTs FDTs')
+  then have "((F, D), T) \<in> (\<lambda>x. case x of (F, x) \<Rightarrow> ((F, C), x)) ` set fs
+               \<or> ((F, D), T) \<in> set FDTs" by clarsimp
+  then show ?case proof(rule disjE)
+    assume "((F, D), T) \<in> (\<lambda>x. case x of (F, x) \<Rightarrow> ((F, C), x)) ` set fs"
+    then have CD[simp]: "C = D" and fs: "(F, T) \<in> set fs" by clarsimp+
+    then have "(D, D) \<in> (subcls1 P)\<^sup>+ \<Longrightarrow> False" proof -
+      assume DD: "(D, D) \<in> (subcls1 P)\<^sup>+"
+      obtain z where z1: "P \<turnstile> D \<prec>\<^sup>1 z" and z_s: "P \<turnstile> z \<preceq>\<^sup>* D"
+        using tranclD[OF DD] by clarsimp
+      have [simp]: "z = D'" using subcls1D[OF z1] has_fields_rec.hyps(1) by clarsimp
+      then have "((F, D), T) \<in> set FDTs"
+        using z_s all_fields_in_has_fields[OF has_fields_rec.hyps(3) _ has_fields_rec.hyps(1) fs]
+         by simp
+      then have "(D, z) \<notin> (subcls1 P)\<^sup>+" using has_fields_rec.hyps(4) by simp
+      then show False using z1 by auto
+    qed
+    then show ?case by clarsimp
+  next
+    assume "((F, D), T) \<in> set FDTs"
+    then show ?case using has_fields_rec by(blast dest:subcls1I trancl_into_trancl)
+  qed
+next
+  case (has_fields_Object D fs ms FDTs)
+  then show ?case by(fastforce dest: tranclD)
+qed
 (*>*)
 
 
 lemma has_fields_mono_lem:
 assumes sub: "P \<turnstile> D \<preceq>\<^sup>* C"
 shows "P \<turnstile> C has_fields FDTs
          \<Longrightarrow> \<exists>pre. P \<turnstile> D has_fields pre@FDTs \<and> dom(map_of pre) \<inter> dom(map_of FDTs) = {}"
 (*<*)
-using sub apply(induct rule:converse_rtrancl_induct)
- apply(rule_tac x = "[]" in exI)
- apply simp
-apply clarsimp
-apply(rename_tac D' D pre)
-apply(subgoal_tac "(D',C) : (subcls1 P)^+")
- prefer 2 apply(erule (1) rtrancl_into_trancl2)
-apply(drule subcls1D)
-apply clarsimp
-apply(rename_tac fs ms)
-apply(drule (2) has_fields_rec)
- apply(rule refl)
-apply(rule_tac x = "map (\<lambda>(F,T). ((F,D'),T)) fs @ pre" in exI)
-apply simp
-apply(simp add:Int_Un_distrib2)
-apply(rule equals0I)
-apply(auto dest: subcls_notin_has_fields simp:dom_map_of_conv_image_fst image_def)
-done
+using sub proof(induct rule:converse_rtrancl_induct)
+  case base
+  then show ?case by(rule_tac x = "[]" in exI) simp
+next
+  case (step D' D)
+  then obtain pre where D_flds: "P \<turnstile> D has_fields pre @ FDTs" and
+    dom: "dom (map_of pre) \<inter> dom (map_of FDTs) = {}" by clarsimp
+  have "(D',C) \<in> (subcls1 P)^+" by (rule rtrancl_into_trancl2[OF step.hyps(1,2)])
+  obtain fs ms where D'_cls: "class P D' = \<lfloor>(D, fs, ms)\<rfloor>" "D' \<noteq> Object"
+    using subcls1D[OF step.hyps(1)] by clarsimp+
+  have "P \<turnstile> D' has_fields map (\<lambda>(F, T). ((F, D'), T)) fs @ pre @ FDTs"
+    using has_fields_rec[OF D'_cls D_flds] by simp
+  also have "dom (map_of (map (\<lambda>(F, T). ((F, D'), T)) fs @ pre))
+                 \<inter> dom (map_of FDTs) = {}"
+    using dom subcls_notin_has_fields[OF D_flds, where D=D'] step.hyps(1)
+      by(auto simp:dom_map_of_conv_image_fst) fast
+  ultimately show ?case
+    by(rule_tac x = "map (\<lambda>(F,T). ((F,D'),T)) fs @ pre" in exI) simp
+qed
 (*>*)
 
 (* FIXME why is Field not displayed correctly? TypeRel qualifier seems to confuse printer*)
 definition has_field :: "'m prog \<Rightarrow> cname \<Rightarrow> vname \<Rightarrow> ty \<Rightarrow> cname \<Rightarrow> bool"
                    ("_ \<turnstile> _ has _:_ in _" [51,51,51,51,51] 50)
 where
   "P \<turnstile> C has F:T in D  \<equiv>
   \<exists>FDTs. P \<turnstile> C has_fields FDTs \<and> map_of FDTs (F,D) = Some T"
 
 lemma has_field_mono:
-  "\<lbrakk> P \<turnstile> C has F:T in D; P \<turnstile> C' \<preceq>\<^sup>* C \<rbrakk> \<Longrightarrow> P \<turnstile> C' has F:T in D"
+assumes has: " P \<turnstile> C has F:T in D" and sub: "P \<turnstile> C' \<preceq>\<^sup>* C"
+shows "P \<turnstile> C' has F:T in D"
 (*<*)
-apply(clarsimp simp:has_field_def)
-apply(drule (1) has_fields_mono_lem)
-apply(fastforce simp: map_add_def split:option.splits)
-done
+proof -
+  obtain FDTs where FDTs:"P \<turnstile> C has_fields FDTs" and "map_of FDTs (F, D) = \<lfloor>T\<rfloor>"
+    using has by(clarsimp simp: has_field_def)
+  also obtain pre where "P \<turnstile> C' has_fields pre @ FDTs"
+     and "dom (map_of pre) \<inter> dom (map_of FDTs) = {}"
+    using has_fields_mono_lem[OF sub FDTs] by clarify
+  ultimately show ?thesis by(fastforce simp: has_field_def map_add_def split:option.splits)
+qed
 (*>*)
 
 
 definition sees_field :: "'m prog \<Rightarrow> cname \<Rightarrow> vname \<Rightarrow> ty \<Rightarrow> cname \<Rightarrow> bool"
                   ("_ \<turnstile> _ sees _:_ in _" [51,51,51,51,51] 50)
 where
   "P \<turnstile> C sees F:T in D  \<equiv>
   \<exists>FDTs. P \<turnstile> C has_fields FDTs \<and>
             map_of (map (\<lambda>((F,D),T). (F,(D,T))) FDTs) F = Some(D,T)"
 
 lemma map_of_remap_SomeD:
   "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<Longrightarrow> map_of t (k, k') = Some x"
 (*<*)by (induct t) (auto simp:fun_upd_apply split: if_split_asm)(*>*)
 
 
 lemma has_visible_field:
   "P \<turnstile> C sees F:T in D \<Longrightarrow> P \<turnstile> C has F:T in D"
 (*<*)by(auto simp add:has_field_def sees_field_def map_of_remap_SomeD)(*>*)
 
 
 lemma sees_field_fun:
   "\<lbrakk>P \<turnstile> C sees F:T in D; P \<turnstile> C sees F:T' in D'\<rbrakk> \<Longrightarrow> T' = T \<and> D' = D"
 (*<*)by(fastforce simp:sees_field_def dest:has_fields_fun)(*>*)
 
 
 lemma sees_field_decl_above:
   "P \<turnstile> C sees F:T in D \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* D"
 (*<*)
-apply(auto simp:sees_field_def)
-apply(blast  intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
-done
+by(auto simp:sees_field_def
+        intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
 (*>*)
 
-(* FIXME ugly *)  
 lemma sees_field_idemp:
-  "P \<turnstile> C sees F:T in D \<Longrightarrow> P \<turnstile> D sees F:T in D"
+assumes sees: "P \<turnstile> C sees F:T in D"
+shows "P \<turnstile> D sees F:T in D"
 (*<*)
-  apply (unfold sees_field_def)
-  apply clarsimp
-  apply (rule_tac P = "map_of xs F = y" for xs y in mp)
-   prefer 2 
-   apply assumption 
-  apply (thin_tac "map_of xs F = y" for xs y)
-  apply (erule Fields.induct)
-   apply clarsimp
-   apply (frule map_of_SomeD)
-   apply clarsimp
-   apply (fastforce intro: has_fields_rec)
-  apply clarsimp
-  apply (frule map_of_SomeD)
-  apply clarsimp
-  apply (fastforce intro: has_fields_Object)
-  done
+proof -
+  obtain FDTs where C_flds: "P \<turnstile> C has_fields FDTs"
+     and FDTs: "map_of (map (\<lambda>((F, D), T). (F, D, T)) FDTs) F = \<lfloor>(D, T)\<rfloor>"
+     (is "?FDTs")
+   using sees by(clarsimp simp: sees_field_def)
+  have map: "\<And>C' fs. map_of (map ((\<lambda>((F, D), a). (F, D, a)) \<circ> (\<lambda>(F, y). ((F, C'), y))) fs) F 
+              = \<lfloor>(D, T)\<rfloor> \<Longrightarrow> C' = D \<and> (F, T) \<in> set fs"
+    by(frule map_of_SomeD) clarsimp
+  have "?FDTs \<longrightarrow> P \<turnstile> D sees F:T in D"
+  using C_flds proof induct
+    case NObj: has_fields_rec
+    then show ?case using map by (fastforce intro: has_fields_rec simp: sees_field_def)
+  next
+    case Obj: has_fields_Object
+    then show ?case using map by(fastforce intro: has_fields_Object simp: sees_field_def)
+  qed
+  then show ?thesis using FDTs by(rule mp)
+qed
 (*>*)
 
 subsection "Functional lookup"
 
 definition "method" :: "'m prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> cname \<times> ty list \<times> ty \<times> 'm"
 where
   "method P C M  \<equiv>  THE (D,Ts,T,m). P \<turnstile> C sees M:Ts \<rightarrow> T = m in D"
 
 definition field  :: "'m prog \<Rightarrow> cname \<Rightarrow> vname \<Rightarrow> cname \<times> ty"
 where
   "field P C F  \<equiv>  THE (D,T). P \<turnstile> C sees F:T in D"
                                                         
 definition fields :: "'m prog \<Rightarrow> cname \<Rightarrow> ((vname \<times> cname) \<times> ty) list" 
 where
   "fields P C  \<equiv>  THE FDTs. P \<turnstile> C has_fields FDTs"                
 
 lemma fields_def2 [simp]: "P \<turnstile> C has_fields FDTs \<Longrightarrow> fields P C = FDTs"
 (*<*)by (unfold fields_def) (auto dest: has_fields_fun)(*>*)
 
 lemma field_def2 [simp]: "P \<turnstile> C sees F:T in D \<Longrightarrow> field P C F = (D,T)"
 (*<*)by (unfold field_def) (auto dest: sees_field_fun)(*>*)
 
 lemma method_def2 [simp]: "P \<turnstile> C sees M: Ts\<rightarrow>T = m in D \<Longrightarrow> method P C M = (D,Ts,T,m)"
 (*<*)by (unfold method_def) (auto dest: sees_method_fun)(*>*)
 
 subsection "Code generator setup"
 
 code_pred 
   (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
   subcls1p 
 .
 declare subcls1_def [code_pred_def]
 
 code_pred 
   (modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool)
   [inductify]
   subcls1 
 .
 definition subcls' where "subcls' G = (subcls1p G)^**"
 code_pred
   (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
   [inductify]
   subcls'
 .
 
 lemma subcls_conv_subcls' [code_unfold]:
   "(subcls1 G)^* = {(C, D). subcls' G C D}"
   by (simp add: subcls'_def subcls1_def rtrancl_def)
 
 code_pred 
   (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
   widen 
 .
 
 code_pred 
   (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
   Fields
 .
 
 lemma has_field_code [code_pred_intro]:
   "\<lbrakk> P \<turnstile> C has_fields FDTs; map_of FDTs (F, D) = \<lfloor>T\<rfloor> \<rbrakk>
   \<Longrightarrow> P \<turnstile> C has F:T in D"
 by(auto simp add: has_field_def)
 
 code_pred 
   (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
   has_field
 by(auto simp add: has_field_def)
 
 lemma sees_field_code [code_pred_intro]:
   "\<lbrakk> P \<turnstile> C has_fields FDTs; map_of (map (\<lambda>((F, D), T). (F, D, T)) FDTs) F = \<lfloor>(D, T)\<rfloor> \<rbrakk>
   \<Longrightarrow> P \<turnstile> C sees F:T in D"
 by(auto simp add: sees_field_def)
 
 code_pred 
   (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> i \<Rightarrow> bool, 
           i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
   sees_field
 by(auto simp add: sees_field_def)
 
 code_pred
   (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool)
   Methods 
 .
 
 lemma Method_code [code_pred_intro]:
   "\<lbrakk> P \<turnstile> C sees_methods Mm; Mm M = \<lfloor>((Ts, T, m), D)\<rfloor> \<rbrakk>
   \<Longrightarrow> P \<turnstile> C sees M: Ts\<rightarrow>T = m in D"
 by(auto simp add: Method_def)
 
 code_pred
   (modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> bool,
           i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool)
   Method
 by(auto simp add: Method_def)
 
 lemma eval_Method_i_i_i_o_o_o_o_conv:
   "Predicate.eval (Method_i_i_i_o_o_o_o P C M) = (\<lambda>(Ts, T, m, D). P \<turnstile> C sees M:Ts\<rightarrow>T=m in D)"
 by(auto intro: Method_i_i_i_o_o_o_oI elim: Method_i_i_i_o_o_o_oE intro!: ext)
 
 lemma method_code [code]:
   "method P C M = 
   Predicate.the (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (\<lambda>(Ts, T, m, D). Predicate.single (D, Ts, T, m)))"
 apply (rule sym, rule the_eqI)
 apply (simp add: method_def eval_Method_i_i_i_o_o_o_o_conv)
 apply (rule arg_cong [where f=The])
 apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
 done
 
 lemma eval_Fields_conv:
   "Predicate.eval (Fields_i_i_o P C) = (\<lambda>FDTs. P \<turnstile> C has_fields FDTs)"
 by(auto intro: Fields_i_i_oI elim: Fields_i_i_oE intro!: ext)
 
 lemma fields_code [code]:
   "fields P C = Predicate.the (Fields_i_i_o P C)"
 by(simp add: fields_def Predicate.the_def eval_Fields_conv)
 
 lemma eval_sees_field_i_i_i_o_o_conv:
   "Predicate.eval (sees_field_i_i_i_o_o P C F) = (\<lambda>(T, D). P \<turnstile> C sees F:T in D)"
 by(auto intro!: ext intro: sees_field_i_i_i_o_oI elim: sees_field_i_i_i_o_oE)
 
 lemma eval_sees_field_i_i_i_o_i_conv:
   "Predicate.eval (sees_field_i_i_i_o_i P C F D) = (\<lambda>T. P \<turnstile> C sees F:T in D)"
 by(auto intro!: ext intro: sees_field_i_i_i_o_iI elim: sees_field_i_i_i_o_iE)
 
 lemma field_code [code]:
   "field P C F = Predicate.the (Predicate.bind (sees_field_i_i_i_o_o P C F) (\<lambda>(T, D). Predicate.single (D, T)))"
 apply (rule sym, rule the_eqI)
 apply (simp add: field_def eval_sees_field_i_i_i_o_o_conv)
 apply (rule arg_cong [where f=The])
 apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
 done
 
 (*<*)
 end
 (*>*)
diff --git a/thys/Jinja/Common/WellForm.thy b/thys/Jinja/Common/WellForm.thy
--- a/thys/Jinja/Common/WellForm.thy
+++ b/thys/Jinja/Common/WellForm.thy
@@ -1,434 +1,423 @@
 (*  Title:      Jinja/J/WellForm.thy
 
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Generic Well-formedness of programs\<close>
 
 theory WellForm imports TypeRel SystemClasses begin
 
 text \<open>\noindent This theory defines global well-formedness conditions
 for programs but does not look inside method bodies.  Hence it works
 for both Jinja and JVM programs. Well-typing of expressions is defined
 elsewhere (in theory \<open>WellType\<close>).
 
 Because Jinja does not have method overloading, its policy for method
 overriding is the classical one: \emph{covariant in the result type
 but contravariant in the argument types.} This means the result type
 of the overriding method becomes more specific, the argument types
 become more general.
 \<close>
 
 type_synonym 'm wf_mdecl_test = "'m prog \<Rightarrow> cname \<Rightarrow> 'm mdecl \<Rightarrow> bool"
 
 definition wf_fdecl :: "'m prog \<Rightarrow> fdecl \<Rightarrow> bool"
 where
   "wf_fdecl P \<equiv> \<lambda>(F,T). is_type P T"
 
 definition wf_mdecl :: "'m wf_mdecl_test \<Rightarrow> 'm wf_mdecl_test"
 where
   "wf_mdecl wf_md P C \<equiv> \<lambda>(M,Ts,T,mb).
   (\<forall>T\<in>set Ts. is_type P T) \<and> is_type P T \<and> wf_md P C (M,Ts,T,mb)"
 
 definition wf_cdecl :: "'m wf_mdecl_test \<Rightarrow> 'm prog \<Rightarrow> 'm cdecl \<Rightarrow> bool"
 where
   "wf_cdecl wf_md P  \<equiv>  \<lambda>(C,(D,fs,ms)).
   (\<forall>f\<in>set fs. wf_fdecl P f) \<and>  distinct_fst fs \<and>
   (\<forall>m\<in>set ms. wf_mdecl wf_md P C m) \<and>  distinct_fst ms \<and>
   (C \<noteq> Object \<longrightarrow>
    is_class P D \<and> \<not> P \<turnstile> D \<preceq>\<^sup>* C \<and>
    (\<forall>(M,Ts,T,m)\<in>set ms.
       \<forall>D' Ts' T' m'. P \<turnstile> D sees M:Ts' \<rightarrow> T' = m' in D' \<longrightarrow>
                        P \<turnstile> Ts' [\<le>] Ts \<and> P \<turnstile> T \<le> T'))"
 
 definition wf_syscls :: "'m prog \<Rightarrow> bool"
 where
   "wf_syscls P  \<equiv>  {Object} \<union> sys_xcpts \<subseteq> set(map fst P)"
 
 definition wf_prog :: "'m wf_mdecl_test \<Rightarrow> 'm prog \<Rightarrow> bool"
 where
   "wf_prog wf_md P  \<equiv>  wf_syscls P \<and> (\<forall>c \<in> set P. wf_cdecl wf_md P c) \<and> distinct_fst P"
 
 
 subsection\<open>Well-formedness lemmas\<close>
 
 lemma class_wf: 
   "\<lbrakk>class P C = Some c; wf_prog wf_md P\<rbrakk> \<Longrightarrow> wf_cdecl wf_md P (C,c)"
-(*<*)
-apply (unfold wf_prog_def class_def)
-apply (fast dest: map_of_SomeD)
-done
-(*>*)
+(*<*)by (unfold wf_prog_def class_def) (fast dest: map_of_SomeD)(*>*)
 
 
 lemma class_Object [simp]: 
   "wf_prog wf_md P \<Longrightarrow> \<exists>C fs ms. class P Object = Some (C,fs,ms)"
-(*<*)
-apply (unfold wf_prog_def wf_syscls_def class_def)
-apply (auto simp: map_of_SomeI)
-done
+(*<*)by (unfold wf_prog_def wf_syscls_def class_def)
+        (auto simp: map_of_SomeI)
 (*>*)
 
 
 lemma is_class_Object [simp]:
   "wf_prog wf_md P \<Longrightarrow> is_class P Object"
 (*<*)by (simp add: is_class_def)(*>*)
 (* Unused
 lemma is_class_supclass:
 assumes wf: "wf_prog wf_md P" and sub: "P \<turnstile> C \<preceq>\<^sup>* D"
 shows "is_class P C \<Longrightarrow> is_class P D"
-using sub apply(induct)
- apply assumption
-apply(fastforce simp:wf_cdecl_def subcls1_def is_class_def
-               dest:class_wf[OF _ wf])
-done
+(*<*)
+using sub proof(induct)
+  case step then show ?case
+    by(auto simp:wf_cdecl_def is_class_def dest!:class_wf[OF _ wf] subcls1D)
+qed simp
+(*>*)
 
 This is NOT true because P \<turnstile> NT \<le> Class C for any Class C
 lemma is_type_suptype: "\<lbrakk> wf_prog p P; is_type P T; P \<turnstile> T \<le> T' \<rbrakk>
  \<Longrightarrow> is_type P T'"
 *)
 
 lemma is_class_xcpt:
   "\<lbrakk> C \<in> sys_xcpts; wf_prog wf_md P \<rbrakk> \<Longrightarrow> is_class P C"
 (*<*)
-  apply (simp add: wf_prog_def wf_syscls_def is_class_def class_def)
-  apply (fastforce intro!: map_of_SomeI)
-  done
+by (fastforce intro!: map_of_SomeI
+              simp add: wf_prog_def wf_syscls_def is_class_def class_def)
 (*>*)
 
 
 lemma subcls1_wfD:
-  "\<lbrakk> P \<turnstile> C \<prec>\<^sup>1 D; wf_prog wf_md P \<rbrakk> \<Longrightarrow> D \<noteq> C \<and> (D,C) \<notin> (subcls1 P)\<^sup>+"
+assumes sub1: "P \<turnstile> C \<prec>\<^sup>1 D" and wf: "wf_prog wf_md P"
+shows "D \<noteq> C \<and> (D,C) \<notin> (subcls1 P)\<^sup>+"
 (*<*)
-apply( frule r_into_trancl)
-apply( drule subcls1D)
-apply(clarify)
-apply( drule (1) class_wf)
-apply( unfold wf_cdecl_def)
-apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
-done
+proof -
+  obtain fs ms where "C \<noteq> Object" and cls: "class P C = \<lfloor>(D, fs, ms)\<rfloor>"
+    using subcls1D[OF sub1] by clarify
+  then show ?thesis using wf class_wf[OF cls wf] r_into_trancl[OF sub1]
+    by(force simp add: wf_cdecl_def reflcl_trancl [THEN sym]
+             simp del: reflcl_trancl)
+qed
 (*>*)
 
 
 lemma wf_cdecl_supD: 
   "\<lbrakk>wf_cdecl wf_md P (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class P D"
 (*<*)by (auto simp: wf_cdecl_def)(*>*)
 
 
 lemma subcls_asym:
   "\<lbrakk> wf_prog wf_md P; (C,D) \<in> (subcls1 P)\<^sup>+ \<rbrakk> \<Longrightarrow> (D,C) \<notin> (subcls1 P)\<^sup>+"
-(*<*)
-apply(erule tranclE)
-apply(fast dest!: subcls1_wfD )
-apply(fast dest!: subcls1_wfD intro: trancl_trans)
-done
-(*>*)
+(*<*)by(erule tranclE; fast dest!: subcls1_wfD intro: trancl_trans)(*>*)
 
 
 lemma subcls_irrefl:
   "\<lbrakk> wf_prog wf_md P; (C,D) \<in> (subcls1 P)\<^sup>+ \<rbrakk> \<Longrightarrow> C \<noteq> D"
-(*<*)
-apply (erule trancl_trans_induct)
-apply  (auto dest: subcls1_wfD subcls_asym)
-done
-(*>*)
+(*<*)by (erule trancl_trans_induct) (auto dest: subcls1_wfD subcls_asym)(*>*)
 
 
 lemma acyclic_subcls1:
   "wf_prog wf_md P \<Longrightarrow> acyclic (subcls1 P)"
-(*<*)
-apply (unfold acyclic_def)
-apply (fast dest: subcls_irrefl)
-done
-(*>*)
+(*<*)by (unfold acyclic_def) (fast dest: subcls_irrefl)(*>*)
 
 
 lemma wf_subcls1:
   "wf_prog wf_md P \<Longrightarrow> wf ((subcls1 P)\<inverse>)"
 (*<*)
-apply (rule finite_acyclic_wf)
-apply ( subst finite_converse)
-apply ( rule finite_subcls1)
-apply (subst acyclic_converse)
-apply (erule acyclic_subcls1)
-done
+proof -
+  assume wf: "wf_prog wf_md P"
+  have "finite (subcls1 P)" by(rule finite_subcls1)
+  then have fin': "finite ((subcls1 P)\<inverse>)" by(subst finite_converse)
+
+  from wf have "acyclic (subcls1 P)" by(rule acyclic_subcls1)
+  then have acyc': "acyclic ((subcls1 P)\<inverse>)" by (subst acyclic_converse)
+
+  from fin' acyc' show ?thesis by (rule finite_acyclic_wf)
+qed
 (*>*)
 
 
 lemma single_valued_subcls1:
   "wf_prog wf_md G \<Longrightarrow> single_valued (subcls1 G)"
 (*<*)
 by(auto simp:wf_prog_def distinct_fst_def single_valued_def dest!:subcls1D)
 (*>*)
 
 
 lemma subcls_induct: 
   "\<lbrakk> wf_prog wf_md P; \<And>C. \<forall>D. (C,D) \<in> (subcls1 P)\<^sup>+ \<longrightarrow> Q D \<Longrightarrow> Q C \<rbrakk> \<Longrightarrow> Q C"
 (*<*)
   (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
-  assume ?A thus ?thesis apply -
-apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
-apply(rule p)
-apply(auto)
-done
+  assume ?A then have wf: "wf_prog wf_md P" by assumption
+  have wf':"wf (((subcls1 P)\<^sup>+)\<inverse>)" using wf_trancl[OF wf_subcls1[OF wf]]
+    by(simp only: trancl_converse)
+  show ?thesis using wf_induct[where a = C and P = Q, OF wf' p] by simp
 qed
 (*>*)
 
 
 lemma subcls1_induct_aux:
-  "\<lbrakk> is_class P C; wf_prog wf_md P; Q Object;
-    \<And>C D fs ms.
+assumes "is_class P C" and wf: "wf_prog wf_md P" and QObj: "Q Object"
+shows
+ "\<lbrakk> \<And>C D fs ms.
     \<lbrakk> C \<noteq> Object; is_class P C; class P C = Some (D,fs,ms) \<and>
       wf_cdecl wf_md P (C,D,fs,ms) \<and> P \<turnstile> C \<prec>\<^sup>1 D \<and> is_class P D \<and> Q D\<rbrakk> \<Longrightarrow> Q C \<rbrakk>
   \<Longrightarrow> Q C"
 (*<*)
-  (is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
+  (is "PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
-  assume ?A ?B ?C thus ?thesis apply -
-apply(unfold is_class_def)
-apply( rule impE)
-prefer 2
-apply(   assumption)
-prefer 2
-apply(  assumption)
-apply( erule thin_rl)
-apply( rule subcls_induct)
-apply(  assumption)
-apply( rule impI)
-apply( case_tac "C = Object")
-apply(  fast)
-apply safe
-apply( frule (1) class_wf)
-apply( frule (1) wf_cdecl_supD)
-
-apply( subgoal_tac "P \<turnstile> C \<prec>\<^sup>1 a")
-apply( erule_tac [2] subcls1I)
-apply(  rule p)
-apply (unfold is_class_def)
-apply auto
-done
+  have "class P C \<noteq> None \<longrightarrow> Q C"
+  proof(induct rule: subcls_induct[OF wf])
+    case (1 C)
+    have "class P C \<noteq> None \<Longrightarrow> Q C"
+    proof(cases "C = Object")
+      case True
+      then show ?thesis using QObj by fast
+    next
+      case False
+      assume nNone: "class P C \<noteq> None"
+      then have is_cls: "is_class P C" by(simp add: is_class_def)
+      obtain D fs ms where cls: "class P C = \<lfloor>(D, fs, ms)\<rfloor>" using nNone by safe
+      also have wfC: "wf_cdecl wf_md P (C, D, fs, ms)" by(rule class_wf[OF cls wf])
+      moreover have D: "is_class P D" by(rule wf_cdecl_supD[OF wfC False])
+      moreover have "P \<turnstile> C \<prec>\<^sup>1 D" by(rule subcls1I[OF cls False])
+      moreover have "class P D \<noteq> None" using D by(simp add: is_class_def)
+      ultimately show ?thesis using 1 by (auto intro: p[OF False is_cls])
+    qed
+  then show "class P C \<noteq> None \<longrightarrow> Q C" by simp
+  qed
+  thus ?thesis using assms by(unfold is_class_def) simp
 qed
 (*>*)
 
 (* FIXME can't we prove this one directly?? *)
 lemma subcls1_induct [consumes 2, case_names Object Subcls]:
   "\<lbrakk> wf_prog wf_md P; is_class P C; Q Object;
     \<And>C D. \<lbrakk>C \<noteq> Object; P \<turnstile> C \<prec>\<^sup>1 D; is_class P D; Q D\<rbrakk> \<Longrightarrow> Q C \<rbrakk>
   \<Longrightarrow> Q C"
-(*<*)
-  apply (erule subcls1_induct_aux, assumption, assumption)
-  apply blast
-  done
-(*>*)
+(*<*)by (erule (2) subcls1_induct_aux) blast(*>*)
 
 
 lemma subcls_C_Object:
-  "\<lbrakk> is_class P C; wf_prog wf_md P \<rbrakk> \<Longrightarrow> P \<turnstile> C \<preceq>\<^sup>* Object"
+assumes "class": "is_class P C" and wf: "wf_prog wf_md P"
+shows "P \<turnstile> C \<preceq>\<^sup>* Object"
 (*<*)
-apply(erule (1) subcls1_induct)
- apply( fast)
-apply(erule (1) converse_rtrancl_into_rtrancl)
-done
+using wf "class"
+proof(induct rule: subcls1_induct)
+  case Subcls
+  then show ?case by(simp add: converse_rtrancl_into_rtrancl)
+qed fast
 (*>*)
 
 
 lemma is_type_pTs:
 assumes "wf_prog wf_md P" and "(C,S,fs,ms) \<in> set P" and "(M,Ts,T,m) \<in> set ms"
 shows "set Ts \<subseteq> types P"
 (*<*)
 proof
   from assms have "wf_mdecl wf_md P C (M,Ts,T,m)" 
     by (unfold wf_prog_def wf_cdecl_def) auto  
   hence "\<forall>t \<in> set Ts. is_type P t" by (unfold wf_mdecl_def) auto
   moreover fix t assume "t \<in> set Ts"
   ultimately have "is_type P t" by blast
   thus "t \<in> types P" ..
 qed
 (*>*)
 
 
 subsection\<open>Well-formedness and method lookup\<close>
 
 lemma sees_wf_mdecl:
-  "\<lbrakk> wf_prog wf_md P; P \<turnstile> C sees M:Ts\<rightarrow>T = m in D \<rbrakk> \<Longrightarrow> wf_mdecl wf_md P D (M,Ts,T,m)"
+assumes wf: "wf_prog wf_md P" and sees: "P \<turnstile> C sees M:Ts\<rightarrow>T = m in D"
+shows "wf_mdecl wf_md P D (M,Ts,T,m)"
 (*<*)
-apply(drule visible_method_exists)
-apply(fastforce simp:wf_cdecl_def dest!:class_wf dest:map_of_SomeD)
-done
+using wf visible_method_exists[OF sees]
+by(fastforce simp:wf_cdecl_def dest!:class_wf dest:map_of_SomeD)
 (*>*)
 
 
 lemma sees_method_mono [rule_format (no_asm)]: 
-  "\<lbrakk> P \<turnstile> C' \<preceq>\<^sup>* C; wf_prog wf_md P \<rbrakk> \<Longrightarrow>
-  \<forall>D Ts T m. P \<turnstile> C sees M:Ts\<rightarrow>T = m in D \<longrightarrow>
+assumes sub: "P \<turnstile> C' \<preceq>\<^sup>* C" and wf: "wf_prog wf_md P"
+shows "\<forall>D Ts T m. P \<turnstile> C sees M:Ts\<rightarrow>T = m in D \<longrightarrow>
      (\<exists>D' Ts' T' m'. P \<turnstile> C' sees M:Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T)"
 (*<*)
-apply( drule rtranclD)
-apply( erule disjE)
-apply(  fastforce)
-apply( erule conjE)
-apply( erule trancl_trans_induct)
-prefer 2
-apply(  clarify)
-apply(  drule spec, drule spec, drule spec, drule spec, erule (1) impE)
-apply clarify
-apply(  fast elim: widen_trans widens_trans)
-apply( clarify)
-apply( drule subcls1D)
-apply( clarify)
-apply(clarsimp simp:Method_def)
-apply(frule (2) sees_methods_rec)
-apply(rule refl)
-apply(case_tac "map_of ms M")
-apply(rule_tac x = D in exI)
-apply(rule_tac x = Ts in exI)
-apply(rule_tac x = T in exI)
-apply simp
-apply(rule_tac x = m in exI)
-apply(fastforce simp add:map_add_def split:option.split)
-apply clarsimp
-apply(rename_tac Ts' T' m')
-apply( drule (1) class_wf)
-apply( unfold wf_cdecl_def Method_def)
-apply( frule map_of_SomeD)
-apply auto
-apply(drule (1) bspec, simp)
-apply(erule_tac x=D in allE, erule_tac x=Ts in allE, erule_tac x=T in allE)
-apply(fastforce simp:map_add_def split:option.split)
-done
+  (is "\<forall>D Ts T m. ?P C D Ts T m \<longrightarrow> ?Q C' D Ts T m")
+proof(rule disjE[OF rtranclD[OF sub]])
+  assume "C' = C"
+  then show ?thesis using assms by fastforce
+next
+  assume "C' \<noteq> C \<and> (C', C) \<in> (subcls1 P)\<^sup>+"
+  then have neq: "C' \<noteq> C" and subcls1: "(C', C) \<in> (subcls1 P)\<^sup>+" by simp+
+  show ?thesis proof(induct rule: trancl_trans_induct[OF subcls1])
+    case (2 x y z)
+    then have zy: "\<And>D Ts T m. ?P z D Ts T m \<Longrightarrow> ?Q y D Ts T m" by blast
+    have "\<And>D Ts T m. ?P z D Ts T m \<Longrightarrow> ?Q x D Ts T m"
+    proof -
+      fix D Ts T m assume P: "?P z D Ts T m"
+      then show "?Q x D Ts T m" using zy[OF P] 2(2)
+        by(fast elim: widen_trans widens_trans)
+    qed
+    then show ?case by blast
+  next
+    case (1 x y)
+    have "\<And>D Ts T m. ?P y D Ts T m \<Longrightarrow> ?Q x D Ts T m"
+    proof -
+      fix D Ts T m assume P: "?P y D Ts T m"
+      then obtain Mm where sees: "P \<turnstile> y sees_methods Mm" and
+                           M: "Mm M = \<lfloor>((Ts, T, m), D)\<rfloor>"
+        by(clarsimp simp:Method_def)
+      obtain fs ms where nObj: "x \<noteq> Object" and
+                         cls: "class P x = \<lfloor>(y, fs, ms)\<rfloor>"
+        using subcls1D[OF 1] by clarsimp
+      have x_meth: "P \<turnstile> x sees_methods Mm ++ (map_option (\<lambda>m. (m, x)) \<circ> map_of ms)"
+        using sees_methods_rec[OF cls nObj sees] by simp
+      show "?Q x D Ts T m" proof(cases "map_of ms M")
+        case None
+        then have "\<exists>m'. P \<turnstile> x sees M :  Ts\<rightarrow>T = m' in D" using M x_meth
+          by(fastforce simp add:Method_def map_add_def split:option.split)
+        then show ?thesis by auto
+      next
+        case (Some a)
+        then obtain Ts' T' m' where a: "a = (Ts',T',m')" by(cases a)
+        then have "(\<exists>m' Mm. P \<turnstile> y sees_methods Mm \<and> Mm M = \<lfloor>((Ts, T, m'), D)\<rfloor>)
+              \<longrightarrow> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T"
+          using nObj class_wf[OF cls wf] map_of_SomeD[OF Some]
+          by(clarsimp simp: wf_cdecl_def Method_def) fast
+        then show ?thesis using Some a sees M x_meth
+          by(fastforce simp:Method_def map_add_def split:option.split)
+      qed
+    qed
+    then show ?case by simp
+  qed
+qed
 (*>*)
 
 
 lemma sees_method_mono2:
   "\<lbrakk> P \<turnstile> C' \<preceq>\<^sup>* C; wf_prog wf_md P;
      P \<turnstile> C sees M:Ts\<rightarrow>T = m in D; P \<turnstile> C' sees M:Ts'\<rightarrow>T' = m' in D' \<rbrakk>
   \<Longrightarrow> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T"
 (*<*)by(blast dest:sees_method_mono sees_method_fun)(*>*)
 
 
 lemma mdecls_visible:
 assumes wf: "wf_prog wf_md P" and "class": "is_class P C"
 shows "\<And>D fs ms. class P C = Some(D,fs,ms)
          \<Longrightarrow> \<exists>Mm. P \<turnstile> C sees_methods Mm \<and> (\<forall>(M,Ts,T,m) \<in> set ms. Mm M = Some((Ts,T,m),C))"
 (*<*)
 using wf "class"
 proof (induct rule:subcls1_induct)
   case Object
   with wf have "distinct_fst ms"
     by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
   with Object show ?case by(fastforce intro!: sees_methods_Object map_of_SomeI)
 next
   case Subcls
   with wf have "distinct_fst ms"
     by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
   with Subcls show ?case
     by(fastforce elim:sees_methods_rec dest:subcls1D map_of_SomeI
                 simp:is_class_def)
 qed
 (*>*)
 
 
 lemma mdecl_visible:
 assumes wf: "wf_prog wf_md P" and C: "(C,S,fs,ms) \<in> set P" and  m: "(M,Ts,T,m) \<in> set ms"
 shows "P \<turnstile> C sees M:Ts\<rightarrow>T = m in C"
 (*<*)
 proof -
   from wf C have "class": "class P C = Some (S,fs,ms)"
     by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
   from "class" have "is_class P C" by(auto simp:is_class_def)                   
   with assms "class" show ?thesis
     by(bestsimp simp:Method_def dest:mdecls_visible)
 qed
 (*>*)
 
 
 lemma Call_lemma:
-  "\<lbrakk> P \<turnstile> C sees M:Ts\<rightarrow>T = m in D; P \<turnstile> C' \<preceq>\<^sup>* C; wf_prog wf_md P \<rbrakk>
-  \<Longrightarrow> \<exists>D' Ts' T' m'.
+assumes sees: "P \<turnstile> C sees M:Ts\<rightarrow>T = m in D" and sub: "P \<turnstile> C' \<preceq>\<^sup>* C" and wf: "wf_prog wf_md P"
+shows "\<exists>D' Ts' T' m'.
        P \<turnstile> C' sees M:Ts'\<rightarrow>T' = m' in D' \<and> P \<turnstile> Ts [\<le>] Ts' \<and> P \<turnstile> T' \<le> T \<and> P \<turnstile> C' \<preceq>\<^sup>* D'
        \<and> is_type P T' \<and> (\<forall>T\<in>set Ts'. is_type P T) \<and> wf_md P D' (M,Ts',T',m')"
 (*<*)
-apply(frule (2) sees_method_mono)
-apply(fastforce intro:sees_method_decl_above dest:sees_wf_mdecl
-               simp: wf_mdecl_def)
-done
+using assms sees_method_mono[OF sub wf sees]
+by(fastforce intro:sees_method_decl_above dest:sees_wf_mdecl
+             simp: wf_mdecl_def)
 (*>*)
 
 
 lemma wf_prog_lift:
   assumes wf: "wf_prog (\<lambda>P C bd. A P C bd) P"
   and rule:
   "\<And>wf_md C M Ts C T m bd.
    wf_prog wf_md P \<Longrightarrow>
    P \<turnstile> C sees M:Ts\<rightarrow>T = m in C \<Longrightarrow>   
    set Ts \<subseteq>  types P \<Longrightarrow>
    bd = (M,Ts,T,m) \<Longrightarrow>
    A P C bd \<Longrightarrow>
    B P C bd"
   shows "wf_prog (\<lambda>P C bd. B P C bd) P"
 (*<*)
 proof -
-  from wf show ?thesis
-    apply (unfold wf_prog_def wf_cdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply (unfold wf_mdecl_def)
-    apply clarsimp
-    apply (drule bspec, assumption)
-    apply clarsimp
-    apply (frule mdecl_visible [OF wf], assumption+)
-    apply (frule is_type_pTs [OF wf], assumption+)
-    apply (drule rule [OF wf], assumption+)
-    apply auto
-    done
+  have "\<And>c. c\<in>set P \<Longrightarrow> wf_cdecl A P c \<Longrightarrow> wf_cdecl B P c"
+  proof -
+    fix c assume "c\<in>set P" and "wf_cdecl A P c"
+    then show "wf_cdecl B P c"
+     using rule[OF wf mdecl_visible[OF wf] is_type_pTs[OF wf]]
+     by (auto simp: wf_cdecl_def wf_mdecl_def)
+  qed
+  then show ?thesis using wf by (clarsimp simp: wf_prog_def)
 qed
 (*>*)
 
 
 subsection\<open>Well-formedness and field lookup\<close>
 
 lemma wf_Fields_Ex:
-  "\<lbrakk> wf_prog wf_md P; is_class P C \<rbrakk> \<Longrightarrow> \<exists>FDTs. P \<turnstile> C has_fields FDTs"
+assumes wf: "wf_prog wf_md P" and "is_class P C"
+shows "\<exists>FDTs. P \<turnstile> C has_fields FDTs"
 (*<*)
-apply(frule class_Object)
-apply(erule (1) subcls1_induct)
- apply(blast intro:has_fields_Object)
-apply(blast intro:has_fields_rec dest:subcls1D)
-done
+using assms proof(induct rule:subcls1_induct)
+  case Object
+  then show ?case using class_Object[OF wf]
+    by(blast intro:has_fields_Object)
+next
+  case Subcls
+  then show ?case by(blast intro:has_fields_rec dest:subcls1D)
+qed
 (*>*)
 
 
 lemma has_fields_types:
   "\<lbrakk> P \<turnstile> C has_fields FDTs; (FD,T) \<in> set FDTs; wf_prog wf_md P \<rbrakk> \<Longrightarrow> is_type P T"
 (*<*)
-apply(induct rule:Fields.induct)
- apply(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
-apply(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
-done
+proof(induct rule:Fields.induct)
+qed(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)+
 (*>*)
 
 
 lemma sees_field_is_type:
   "\<lbrakk> P \<turnstile> C sees F:T in D; wf_prog wf_md P \<rbrakk> \<Longrightarrow> is_type P T"
 (*<*)
 by(fastforce simp: sees_field_def
             elim: has_fields_types map_of_SomeD[OF map_of_remap_SomeD])
 (*>*)
 
 lemma wf_syscls:
   "set SystemClasses \<subseteq> set P \<Longrightarrow> wf_syscls P"
 (*<*)
-apply (simp add: image_def SystemClasses_def wf_syscls_def sys_xcpts_def
+by (force simp add: image_def SystemClasses_def wf_syscls_def sys_xcpts_def
                  ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
- apply force
-done
 (*>*)
 
 end
diff --git a/thys/Jinja/JVM/JVMDefensive.thy b/thys/Jinja/JVM/JVMDefensive.thy
--- a/thys/Jinja/JVM/JVMDefensive.thy
+++ b/thys/Jinja/JVM/JVMDefensive.thy
@@ -1,190 +1,196 @@
 (*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
     Author:     Gerwin Klein
     Copyright   GPL
 *)
 
 section \<open>A Defensive JVM\<close>
 
 theory JVMDefensive
 imports JVMExec "../Common/Conform"
 begin
 
 text \<open>
   Extend the state space by one element indicating a type error (or
   other abnormal termination)\<close>
 datatype 'a type_error = TypeError | Normal 'a
 
 fun is_Addr :: "val \<Rightarrow> bool" where
   "is_Addr (Addr a) \<longleftrightarrow> True"
 | "is_Addr v \<longleftrightarrow> False"
 
 fun is_Intg :: "val \<Rightarrow> bool" where
   "is_Intg (Intg i) \<longleftrightarrow> True"
 | "is_Intg v \<longleftrightarrow> False"
 
 fun is_Bool :: "val \<Rightarrow> bool" where
   "is_Bool (Bool b) \<longleftrightarrow> True"
 | "is_Bool v \<longleftrightarrow> False"
 
 definition is_Ref :: "val \<Rightarrow> bool" where
   "is_Ref v \<longleftrightarrow> v = Null \<or> is_Addr v"
 
 primrec check_instr :: "[instr, jvm_prog, heap, val list, val list, 
                   cname, mname, pc, frame list] \<Rightarrow> bool" where
   check_instr_Load:
     "check_instr (Load n) P h stk loc C M\<^sub>0 pc frs = 
     (n < length loc)"
 
 | check_instr_Store:
     "check_instr (Store n) P h stk loc C\<^sub>0 M\<^sub>0 pc frs = 
     (0 < length stk \<and> n < length loc)"
 
 | check_instr_Push:
     "check_instr (Push v) P h stk loc C\<^sub>0 M\<^sub>0 pc frs = 
     (\<not>is_Addr v)"
 
 | check_instr_New:
     "check_instr (New C) P h stk loc C\<^sub>0 M\<^sub>0 pc frs = 
     is_class P C"
 
 | check_instr_Getfield:
     "check_instr (Getfield F C) P h stk loc C\<^sub>0 M\<^sub>0 pc frs = 
     (0 < length stk \<and> (\<exists>C' T. P \<turnstile> C sees F:T in C') \<and> 
     (let (C', T) = field P C F; ref = hd stk in 
       C' = C \<and> is_Ref ref \<and> (ref \<noteq> Null \<longrightarrow> 
         h (the_Addr ref) \<noteq> None \<and> 
         (let (D,vs) = the (h (the_Addr ref)) in 
           P \<turnstile> D \<preceq>\<^sup>* C \<and> vs (F,C) \<noteq> None \<and> P,h \<turnstile> the (vs (F,C)) :\<le> T))))" 
 
 | check_instr_Putfield:
     "check_instr (Putfield F C) P h stk loc C\<^sub>0 M\<^sub>0 pc frs = 
     (1 < length stk \<and> (\<exists>C' T. P \<turnstile> C sees F:T in C') \<and>
     (let (C', T) = field P C F; v = hd stk; ref = hd (tl stk) in 
       C' = C \<and> is_Ref ref \<and> (ref \<noteq> Null \<longrightarrow> 
         h (the_Addr ref) \<noteq> None \<and> 
         (let D = fst (the (h (the_Addr ref))) in 
           P \<turnstile> D \<preceq>\<^sup>* C \<and> P,h \<turnstile> v :\<le> T))))" 
 
 | check_instr_Checkcast:
     "check_instr (Checkcast C) P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (0 < length stk \<and> is_class P C \<and> is_Ref (hd stk))"
 
 | check_instr_Invoke:
     "check_instr (Invoke M n) P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (n < length stk \<and> is_Ref (stk!n) \<and>  
     (stk!n \<noteq> Null \<longrightarrow> 
       (let a = the_Addr (stk!n); 
            C = cname_of h a;
            Ts = fst (snd (method P C M))
       in h a \<noteq> None \<and> P \<turnstile> C has M \<and> 
          P,h \<turnstile> rev (take n stk) [:\<le>] Ts)))"
  
 | check_instr_Return:
     "check_instr Return P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (0 < length stk \<and> ((0 < length frs) \<longrightarrow> 
       (P \<turnstile> C\<^sub>0 has M\<^sub>0) \<and>    
       (let v = hd stk; 
            T = fst (snd (snd (method P C\<^sub>0 M\<^sub>0)))
        in P,h \<turnstile> v :\<le> T)))"
  
 | check_instr_Pop:
     "check_instr Pop P h stk loc C\<^sub>0 M\<^sub>0 pc frs = 
     (0 < length stk)"
 
 | check_instr_IAdd:
     "check_instr IAdd P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (1 < length stk \<and> is_Intg (hd stk) \<and> is_Intg (hd (tl stk)))"
 
 | check_instr_IfFalse:
     "check_instr (IfFalse b) P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (0 < length stk \<and> is_Bool (hd stk) \<and> 0 \<le> int pc+b)"
 
 | check_instr_CmpEq:
     "check_instr CmpEq P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (1 < length stk)"
 
 | check_instr_Goto:
     "check_instr (Goto b) P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (0 \<le> int pc+b)"
 
 | check_instr_Throw:
     "check_instr Throw P h stk loc C\<^sub>0 M\<^sub>0 pc frs =
     (0 < length stk \<and> is_Ref (hd stk))"
 
 definition check :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> bool" where
   "check P \<sigma> = (let (xcpt, h, frs) = \<sigma> in
                (case frs of [] \<Rightarrow> True | (stk,loc,C,M,pc)#frs' \<Rightarrow> 
                 P \<turnstile> C has M \<and>
                 (let (C',Ts,T,mxs,mxl\<^sub>0,ins,xt) = method P C M; i = ins!pc in
                  pc < size ins \<and> size stk \<le> mxs \<and>
                  check_instr i P h stk loc C M pc frs')))"
 
 
 definition exec_d :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> jvm_state option type_error" where
   "exec_d P \<sigma> = (if check P \<sigma> then Normal (exec (P, \<sigma>)) else TypeError)"
 
 
 inductive_set
   exec_1_d :: "jvm_prog \<Rightarrow> (jvm_state type_error \<times> jvm_state type_error) set" 
   and exec_1_d' :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
                    ("_ \<turnstile> _ -jvmd\<rightarrow>\<^sub>1 _" [61,61,61]60)
   for P :: jvm_prog
 where
   "P \<turnstile> \<sigma> -jvmd\<rightarrow>\<^sub>1 \<sigma>' \<equiv> (\<sigma>,\<sigma>') \<in> exec_1_d P"
 | exec_1_d_ErrorI: "exec_d P \<sigma> = TypeError \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow>\<^sub>1 TypeError"
 | exec_1_d_NormalI: "exec_d P \<sigma> = Normal (Some \<sigma>') \<Longrightarrow> P \<turnstile> Normal \<sigma> -jvmd\<rightarrow>\<^sub>1 Normal \<sigma>'"
 
 \<comment> \<open>reflexive transitive closure:\<close>
 definition exec_all_d :: "jvm_prog \<Rightarrow> jvm_state type_error \<Rightarrow> jvm_state type_error \<Rightarrow> bool" 
     ("_ \<turnstile> _ -jvmd\<rightarrow> _" [61,61,61]60) where
   exec_all_d_def1: "P \<turnstile> \<sigma> -jvmd\<rightarrow> \<sigma>' \<longleftrightarrow> (\<sigma>,\<sigma>') \<in> (exec_1_d P)\<^sup>*"
 
 notation (ASCII)
   "exec_all_d"  ("_ |- _ -jvmd-> _" [61,61,61]60)
 
 lemma exec_1_d_eq:
   "exec_1_d P = {(s,t). \<exists>\<sigma>. s = Normal \<sigma> \<and> t = TypeError \<and> exec_d P \<sigma> = TypeError} \<union> 
                 {(s,t). \<exists>\<sigma> \<sigma>'. s = Normal \<sigma> \<and> t = Normal \<sigma>' \<and> exec_d P \<sigma> = Normal (Some \<sigma>')}"
 by (auto elim!: exec_1_d.cases intro!: exec_1_d.intros)
 
 
 declare split_paired_All [simp del]
 declare split_paired_Ex [simp del]
 
 lemma if_neq [dest!]:
   "(if P then A else B) \<noteq> B \<Longrightarrow> P"
   by (cases P, auto)
 
 lemma exec_d_no_errorI [intro]:
   "check P \<sigma> \<Longrightarrow> exec_d P \<sigma> \<noteq> TypeError"
   by (unfold exec_d_def) simp
 
 theorem no_type_error_commutes:
   "exec_d P \<sigma> \<noteq> TypeError \<Longrightarrow> exec_d P \<sigma> = Normal (exec (P, \<sigma>))"
   by (unfold exec_d_def, auto)
 
 
 lemma defensive_imp_aggressive:
   "P \<turnstile> (Normal \<sigma>) -jvmd\<rightarrow> (Normal \<sigma>') \<Longrightarrow> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'"
 (*<*)
 proof -
   have "\<And>x y. P \<turnstile> x -jvmd\<rightarrow> y \<Longrightarrow> \<forall>\<sigma> \<sigma>'. x = Normal \<sigma> \<longrightarrow> y = Normal \<sigma>' \<longrightarrow>  P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'"
-    apply (unfold exec_all_d_def1)
-    apply (erule rtrancl_induct)
-     apply (simp add: exec_all_def)
-    apply (fold exec_all_d_def1)
-    apply simp
-    apply (intro allI impI)
-    apply (erule exec_1_d.cases, simp)
-    apply (simp add: exec_all_def exec_d_def split: type_error.splits if_split_asm)
-    apply (rule rtrancl_trans, assumption)
-    apply blast
-    done
+  proof -
+    fix x y assume xy: "P \<turnstile> x -jvmd\<rightarrow> y"
+    then have "(x, y) \<in> (exec_1_d P)\<^sup>*" by (unfold exec_all_d_def1)
+    then show "\<forall>\<sigma> \<sigma>'. x = Normal \<sigma> \<longrightarrow> y = Normal \<sigma>' \<longrightarrow>  P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'"
+    proof(induct rule: rtrancl_induct)
+      case base
+      then show ?case by (simp add: exec_all_def)
+    next
+      case (step y' z')
+      show ?case proof(induct rule: exec_1_d.cases[OF step.hyps(2)])
+        case (2 \<sigma> \<sigma>')
+        then have "(\<sigma>, \<sigma>') \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*" using step
+          by(fastforce simp: exec_d_def split: type_error.splits if_split_asm)
+        then show ?case using step 2 by (auto simp: exec_all_def)
+      qed simp
+    qed
+  qed
   moreover
   assume "P \<turnstile> (Normal \<sigma>) -jvmd\<rightarrow> (Normal \<sigma>')" 
   ultimately
   show "P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'" by blast
 qed
 (*>*)
 
 end
diff --git a/thys/Jinja/JVM/JVMExec.thy b/thys/Jinja/JVM/JVMExec.thy
--- a/thys/Jinja/JVM/JVMExec.thy
+++ b/thys/Jinja/JVM/JVMExec.thy
@@ -1,111 +1,114 @@
 (*  Title:      HOL/MicroJava/JVM/JVMExec.thy
     Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 section \<open>Program Execution in the JVM\<close>
 
 theory JVMExec
 imports JVMExecInstr JVMExceptions
 begin
 
 abbreviation
   instrs_of :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> instr list" where
   "instrs_of P C M == fst(snd(snd(snd(snd(snd(method P C M))))))"
 
 fun exec :: "jvm_prog \<times> jvm_state => jvm_state option" where \<comment> \<open>single step execution\<close>
   "exec (P, xp, h, []) = None"
 
 | "exec (P, None, h, (stk,loc,C,M,pc)#frs) =
   (let 
      i = instrs_of P C M ! pc;
      (xcpt', h', frs') = exec_instr i P h stk loc C M pc frs
    in Some(case xcpt' of
              None \<Rightarrow> (None,h',frs')
            | Some a \<Rightarrow> find_handler P a h ((stk,loc,C,M,pc)#frs)))"
 
 | "exec (P, Some xa, h, frs) = None" 
 
 \<comment> \<open>relational view\<close>
 inductive_set
   exec_1 :: "jvm_prog \<Rightarrow> (jvm_state \<times> jvm_state) set"
   and exec_1' :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> jvm_state \<Rightarrow> bool" 
     ("_ \<turnstile>/ _ -jvm\<rightarrow>\<^sub>1/ _" [61,61,61] 60)
   for P :: jvm_prog
 where
   "P \<turnstile> \<sigma> -jvm\<rightarrow>\<^sub>1 \<sigma>' \<equiv> (\<sigma>,\<sigma>') \<in> exec_1 P"
 | exec_1I: "exec (P,\<sigma>) = Some \<sigma>' \<Longrightarrow> P \<turnstile> \<sigma> -jvm\<rightarrow>\<^sub>1 \<sigma>'"
 
 \<comment> \<open>reflexive transitive closure:\<close>
 definition exec_all :: "jvm_prog \<Rightarrow> jvm_state \<Rightarrow> jvm_state \<Rightarrow> bool"
     ("(_ \<turnstile>/ _ -jvm\<rightarrow>/ _)" [61,61,61]60) where
 (* FIXME exec_all \<rightarrow> exec_star, also in Def.JVM *)
   exec_all_def1: "P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>' \<longleftrightarrow> (\<sigma>,\<sigma>') \<in> (exec_1 P)\<^sup>*"
 
 notation (ASCII)
   exec_all  ("_ |-/ _ -jvm->/ _" [61,61,61]60)
 
 
 lemma exec_1_eq:
   "exec_1 P = {(\<sigma>,\<sigma>'). exec (P,\<sigma>) = Some \<sigma>'}"
 (*<*)by (auto intro: exec_1I elim: exec_1.cases)(*>*)
 
 lemma exec_1_iff:
   "P \<turnstile> \<sigma> -jvm\<rightarrow>\<^sub>1 \<sigma>' = (exec (P,\<sigma>) = Some \<sigma>')"
 (*<*)by (simp add: exec_1_eq)(*>*)
 
 lemma exec_all_def:
   "P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>' = ((\<sigma>,\<sigma>') \<in> {(\<sigma>,\<sigma>'). exec (P,\<sigma>) = Some \<sigma>'}\<^sup>*)"
 (*<*)by (simp add: exec_all_def1 exec_1_eq)(*>*)
 
 lemma jvm_refl[iff]: "P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>"
 (*<*)by(simp add: exec_all_def)(*>*)
 
 lemma jvm_trans[trans]:
  "\<lbrakk> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'; P \<turnstile> \<sigma>' -jvm\<rightarrow> \<sigma>'' \<rbrakk> \<Longrightarrow> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>''"
 (*<*)by(simp add: exec_all_def)(*>*)
 
 lemma jvm_one_step1[trans]:
  "\<lbrakk> P \<turnstile> \<sigma> -jvm\<rightarrow>\<^sub>1 \<sigma>'; P \<turnstile> \<sigma>' -jvm\<rightarrow> \<sigma>'' \<rbrakk> \<Longrightarrow> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>''"
 (*<*) by (simp add: exec_all_def1) (*>*)
 
 lemma jvm_one_step2[trans]:
  "\<lbrakk> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'; P \<turnstile> \<sigma>' -jvm\<rightarrow>\<^sub>1 \<sigma>'' \<rbrakk> \<Longrightarrow> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>''"
 (*<*) by (simp add: exec_all_def1) (*>*)
 
 lemma exec_all_conf:
   "\<lbrakk> P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'; P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'' \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<sigma>' -jvm\<rightarrow> \<sigma>'' \<or> P \<turnstile> \<sigma>'' -jvm\<rightarrow> \<sigma>'"
 (*<*)by(simp add: exec_all_def single_valued_def single_valued_confluent)(*>*)
 
 
 lemma exec_all_finalD: "P \<turnstile> (x, h, []) -jvm\<rightarrow> \<sigma> \<Longrightarrow> \<sigma> = (x, h, [])"
 (*<*)
-apply(simp only: exec_all_def)
-apply(erule converse_rtranclE)
- apply simp
-apply simp
-done
+proof -
+  assume "P \<turnstile> (x, h, []) -jvm\<rightarrow> \<sigma>"
+  then have "((x, h, []), \<sigma>) \<in> {(\<sigma>, \<sigma>'). exec (P, \<sigma>) = \<lfloor>\<sigma>'\<rfloor>}\<^sup>*"
+    by(simp only: exec_all_def)
+  then show ?thesis proof(rule converse_rtranclE) qed simp+
+qed
 (*>*)
 
 lemma exec_all_deterministic:
   "\<lbrakk> P \<turnstile> \<sigma> -jvm\<rightarrow> (x,h,[]); P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>' \<rbrakk> \<Longrightarrow> P \<turnstile> \<sigma>' -jvm\<rightarrow> (x,h,[])"
 (*<*)
-apply(drule (1) exec_all_conf)
-apply(blast dest!: exec_all_finalD)
-done
+proof -
+  assume assms: "P \<turnstile> \<sigma> -jvm\<rightarrow> (x,h,[])" "P \<turnstile> \<sigma> -jvm\<rightarrow> \<sigma>'"
+  show ?thesis using exec_all_conf[OF assms]
+    by(blast dest!: exec_all_finalD)
+qed
 (*>*)
 
 
 text \<open>
   The start configuration of the JVM: in the start heap, we call a 
   method \<open>m\<close> of class \<open>C\<close> in program \<open>P\<close>. The 
   \<open>this\<close> pointer of the frame is set to \<open>Null\<close> to simulate
   a static method invokation.
 \<close>
 definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where
   "start_state P C M =
   (let (D,Ts,T,mxs,mxl\<^sub>0,b) = method P C M in
     (None, start_heap P, [([], Null # replicate mxl\<^sub>0 undefined, C, M, 0)]))"
 
 end