diff --git a/thys/Jinja/J/DefAss.thy b/thys/Jinja/J/DefAss.thy
--- a/thys/Jinja/J/DefAss.thy
+++ b/thys/Jinja/J/DefAss.thy
@@ -1,194 +1,194 @@
 (*  Title:      Jinja/DefAss.thy
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Definite assignment\<close>
 
 theory DefAss imports BigStep begin
 
 subsection "Hypersets"
 
 type_synonym 'a hyperset = "'a set option"
 
 definition hyperUn :: "'a hyperset \<Rightarrow> 'a hyperset \<Rightarrow> 'a hyperset"   (infixl "\<squnion>" 65)
 where
   "A \<squnion> B  \<equiv>  case A of None \<Rightarrow> None
                  | \<lfloor>A\<rfloor> \<Rightarrow> (case B of None \<Rightarrow> None | \<lfloor>B\<rfloor> \<Rightarrow> \<lfloor>A \<union> B\<rfloor>)"
 
 definition hyperInt :: "'a hyperset \<Rightarrow> 'a hyperset \<Rightarrow> 'a hyperset"   (infixl "\<sqinter>" 70)
 where
   "A \<sqinter> B  \<equiv>  case A of None \<Rightarrow> B
                  | \<lfloor>A\<rfloor> \<Rightarrow> (case B of None \<Rightarrow> \<lfloor>A\<rfloor> | \<lfloor>B\<rfloor> \<Rightarrow> \<lfloor>A \<inter> B\<rfloor>)"
 
 definition hyperDiff1 :: "'a hyperset \<Rightarrow> 'a \<Rightarrow> 'a hyperset"   (infixl "\<ominus>" 65)
 where
   "A \<ominus> a  \<equiv>  case A of None \<Rightarrow> None | \<lfloor>A\<rfloor> \<Rightarrow> \<lfloor>A - {a}\<rfloor>"
 
 definition hyper_isin :: "'a \<Rightarrow> 'a hyperset \<Rightarrow> bool"   (infix "\<in>\<in>" 50)
 where
   "a \<in>\<in> A  \<equiv>  case A of None \<Rightarrow> True | \<lfloor>A\<rfloor> \<Rightarrow> a \<in> A"
 
 definition hyper_subset :: "'a hyperset \<Rightarrow> 'a hyperset \<Rightarrow> bool"   (infix "\<sqsubseteq>" 50)
 where
   "A \<sqsubseteq> B  \<equiv>  case B of None \<Rightarrow> True
                  | \<lfloor>B\<rfloor> \<Rightarrow> (case A of None \<Rightarrow> False | \<lfloor>A\<rfloor> \<Rightarrow> A \<subseteq> B)"
 
 lemmas hyperset_defs =
  hyperUn_def hyperInt_def hyperDiff1_def hyper_isin_def hyper_subset_def
 
 lemma [simp]: "\<lfloor>{}\<rfloor> \<squnion> A = A  \<and>  A \<squnion> \<lfloor>{}\<rfloor> = A"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma [simp]: "\<lfloor>A\<rfloor> \<squnion> \<lfloor>B\<rfloor> = \<lfloor>A \<union> B\<rfloor> \<and> \<lfloor>A\<rfloor> \<ominus> a = \<lfloor>A - {a}\<rfloor>"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma [simp]: "None \<squnion> A = None \<and> A \<squnion> None = None"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma [simp]: "a \<in>\<in> None \<and> None \<ominus> a = None"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma hyperUn_assoc: "(A \<squnion> B) \<squnion> C = A \<squnion> (B \<squnion> C)"
 (*<*)by(simp add:hyperset_defs Un_assoc)(*>*)
 
 lemma hyper_insert_comm: "A \<squnion> \<lfloor>{a}\<rfloor> = \<lfloor>{a}\<rfloor> \<squnion> A \<and> A \<squnion> (\<lfloor>{a}\<rfloor> \<squnion> B) = \<lfloor>{a}\<rfloor> \<squnion> (A \<squnion> B)"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 
 subsection "Definite assignment"
 
 primrec
   \<A>  :: "'a exp \<Rightarrow> 'a hyperset"
   and \<A>s :: "'a exp list \<Rightarrow> 'a hyperset"
 where
   "\<A> (new C) = \<lfloor>{}\<rfloor>"
 | "\<A> (Cast C e) = \<A> e"
 | "\<A> (Val v) = \<lfloor>{}\<rfloor>"
 | "\<A> (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = \<A> e\<^sub>1 \<squnion> \<A> e\<^sub>2"
 | "\<A> (Var V) = \<lfloor>{}\<rfloor>"
 | "\<A> (LAss V e) = \<lfloor>{V}\<rfloor> \<squnion> \<A> e"
 | "\<A> (e\<bullet>F{D}) = \<A> e"
 | "\<A> (e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = \<A> e\<^sub>1 \<squnion> \<A> e\<^sub>2"
 | "\<A> (e\<bullet>M(es)) = \<A> e \<squnion> \<A>s es"
 | "\<A> ({V:T; e}) = \<A> e \<ominus> V"
 | "\<A> (e\<^sub>1;;e\<^sub>2) = \<A> e\<^sub>1 \<squnion> \<A> e\<^sub>2"
 | "\<A> (if (e) e\<^sub>1 else e\<^sub>2) =  \<A> e \<squnion> (\<A> e\<^sub>1 \<sqinter> \<A> e\<^sub>2)"
 | "\<A> (while (b) e) = \<A> b"
 | "\<A> (throw e) = None"
 | "\<A> (try e\<^sub>1 catch(C V) e\<^sub>2) = \<A> e\<^sub>1 \<sqinter> (\<A> e\<^sub>2 \<ominus> V)"
 
 | "\<A>s ([]) = \<lfloor>{}\<rfloor>"
 | "\<A>s (e#es) = \<A> e \<squnion> \<A>s es"
 
 primrec
   \<D>  :: "'a exp \<Rightarrow> 'a hyperset \<Rightarrow> bool"
   and \<D>s :: "'a exp list \<Rightarrow> 'a hyperset \<Rightarrow> bool"
 where
   "\<D> (new C) A = True"
 | "\<D> (Cast C e) A = \<D> e A"
 | "\<D> (Val v) A = True"
 | "\<D> (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e\<^sub>1))"
 | "\<D> (Var V) A = (V \<in>\<in> A)"
 | "\<D> (LAss V e) A = \<D> e A"
 | "\<D> (e\<bullet>F{D}) A = \<D> e A"
 | "\<D> (e\<^sub>1\<bullet>F{D}:=e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e\<^sub>1))"
 | "\<D> (e\<bullet>M(es)) A = (\<D> e A \<and> \<D>s es (A \<squnion> \<A> e))"
 | "\<D> ({V:T; e}) A = \<D> e (A \<ominus> V)"
 | "\<D> (e\<^sub>1;;e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e\<^sub>1))"
 | "\<D> (if (e) e\<^sub>1 else e\<^sub>2) A =
   (\<D> e A \<and> \<D> e\<^sub>1 (A \<squnion> \<A> e) \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e))"
 | "\<D> (while (e) c) A = (\<D> e A \<and> \<D> c (A \<squnion> \<A> e))"
 | "\<D> (throw e) A = \<D> e A"
 | "\<D> (try e\<^sub>1 catch(C V) e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<lfloor>{V}\<rfloor>))"
 
 | "\<D>s ([]) A = True"
 | "\<D>s (e#es) A = (\<D> e A \<and> \<D>s es (A \<squnion> \<A> e))"
 
 lemma As_map_Val[simp]: "\<A>s (map Val vs) = \<lfloor>{}\<rfloor>"
 (*<*)by (induct vs) simp_all(*>*)
 
 lemma D_append[iff]: "\<And>A. \<D>s (es @ es') A = (\<D>s es A \<and> \<D>s es' (A \<squnion> \<A>s es))"
 (*<*)by (induct es type:list) (auto simp:hyperUn_assoc)(*>*)
 
 
 lemma A_fv: "\<And>A. \<A> e = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> fv e"
 and  "\<And>A. \<A>s es = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> fvs es"
 (*<*)
-apply(induct e and es rule: \<A>.induct \<A>s.induct)
-apply (simp_all add:hyperset_defs)
-apply blast+
-done
+by (induct e and es rule: \<A>.induct \<A>s.induct)
+   (fastforce simp add:hyperset_defs)+
 (*>*)
 
 
 lemma sqUn_lem: "A \<sqsubseteq> A' \<Longrightarrow> A \<squnion> B \<sqsubseteq> A' \<squnion> B"
 (*<*)by(simp add:hyperset_defs) blast(*>*)
 
 lemma diff_lem: "A \<sqsubseteq> A' \<Longrightarrow> A \<ominus> b \<sqsubseteq> A' \<ominus> b"
 (*<*)by(simp add:hyperset_defs) blast(*>*)
 
 (* This order of the premises avoids looping of the simplifier *)
 lemma D_mono: "\<And>A A'. A \<sqsubseteq> A' \<Longrightarrow> \<D> e A \<Longrightarrow> \<D> (e::'a exp) A'"
 and Ds_mono: "\<And>A A'. A \<sqsubseteq> A' \<Longrightarrow> \<D>s es A \<Longrightarrow> \<D>s (es::'a exp list) A'"
 (*<*)
-apply(induct e and es rule: \<D>.induct \<D>s.induct)
-apply simp
-apply simp
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-apply (fastforce simp add:hyperset_defs)
-apply simp
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-apply simp apply (iprover dest:sqUn_lem)
-apply simp apply (iprover dest:diff_lem)
-apply simp apply (iprover dest:sqUn_lem)
-apply simp apply (iprover dest:sqUn_lem)
-apply simp apply (iprover dest:sqUn_lem)
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-done
+proof(induct e and es rule: \<D>.induct \<D>s.induct)
+  case BinOp then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Var then show ?case by (fastforce simp add:hyperset_defs)
+next
+  case FAss then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Call then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Block then show ?case by simp (iprover dest:diff_lem)
+next
+  case Seq then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Cond then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case While then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case TryCatch then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Cons_exp then show ?case by simp (iprover dest:sqUn_lem)
+qed simp_all
 (*>*)
 
 (* And this is the order of premises preferred during application: *)
 lemma D_mono': "\<D> e A \<Longrightarrow> A \<sqsubseteq> A' \<Longrightarrow> \<D> e A'"
 and Ds_mono': "\<D>s es A \<Longrightarrow> A \<sqsubseteq> A' \<Longrightarrow> \<D>s es A'"
 (*<*)by(blast intro:D_mono, blast intro:Ds_mono)(*>*)
 
 (*
 text{* @{term"\<A>"} is sound w.r.t.\ the big step semantics: it
 computes a conservative approximation of the variables actually
 assigned to. *}
 
 lemma "P \<turnstile> \<langle>e,(h\<^sub>0,l\<^sub>0)\<rangle> \<Rightarrow> \<langle>e',(h\<^sub>1,l\<^sub>1)\<rangle> \<Longrightarrow> (!!A. \<A> e = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> dom l\<^sub>1)"
 and "P \<turnstile> \<langle>es,(h\<^sub>0,l\<^sub>0)\<rangle> [\<Rightarrow>] \<langle>es',(h\<^sub>1,l\<^sub>1)\<rangle> \<Longrightarrow> (!!A. \<A>s es = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> dom l\<^sub>1)"
 
 proof (induct rule:eval_evals_induct)
   case LAss thus ?case apply(simp add:dom_def hyperset_defs) apply blast
 apply blast
 next
   case FAss thus ?case by simp (blast dest:eval_lcl_incr)
 next
   case BinOp thus ?case by simp (blast dest:eval_lcl_incr)
 next
   case Call thus  ?case by simp (blast dest:evals_lcl_incr)
 next
   case Cons thus ?case by simp (blast dest:evals_lcl_incr)
 next
   case Block thus ?case by(simp del: fun_upd_apply) blast
 next
   case Seq thus ?case by simp (blast dest:eval_lcl_incr)
 next
   case CondT thus ?case by simp (blast dest:eval_lcl_incr)
 next
   case CondF thus ?case by simp (blast dest:eval_lcl_incr)
 next
   case Try thus ?case by(fastforce dest!: eval_lcl_incr)
 next
   case TryCatch thus ?case by(fastforce dest!: eval_lcl_incr)
 qed auto
 *)
 end
diff --git a/thys/Jinja/J/JWellForm.thy b/thys/Jinja/J/JWellForm.thy
--- a/thys/Jinja/J/JWellForm.thy
+++ b/thys/Jinja/J/JWellForm.thy
@@ -1,64 +1,53 @@
 (*  Title:      Jinja/J/JWellForm.thy
 
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Well-formedness Constraints\<close>
 
 theory JWellForm
 imports "../Common/WellForm" WWellForm WellType DefAss
 begin
 
 definition wf_J_mdecl :: "J_prog \<Rightarrow> cname \<Rightarrow> J_mb mdecl \<Rightarrow> bool"
 where
   "wf_J_mdecl P C  \<equiv>  \<lambda>(M,Ts,T,(pns,body)).
   length Ts = length pns \<and>
   distinct pns \<and>
   this \<notin> set pns \<and>
   (\<exists>T'. P,[this\<mapsto>Class C,pns[\<mapsto>]Ts] \<turnstile> body :: T' \<and> P \<turnstile> T' \<le> T) \<and>
   \<D> body \<lfloor>{this} \<union> set pns\<rfloor>"
 
 lemma wf_J_mdecl[simp]:
   "wf_J_mdecl P C (M,Ts,T,pns,body) \<equiv>
   (length Ts = length pns \<and>
   distinct pns \<and>
   this \<notin> set pns \<and>
   (\<exists>T'. P,[this\<mapsto>Class C,pns[\<mapsto>]Ts] \<turnstile> body :: T' \<and> P \<turnstile> T' \<le> T) \<and>
   \<D> body \<lfloor>{this} \<union> set pns\<rfloor>)"
 (*<*)by(simp add:wf_J_mdecl_def)(*>*)
 
 
 abbreviation
   wf_J_prog :: "J_prog \<Rightarrow> bool" where
   "wf_J_prog == wf_prog wf_J_mdecl"
 
 lemma wf_J_prog_wf_J_mdecl:
   "\<lbrakk> wf_J_prog P; (C, D, fds, mths) \<in> set P; jmdcl \<in> set mths \<rbrakk>
   \<Longrightarrow> wf_J_mdecl P C jmdcl"
-(*<*)
-apply (simp add: wf_prog_def)
-apply (simp add: wf_cdecl_def)
-apply (erule conjE)+
-apply (drule bspec, assumption)
-apply simp
-apply (erule conjE)+
-apply (drule bspec, assumption)
-apply (simp add: wf_mdecl_def split_beta)
-done
-(*>*)
+(*<*)by(fastforce simp: wf_prog_def wf_cdecl_def wf_mdecl_def)(*>*)
 
 
 lemma wf_mdecl_wwf_mdecl: "wf_J_mdecl P C Md \<Longrightarrow> wwf_J_mdecl P C Md"
 (*<*)by(fastforce simp:wwf_J_mdecl_def dest!:WT_fv)(*>*)
 
 
 lemma wf_prog_wwf_prog: "wf_J_prog P \<Longrightarrow> wwf_J_prog P"
 (*<*)
-apply(simp add:wf_prog_def wf_cdecl_def wf_mdecl_def)
-apply(fast intro:wf_mdecl_wwf_mdecl)
-done
+by (simp add:wf_prog_def wf_cdecl_def wf_mdecl_def)
+   (fast intro:wf_mdecl_wwf_mdecl)
 (*>*)
 
 
 end
diff --git a/thys/Jinja/J/Progress.thy b/thys/Jinja/J/Progress.thy
--- a/thys/Jinja/J/Progress.thy
+++ b/thys/Jinja/J/Progress.thy
@@ -1,626 +1,619 @@
 (*  Title:      Jinja/J/SmallProgress.thy
 
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Progress of Small Step Semantics\<close>
 
 theory Progress
 imports Equivalence WellTypeRT DefAss "../Common/Conform"
 begin
 
 lemma final_addrE:
   "\<lbrakk> P,E,h \<turnstile> e : Class C; final e;
     \<And>a. e = addr a \<Longrightarrow> R;
     \<And>a. e = Throw a \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
 (*<*)by(auto simp:final_def)(*>*)
 
 
 lemma finalRefE:
  "\<lbrakk> P,E,h \<turnstile> e : T; is_refT T; final e;
    e = null \<Longrightarrow> R;
    \<And>a C. \<lbrakk> e = addr a; T = Class C \<rbrakk> \<Longrightarrow> R;
    \<And>a. e = Throw a \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
 (*<*)by(auto simp:final_def is_refT_def)(*>*)
 
 
 text\<open>Derivation of new induction scheme for well typing:\<close>
 
 inductive
   WTrt' :: "[J_prog,heap,env,expr,ty] \<Rightarrow> bool"
   and WTrts' :: "[J_prog,heap,env,expr list, ty list] \<Rightarrow> bool"
   and WTrt2' :: "[J_prog,env,heap,expr,ty] \<Rightarrow> bool"
         ("_,_,_ \<turnstile> _ :'' _"   [51,51,51]50)
   and WTrts2' :: "[J_prog,env,heap,expr list, ty list] \<Rightarrow> bool"
         ("_,_,_ \<turnstile> _ [:''] _" [51,51,51]50)
   for P :: J_prog and h :: heap
 where
   "P,E,h \<turnstile> e :' T \<equiv> WTrt' P h E e T"
 | "P,E,h \<turnstile> es [:'] Ts \<equiv> WTrts' P h E es Ts"
 
 | "is_class P C  \<Longrightarrow>  P,E,h \<turnstile> new C :' Class C"
 | "\<lbrakk> P,E,h \<turnstile> e :' T; is_refT T; is_class P C \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> Cast C e :' Class C"
 | "typeof\<^bsub>h\<^esub> v = Some T \<Longrightarrow> P,E,h \<turnstile> Val v :' T"
 | "E v = Some T  \<Longrightarrow>  P,E,h \<turnstile> Var v :' T"
 | "\<lbrakk> P,E,h \<turnstile> e\<^sub>1 :' T\<^sub>1;  P,E,h \<turnstile> e\<^sub>2 :' T\<^sub>2 \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> e\<^sub>1 \<guillemotleft>Eq\<guillemotright> e\<^sub>2 :' Boolean"
 | "\<lbrakk> P,E,h \<turnstile> e\<^sub>1 :' Integer;  P,E,h \<turnstile> e\<^sub>2 :' Integer \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> e\<^sub>1 \<guillemotleft>Add\<guillemotright> e\<^sub>2 :' Integer"
 | "\<lbrakk> P,E,h \<turnstile> Var V :' T;  P,E,h \<turnstile> e :' T';  P \<turnstile> T' \<le> T \<^cancel>\<open>V \<noteq> This\<close> \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> V:=e :' Void"
 | "\<lbrakk> P,E,h \<turnstile> e :' Class C; P \<turnstile> C has F:T in D \<rbrakk> \<Longrightarrow> P,E,h \<turnstile> e\<bullet>F{D} :' T"
 | "P,E,h \<turnstile> e :' NT \<Longrightarrow> P,E,h \<turnstile> e\<bullet>F{D} :' T"
 | "\<lbrakk> P,E,h \<turnstile> e\<^sub>1 :' Class C;  P \<turnstile> C has F:T in D;
     P,E,h \<turnstile> e\<^sub>2 :' T\<^sub>2;  P \<turnstile> T\<^sub>2 \<le> T \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> e\<^sub>1\<bullet>F{D}:=e\<^sub>2 :' Void"
 | "\<lbrakk> P,E,h \<turnstile> e\<^sub>1:'NT; P,E,h \<turnstile> e\<^sub>2 :' T\<^sub>2 \<rbrakk> \<Longrightarrow> P,E,h \<turnstile> e\<^sub>1\<bullet>F{D}:=e\<^sub>2 :' Void"
 | "\<lbrakk> P,E,h \<turnstile> e :' Class C; P \<turnstile> C sees M:Ts \<rightarrow> T = (pns,body) in D;
     P,E,h \<turnstile> es [:'] Ts'; P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> e\<bullet>M(es) :' T"
 | "\<lbrakk> P,E,h \<turnstile> e :' NT; P,E,h \<turnstile> es [:'] Ts \<rbrakk> \<Longrightarrow> P,E,h \<turnstile> e\<bullet>M(es) :' T"
 | "P,E,h \<turnstile> [] [:'] []"
 | "\<lbrakk> P,E,h \<turnstile> e :' T;  P,E,h \<turnstile> es [:'] Ts \<rbrakk> \<Longrightarrow>  P,E,h \<turnstile> e#es [:'] T#Ts"
 | "\<lbrakk> typeof\<^bsub>h\<^esub> v = Some T\<^sub>1; P \<turnstile> T\<^sub>1 \<le> T; P,E(V\<mapsto>T),h \<turnstile> e\<^sub>2 :' T\<^sub>2 \<rbrakk>
   \<Longrightarrow>  P,E,h \<turnstile> {V:T := Val v; e\<^sub>2} :' T\<^sub>2"
 | "\<lbrakk> P,E(V\<mapsto>T),h \<turnstile> e :' T'; \<not> assigned V e \<rbrakk> \<Longrightarrow>  P,E,h \<turnstile> {V:T; e} :' T'"
 | "\<lbrakk> P,E,h \<turnstile> e\<^sub>1:' T\<^sub>1;  P,E,h \<turnstile> e\<^sub>2:'T\<^sub>2 \<rbrakk>  \<Longrightarrow>  P,E,h \<turnstile> e\<^sub>1;;e\<^sub>2 :' T\<^sub>2"
 | "\<lbrakk> P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> e\<^sub>1:' T\<^sub>1;  P,E,h \<turnstile> e\<^sub>2:' T\<^sub>2;
     P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<or> P \<turnstile> T\<^sub>2 \<le> T\<^sub>1;
     P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<longrightarrow> T = T\<^sub>2; P \<turnstile> T\<^sub>2 \<le> T\<^sub>1 \<longrightarrow> T = T\<^sub>1 \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :' T"
 (*
  "\<lbrakk> P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> e\<^sub>1:' T\<^sub>1;  P,E,h \<turnstile> e\<^sub>2:' T\<^sub>2; P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :' T\<^sub>2"
  "\<lbrakk> P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> e\<^sub>1:' T\<^sub>1;  P,E,h \<turnstile> e\<^sub>2:' T\<^sub>2; P \<turnstile> T\<^sub>2 \<le> T\<^sub>1 \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :' T\<^sub>1"
 *)
 | "\<lbrakk> P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> c:' T \<rbrakk>
   \<Longrightarrow>  P,E,h \<turnstile> while(e) c :' Void"
 | "\<lbrakk> P,E,h \<turnstile> e :' T\<^sub>r; is_refT T\<^sub>r \<rbrakk>  \<Longrightarrow>  P,E,h \<turnstile> throw e :' T"
 | "\<lbrakk> P,E,h \<turnstile> e\<^sub>1 :' T\<^sub>1;  P,E(V \<mapsto> Class C),h \<turnstile> e\<^sub>2 :' T\<^sub>2; P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 :' T\<^sub>2"
 
 (*<*)
 lemmas WTrt'_induct = WTrt'_WTrts'.induct [split_format (complete)]
   and WTrt'_inducts = WTrt'_WTrts'.inducts [split_format (complete)]
 
 inductive_cases WTrt'_elim_cases[elim!]:
   "P,E,h \<turnstile> V :=e :' T"
 (*>*)
 
 lemma [iff]: "P,E,h \<turnstile> e\<^sub>1;;e\<^sub>2 :' T\<^sub>2 = (\<exists>T\<^sub>1. P,E,h \<turnstile> e\<^sub>1:' T\<^sub>1 \<and> P,E,h \<turnstile> e\<^sub>2:' T\<^sub>2)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)
 
 lemma [iff]: "P,E,h \<turnstile> Val v :' T = (typeof\<^bsub>h\<^esub> v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)
 
 lemma [iff]: "P,E,h \<turnstile> Var v :' T = (E v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)
 
 
 lemma wt_wt': "P,E,h \<turnstile> e : T \<Longrightarrow> P,E,h \<turnstile> e :' T"
 and wts_wts': "P,E,h \<turnstile> es [:] Ts \<Longrightarrow> P,E,h \<turnstile> es [:'] Ts"
 (*<*)
-apply (induct rule:WTrt_inducts)
-prefer 14
-apply(case_tac "assigned V e")
-apply(clarsimp simp add:fun_upd_same assigned_def simp del:fun_upd_apply)
-apply(erule (2) WTrt'_WTrts'.intros)
-apply(erule (1) WTrt'_WTrts'.intros)
-apply(blast intro:WTrt'_WTrts'.intros)+
-done
+proof(induct rule:WTrt_inducts)
+  case (WTrtBlock E V T e T')
+  then show ?case
+  proof(cases "assigned V e")
+    case True then show ?thesis using WTrtBlock.hyps(2)
+      by(clarsimp simp add:fun_upd_same assigned_def WTrt'_WTrts'.intros
+                  simp del:fun_upd_apply)
+  next
+    case False then show ?thesis
+      by (simp add: WTrtBlock.hyps(2) WTrt'_WTrts'.intros)
+  qed
+qed (blast intro:WTrt'_WTrts'.intros)+
 (*>*)
 
 
 lemma wt'_wt: "P,E,h \<turnstile> e :' T \<Longrightarrow> P,E,h \<turnstile> e : T"
 and wts'_wts: "P,E,h \<turnstile> es [:'] Ts \<Longrightarrow> P,E,h \<turnstile> es [:] Ts"
 (*<*)
-apply (induct rule:WTrt'_inducts)
-prefer 16
-apply(rule WTrt_WTrts.intros)
-apply(rule WTrt_WTrts.intros)
-apply(rule WTrt_WTrts.intros)
-apply simp
-apply(erule (2) WTrt_WTrts.intros)
-apply(blast intro:WTrt_WTrts.intros)+
-done
+proof(induct rule:WTrt'_inducts)
+  case Block: (16 v T\<^sub>1 T E V e\<^sub>2 T\<^sub>2)
+  let ?E = "E(V \<mapsto> T)"
+  have "P,?E,h \<turnstile> Val v : T\<^sub>1" using Block.hyps(1) by simp
+  moreover have "P \<turnstile> T\<^sub>1 \<le> T" by(rule Block.hyps(2))
+  ultimately have "P,?E,h \<turnstile> V:=Val v : Void" using WTrtLAss by simp
+  moreover have "P,?E,h \<turnstile> e\<^sub>2 : T\<^sub>2" by(rule Block.hyps(4))
+  ultimately have "P,?E,h \<turnstile> V:=Val v;; e\<^sub>2 : T\<^sub>2" by blast
+  then show ?case by simp
+qed (blast intro:WTrt_WTrts.intros)+
 (*>*)
 
 
 corollary wt'_iff_wt: "(P,E,h \<turnstile> e :' T) = (P,E,h \<turnstile> e : T)"
 (*<*)by(blast intro:wt_wt' wt'_wt)(*>*)
 
 
 corollary wts'_iff_wts: "(P,E,h \<turnstile> es [:'] Ts) = (P,E,h \<turnstile> es [:] Ts)"
 (*<*)by(blast intro:wts_wts' wts'_wts)(*>*)
 
 (*<*)
 lemmas WTrt_inducts2 = WTrt'_inducts [unfolded wt'_iff_wt wts'_iff_wts,
  case_names WTrtNew WTrtCast WTrtVal WTrtVar WTrtBinOpEq WTrtBinOpAdd WTrtLAss WTrtFAcc WTrtFAccNT WTrtFAss
  WTrtFAssNT WTrtCall WTrtCallNT WTrtNil WTrtCons WTrtInitBlock WTrtBlock WTrtSeq WTrtCond
  WTrtWhile WTrtThrow WTrtTry, consumes 1]
 (*>*)
 
 theorem assumes wf: "wwf_J_prog P" and hconf: "P \<turnstile> h \<surd>"
 shows progress: "P,E,h \<turnstile> e : T \<Longrightarrow>
  (\<And>l. \<lbrakk> \<D> e \<lfloor>dom l\<rfloor>; \<not> final e \<rbrakk> \<Longrightarrow> \<exists>e' s'. P \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',s'\<rangle>)"
 and "P,E,h \<turnstile> es [:] Ts \<Longrightarrow>
  (\<And>l. \<lbrakk> \<D>s es \<lfloor>dom l\<rfloor>; \<not> finals es \<rbrakk> \<Longrightarrow> \<exists>es' s'. P \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',s'\<rangle>)"
 (*<*)
 proof (induct rule:WTrt_inducts2)
   case WTrtNew
   show ?case
   proof cases
     assume "\<exists>a. h a = None"
     with assms WTrtNew show ?thesis
       by (fastforce del:exE intro!:RedNew simp add:new_Addr_def
                    elim!:wf_Fields_Ex[THEN exE])
   next
     assume "\<not>(\<exists>a. h a = None)"
     with assms WTrtNew show ?thesis
       by(fastforce intro:RedNewFail simp add:new_Addr_def)
   qed
 next
   case (WTrtCast E e T C)
   have wte: "P,E,h \<turnstile> e : T" and ref: "is_refT T"
    and IH: "\<And>l. \<lbrakk>\<D> e \<lfloor>dom l\<rfloor>; \<not> final e\<rbrakk>
                 \<Longrightarrow> \<exists>e' s'. P \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',s'\<rangle>"
    and D: "\<D> (Cast C e) \<lfloor>dom l\<rfloor>" by fact+
   from D have De: "\<D> e \<lfloor>dom l\<rfloor>" by auto
   show ?case
   proof cases
     assume "final e"
     with wte ref show ?thesis
     proof (rule finalRefE)
       assume "e = null" thus ?case by(fastforce intro:RedCastNull)
     next
       fix D a assume A: "T = Class D" "e = addr a"
       show ?thesis
       proof cases
         assume "P \<turnstile> D \<preceq>\<^sup>* C"
         thus ?thesis using A wte by(fastforce intro:RedCast)
       next
         assume "\<not> P \<turnstile> D \<preceq>\<^sup>* C"
         thus ?thesis using A wte by(force intro!:RedCastFail)
       qed
     next
       fix a assume "e = Throw a"
       thus ?thesis by(blast intro!:red_reds.CastThrow)
     qed
   next
     assume nf: "\<not> final e"
     from IH[OF De nf] show ?thesis by (blast intro:CastRed)
   qed
 next
   case WTrtVal thus ?case by(simp add:final_def)
 next
   case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def)
 next
   case (WTrtBinOpEq E e1 T1 e2 T2)
   show ?case
   proof cases
     assume "final e1"
     thus ?thesis
     proof (rule finalE)
       fix v1 assume [simp]: "e1 = Val v1"
       show ?thesis
       proof cases
         assume "final e2"
         thus ?thesis
         proof (rule finalE)
           fix v2 assume "e2 = Val v2"
           thus ?thesis using WTrtBinOpEq by(fastforce intro:RedBinOp)
         next
           fix a assume "e2 = Throw a"
           thus ?thesis by(auto intro:red_reds.BinOpThrow2)
         qed
       next
         assume "\<not> final e2" with WTrtBinOpEq show ?thesis
           by simp (fast intro!:BinOpRed2)
       qed
     next
       fix a assume "e1 = Throw a"
       thus ?thesis by simp (fast intro:red_reds.BinOpThrow1)
     qed
   next
     assume "\<not> final e1" with WTrtBinOpEq show ?thesis
       by simp (fast intro:BinOpRed1)
   qed
 next
   case (WTrtBinOpAdd E e1 e2)
   show ?case
   proof cases
     assume "final e1"
     thus ?thesis
     proof (rule finalE)
       fix v1 assume [simp]: "e1 = Val v1"
       show ?thesis
       proof cases
         assume "final e2"
         thus ?thesis
         proof (rule finalE)
           fix v2 assume "e2 = Val v2"
           thus ?thesis using WTrtBinOpAdd by(fastforce intro:RedBinOp)
         next
           fix a assume "e2 = Throw a"
           thus ?thesis by(auto intro:red_reds.BinOpThrow2)
         qed
       next
         assume "\<not> final e2" with WTrtBinOpAdd show ?thesis
           by simp (fast intro!:BinOpRed2)
       qed
     next
       fix a assume "e1 = Throw a"
       thus ?thesis by simp (fast intro:red_reds.BinOpThrow1)
     qed
   next
     assume "\<not> final e1" with WTrtBinOpAdd show ?thesis
       by simp (fast intro:BinOpRed1)
   qed
 next
   case (WTrtLAss E V T e T')
   show ?case
   proof cases
     assume "final e" with WTrtLAss show ?thesis
       by(auto simp:final_def intro!:RedLAss red_reds.LAssThrow)
   next
     assume "\<not> final e" with WTrtLAss show ?thesis
       by simp (fast intro:LAssRed)
   qed
 next
   case (WTrtFAcc E e C F T D)
   have wte: "P,E,h \<turnstile> e : Class C"
    and field: "P \<turnstile> C has F:T in D" by fact+
   show ?case
   proof cases
     assume "final e"
     with wte show ?thesis
     proof (rule final_addrE)
       fix a assume e: "e = addr a"
       with wte obtain fs where hp: "h a = Some(C,fs)" by auto
       with hconf have "P,h \<turnstile> (C,fs) \<surd>" using hconf_def by fastforce
       then obtain v where "fs(F,D) = Some v" using field
         by(fastforce dest:has_fields_fun simp:oconf_def has_field_def)
       with hp e show ?thesis by(fastforce intro:RedFAcc)
     next
       fix a assume "e = Throw a"
       thus ?thesis by(fastforce intro:red_reds.FAccThrow)
     qed
   next
     assume "\<not> final e" with WTrtFAcc show ?thesis
       by(fastforce intro!:FAccRed)
   qed
 next
   case (WTrtFAccNT E e F D T)
   show ?case
   proof cases
     assume "final e"  \<comment> \<open>@{term e} is @{term null} or @{term throw}\<close>
     with WTrtFAccNT show ?thesis
       by(fastforce simp:final_def intro: RedFAccNull red_reds.FAccThrow)
   next
     assume "\<not> final e" \<comment> \<open>@{term e} reduces by IH\<close>
     with WTrtFAccNT show ?thesis by simp (fast intro:FAccRed)
   qed
 next
   case (WTrtFAss E e1 C F T D e2 T2)
   have wte1: "P,E,h \<turnstile> e1 : Class C" by fact
   show ?case
   proof cases
     assume "final e1"
     with wte1 show ?thesis
     proof (rule final_addrE)
       fix a assume e1: "e1 = addr a"
       show ?thesis
       proof cases
         assume "final e2"
         thus ?thesis
         proof (rule finalE)
           fix v assume "e2 = Val v"
           thus ?thesis using e1 wte1 by(fastforce intro:RedFAss)
         next
           fix a assume "e2 = Throw a"
           thus ?thesis using e1 by(fastforce intro:red_reds.FAssThrow2)
         qed
       next
         assume "\<not> final e2" with WTrtFAss e1 show ?thesis
           by simp (fast intro!:FAssRed2)
       qed
     next
       fix a assume "e1 = Throw a"
       thus ?thesis by(fastforce intro:red_reds.FAssThrow1)
     qed
   next
     assume "\<not> final e1" with WTrtFAss show ?thesis
       by simp (blast intro!:FAssRed1)
   qed
 next
   case (WTrtFAssNT E e\<^sub>1 e\<^sub>2 T\<^sub>2 F D)
   show ?case
   proof cases
     assume e1: "final e\<^sub>1"  \<comment> \<open>@{term e\<^sub>1} is @{term null} or @{term throw}\<close>
     show ?thesis
     proof cases
       assume "final e\<^sub>2"  \<comment> \<open>@{term e\<^sub>2} is @{term Val} or @{term throw}\<close>
       with WTrtFAssNT e1 show ?thesis
         by(fastforce simp:final_def intro: RedFAssNull red_reds.FAssThrow1 red_reds.FAssThrow2)
     next
       assume "\<not> final e\<^sub>2" \<comment> \<open>@{term e\<^sub>2} reduces by IH\<close>
       with WTrtFAssNT e1 show ?thesis
         by (fastforce  simp:final_def intro!:red_reds.FAssRed2 red_reds.FAssThrow1)
     qed
   next
     assume "\<not> final e\<^sub>1" \<comment> \<open>@{term e\<^sub>1} reduces by IH\<close>
     with WTrtFAssNT show ?thesis by (fastforce intro:FAssRed1)
   qed
 next
   case (WTrtCall E e C M Ts T pns body D es Ts')
   have wte: "P,E,h \<turnstile> e : Class C"
    and "method": "P \<turnstile> C sees M:Ts\<rightarrow>T = (pns,body) in D"
    and wtes: "P,E,h \<turnstile> es [:] Ts'"and sub: "P \<turnstile> Ts' [\<le>] Ts"
    and IHes: "\<And>l.
              \<lbrakk>\<D>s es \<lfloor>dom l\<rfloor>; \<not> finals es\<rbrakk>
              \<Longrightarrow> \<exists>es' s'. P \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',s'\<rangle>"
    and D: "\<D> (e\<bullet>M(es)) \<lfloor>dom l\<rfloor>" by fact+
   show ?case
   proof cases
     assume "final e"
     with wte show ?thesis
     proof (rule final_addrE)
       fix a assume e_addr: "e = addr a"
       show ?thesis
       proof cases
         assume es: "\<exists>vs. es = map Val vs"
         from wte e_addr obtain fs where ha: "h a = Some(C,fs)" by auto
         show ?thesis
           using e_addr ha "method" WTrts_same_length[OF wtes] sub es sees_wf_mdecl[OF wf "method"]
           by (fastforce intro!: RedCall simp:list_all2_iff wf_mdecl_def)
       next
         assume "\<not>(\<exists>vs. es = map Val vs)"
         hence not_all_Val: "\<not>(\<forall>e \<in> set es. \<exists>v. e = Val v)"
           by(simp add:ex_map_conv)
         let ?ves = "takeWhile (\<lambda>e. \<exists>v. e = Val v) es"
         let ?rest = "dropWhile (\<lambda>e. \<exists>v. e = Val v) es"
         let ?ex = "hd ?rest" let ?rst = "tl ?rest"
         from not_all_Val have nonempty: "?rest \<noteq> []" by auto
         hence es: "es = ?ves @ ?ex # ?rst" by simp
         have "\<forall>e \<in> set ?ves. \<exists>v. e = Val v" by(fastforce dest:set_takeWhileD)
         then obtain vs where ves: "?ves = map Val vs"
           using ex_map_conv by blast
         show ?thesis
         proof cases
           assume "final ?ex"
           moreover from nonempty have "\<not>(\<exists>v. ?ex = Val v)"
             by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
               (simp add:dropWhile_eq_Cons_conv)
           ultimately obtain b where ex_Throw: "?ex = Throw b"
             by(fast elim!:finalE)
           show ?thesis using e_addr es ex_Throw ves
             by(fastforce intro:CallThrowParams)
         next
           assume not_fin: "\<not> final ?ex"
           have "finals es = finals(?ves @ ?ex # ?rst)" using es
             by(rule arg_cong)
           also have "\<dots> = finals(?ex # ?rst)" using ves by simp
           finally have "finals es = finals(?ex # ?rst)" .
           hence "\<not> finals es" using not_finals_ConsI[OF not_fin] by blast
           thus ?thesis using e_addr D IHes  by(fastforce intro!:CallParams)
         qed
       qed
     next
       fix a assume "e = Throw a"
       with WTrtCall.prems show ?thesis by(fast intro!:CallThrowObj)
     qed
   next
     assume "\<not> final e"
     with WTrtCall show ?thesis by simp (blast intro!:CallObj)
   qed
 next
   case (WTrtCallNT E e es Ts M T)
   show ?case
   proof cases
     assume "final e"
     moreover
     { fix v assume e: "e = Val v"
       hence "e = null" using WTrtCallNT by simp
       have ?case
       proof cases
         assume "finals es"
         moreover
         { fix vs assume "es = map Val vs"
           with WTrtCallNT e have ?thesis by(fastforce intro: RedCallNull) }
         moreover
         { fix vs a es' assume "es = map Val vs @ Throw a # es'"
           with WTrtCallNT e have ?thesis by(fastforce intro: CallThrowParams) }
         ultimately show ?thesis by(fastforce simp:finals_def)
       next
         assume "\<not> finals es" \<comment> \<open>@{term es} reduces by IH\<close>
         with WTrtCallNT e show ?thesis by(fastforce intro: CallParams)
       qed
     }
     moreover
     { fix a assume "e = Throw a"
       with WTrtCallNT have ?case by(fastforce intro: CallThrowObj) }
     ultimately show ?thesis by(fastforce simp:final_def)
   next
     assume "\<not> final e" \<comment> \<open>@{term e} reduces by IH\<close>
     with WTrtCallNT show ?thesis by (fastforce intro:CallObj)
   qed
 next
   case WTrtNil thus ?case by simp
 next
   case (WTrtCons E e T es Ts)
   have IHe: "\<And>l. \<lbrakk>\<D> e \<lfloor>dom l\<rfloor>; \<not> final e\<rbrakk>
                 \<Longrightarrow> \<exists>e' s'. P \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',s'\<rangle>"
    and IHes: "\<And>l. \<lbrakk>\<D>s es \<lfloor>dom l\<rfloor>; \<not> finals es\<rbrakk>
              \<Longrightarrow> \<exists>es' s'. P \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',s'\<rangle>"
    and D: "\<D>s (e#es) \<lfloor>dom l\<rfloor>" and not_fins: "\<not> finals(e # es)" by fact+
   have De: "\<D> e \<lfloor>dom l\<rfloor>" and Des: "\<D>s es (\<lfloor>dom l\<rfloor> \<squnion> \<A> e)"
     using D by auto
   show ?case
   proof cases
     assume "final e"
     thus ?thesis
     proof (rule finalE)
       fix v assume e: "e = Val v"
       hence Des': "\<D>s es \<lfloor>dom l\<rfloor>" using De Des by auto
       have not_fins_tl: "\<not> finals es" using not_fins e by simp
       show ?thesis using e IHes[OF Des' not_fins_tl]
         by (blast intro!:ListRed2)
     next
       fix a assume "e = Throw a"
       hence False using not_fins by simp
       thus ?thesis ..
     qed
   next
     assume "\<not> final e"
     with IHe[OF De] show ?thesis by(fast intro!:ListRed1)
   qed
 next
   case (WTrtInitBlock v T\<^sub>1 T E V e\<^sub>2 T\<^sub>2)
   have IH2: "\<And>l. \<lbrakk>\<D> e\<^sub>2 \<lfloor>dom l\<rfloor>; \<not> final e\<^sub>2\<rbrakk>
                   \<Longrightarrow> \<exists>e' s'. P \<turnstile> \<langle>e\<^sub>2,(h,l)\<rangle> \<rightarrow> \<langle>e',s'\<rangle>"
    and D: "\<D> {V:T := Val v; e\<^sub>2} \<lfloor>dom l\<rfloor>" by fact+
   show ?case
   proof cases
     assume "final e\<^sub>2"
     then show ?thesis
     proof (rule finalE)
       fix v\<^sub>2 assume "e\<^sub>2 = Val v\<^sub>2"
       thus ?thesis by(fast intro:RedInitBlock)
     next
       fix a assume "e\<^sub>2 = Throw a"
       thus ?thesis by(fast intro:red_reds.InitBlockThrow)
     qed
   next
     assume not_fin2: "\<not> final e\<^sub>2"
     from D have D2: "\<D> e\<^sub>2 \<lfloor>dom(l(V\<mapsto>v))\<rfloor>" by (auto simp:hyperset_defs)
     from IH2[OF D2 not_fin2]
     obtain h' l' e' where red2: "P \<turnstile> \<langle>e\<^sub>2,(h, l(V\<mapsto>v))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>"
       by auto
     from red_lcl_incr[OF red2] have "V \<in> dom l'" by auto
     with red2 show ?thesis by(fastforce intro:InitBlockRed)
   qed
 next
   case (WTrtBlock E V T e T')
   have IH: "\<And>l. \<lbrakk>\<D> e \<lfloor>dom l\<rfloor>; \<not> final e\<rbrakk>
                  \<Longrightarrow> \<exists>e' s'. P \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',s'\<rangle>"
    and unass: "\<not> assigned V e" and D: "\<D> {V:T; e} \<lfloor>dom l\<rfloor>" by fact+
   show ?case
   proof cases
     assume "final e"
     thus ?thesis
     proof (rule finalE)
       fix v assume "e = Val v" thus ?thesis by(fast intro:RedBlock)
     next
       fix a assume "e = Throw a"
       thus ?thesis by(fast intro:red_reds.BlockThrow)
     qed
   next
     assume not_fin: "\<not> final e"
     from D have De: "\<D> e \<lfloor>dom(l(V:=None))\<rfloor>" by(simp add:hyperset_defs)
     from IH[OF De not_fin]
     obtain h' l' e' where red: "P \<turnstile> \<langle>e,(h,l(V:=None))\<rangle> \<rightarrow> \<langle>e',(h',l')\<rangle>"
       by auto
     show ?thesis
     proof (cases "l' V")
       assume "l' V = None"
       with red unass show ?thesis by(blast intro: BlockRedNone)
     next
       fix v assume "l' V = Some v"
       with red unass show ?thesis by(blast intro: BlockRedSome)
     qed
   qed
 next
   case (WTrtSeq E e1 T1 e2 T2)
   show ?case
   proof cases
     assume "final e1"
     thus ?thesis
       by(fast elim:finalE intro:RedSeq red_reds.SeqThrow)
   next
     assume "\<not> final e1" with WTrtSeq show ?thesis
       by simp (blast intro:SeqRed)
   qed
 next
   case (WTrtCond E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T)
   have wt: "P,E,h \<turnstile> e : Boolean" by fact
   show ?case
   proof cases
     assume "final e"
     thus ?thesis
     proof (rule finalE)
       fix v assume val: "e = Val v"
       then obtain b where v: "v = Bool b" using wt by auto
       show ?thesis
       proof (cases b)
         case True with val v show ?thesis by(auto intro:RedCondT)
       next
         case False with val v show ?thesis by(auto intro:RedCondF)
       qed
     next
       fix a assume "e = Throw a"
       thus ?thesis by(fast intro:red_reds.CondThrow)
     qed
   next
     assume "\<not> final e" with WTrtCond show ?thesis
       by simp (fast intro:CondRed)
   qed
 next
   case WTrtWhile show ?case by(fast intro:RedWhile)
 next
   case (WTrtThrow E e T\<^sub>r T)
   show ?case
   proof cases
     assume "final e" \<comment> \<open>Then @{term e} must be @{term throw} or @{term null}\<close>
     with WTrtThrow show ?thesis
       by(fastforce simp:final_def is_refT_def
                   intro:red_reds.ThrowThrow red_reds.RedThrowNull)
   next
     assume "\<not> final e" \<comment> \<open>Then @{term e} must reduce\<close>
     with WTrtThrow show ?thesis by simp (blast intro:ThrowRed)
   qed
 next
   case (WTrtTry E e1 T1 V C e2 T2)
   have wt1: "P,E,h \<turnstile> e1 : T1" by fact
   show ?case
   proof cases
     assume "final e1"
     thus ?thesis
     proof (rule finalE)
       fix v assume "e1 = Val v"
       thus ?thesis by(fast intro:RedTry)
     next
       fix a assume e1_Throw: "e1 = Throw a"
       with wt1 obtain D fs where ha: "h a = Some(D,fs)" by fastforce
       show ?thesis
       proof cases
         assume "P \<turnstile> D \<preceq>\<^sup>* C"
         with e1_Throw ha show ?thesis by(fastforce intro!:RedTryCatch)
       next
         assume "\<not> P \<turnstile> D \<preceq>\<^sup>* C"
         with e1_Throw ha show ?thesis by(force intro!:RedTryFail)
       qed
     qed
   next
     assume "\<not> final e1"
     with WTrtTry show ?thesis by simp (fast intro:TryRed)
   qed
 qed
 (*>*)
 
 
 end
diff --git a/thys/JinjaDCI/J/DefAss.thy b/thys/JinjaDCI/J/DefAss.thy
--- a/thys/JinjaDCI/J/DefAss.thy
+++ b/thys/JinjaDCI/J/DefAss.thy
@@ -1,189 +1,192 @@
 (*  Title:      JinjaDCI/J/DefAss.thy
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/DefAss.thy by Tobias Nipkow
 *)
 
 section \<open> Definite assignment \<close>
 
 theory DefAss imports BigStep begin
 
 subsection "Hypersets"
 
 type_synonym 'a hyperset = "'a set option"
 
 definition hyperUn :: "'a hyperset \<Rightarrow> 'a hyperset \<Rightarrow> 'a hyperset"   (infixl "\<squnion>" 65)
 where
   "A \<squnion> B  \<equiv>  case A of None \<Rightarrow> None
                  | \<lfloor>A\<rfloor> \<Rightarrow> (case B of None \<Rightarrow> None | \<lfloor>B\<rfloor> \<Rightarrow> \<lfloor>A \<union> B\<rfloor>)"
 
 definition hyperInt :: "'a hyperset \<Rightarrow> 'a hyperset \<Rightarrow> 'a hyperset"   (infixl "\<sqinter>" 70)
 where
   "A \<sqinter> B  \<equiv>  case A of None \<Rightarrow> B
                  | \<lfloor>A\<rfloor> \<Rightarrow> (case B of None \<Rightarrow> \<lfloor>A\<rfloor> | \<lfloor>B\<rfloor> \<Rightarrow> \<lfloor>A \<inter> B\<rfloor>)"
 
 definition hyperDiff1 :: "'a hyperset \<Rightarrow> 'a \<Rightarrow> 'a hyperset"   (infixl "\<ominus>" 65)
 where
   "A \<ominus> a  \<equiv>  case A of None \<Rightarrow> None | \<lfloor>A\<rfloor> \<Rightarrow> \<lfloor>A - {a}\<rfloor>"
 
 definition hyper_isin :: "'a \<Rightarrow> 'a hyperset \<Rightarrow> bool"   (infix "\<in>\<in>" 50)
 where
   "a \<in>\<in> A  \<equiv>  case A of None \<Rightarrow> True | \<lfloor>A\<rfloor> \<Rightarrow> a \<in> A"
 
 definition hyper_subset :: "'a hyperset \<Rightarrow> 'a hyperset \<Rightarrow> bool"   (infix "\<sqsubseteq>" 50)
 where
   "A \<sqsubseteq> B  \<equiv>  case B of None \<Rightarrow> True
                  | \<lfloor>B\<rfloor> \<Rightarrow> (case A of None \<Rightarrow> False | \<lfloor>A\<rfloor> \<Rightarrow> A \<subseteq> B)"
 
 lemmas hyperset_defs =
  hyperUn_def hyperInt_def hyperDiff1_def hyper_isin_def hyper_subset_def
 
 lemma [simp]: "\<lfloor>{}\<rfloor> \<squnion> A = A  \<and>  A \<squnion> \<lfloor>{}\<rfloor> = A"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma [simp]: "\<lfloor>A\<rfloor> \<squnion> \<lfloor>B\<rfloor> = \<lfloor>A \<union> B\<rfloor> \<and> \<lfloor>A\<rfloor> \<ominus> a = \<lfloor>A - {a}\<rfloor>"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma [simp]: "None \<squnion> A = None \<and> A \<squnion> None = None"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma [simp]: "a \<in>\<in> None \<and> None \<ominus> a = None"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma hyper_isin_union: "x \<in>\<in> \<lfloor>A\<rfloor> \<Longrightarrow> x \<in>\<in> \<lfloor>A\<rfloor> \<squnion> B"
  by(case_tac B, auto simp: hyper_isin_def)
 
 lemma hyperUn_assoc: "(A \<squnion> B) \<squnion> C = A \<squnion> (B \<squnion> C)"
 (*<*)by(simp add:hyperset_defs Un_assoc)(*>*)
 
 lemma hyper_insert_comm: "A \<squnion> \<lfloor>{a}\<rfloor> = \<lfloor>{a}\<rfloor> \<squnion> A \<and> A \<squnion> (\<lfloor>{a}\<rfloor> \<squnion> B) = \<lfloor>{a}\<rfloor> \<squnion> (A \<squnion> B)"
 (*<*)by(simp add:hyperset_defs)(*>*)
 
 lemma hyper_comm: "A \<squnion> B = B \<squnion> A \<and> A \<squnion> B \<squnion> C = B \<squnion> A \<squnion> C"
-apply(case_tac A, simp, case_tac B, simp)
-apply(case_tac C, simp add: Un_commute)
-apply(simp add: Un_left_commute Un_commute)
-done
+(*<*)
+proof(cases A)
+  case SomeA: Some then show ?thesis
+  proof(cases B)
+    case SomeB: Some with SomeA show ?thesis
+    proof(cases C)
+      case SomeC: Some with SomeA SomeB show ?thesis
+        by(simp add: Un_left_commute Un_commute)
+    qed (simp add: Un_commute)
+  qed simp
+qed simp
+(*>*)
 
 subsection "Definite assignment"
 
 primrec
   \<A>  :: "'a exp \<Rightarrow> 'a hyperset"
   and \<A>s :: "'a exp list \<Rightarrow> 'a hyperset"
 where
   "\<A> (new C) = \<lfloor>{}\<rfloor>"
 | "\<A> (Cast C e) = \<A> e"
 | "\<A> (Val v) = \<lfloor>{}\<rfloor>"
 | "\<A> (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = \<A> e\<^sub>1 \<squnion> \<A> e\<^sub>2"
 | "\<A> (Var V) = \<lfloor>{}\<rfloor>"
 | "\<A> (LAss V e) = \<lfloor>{V}\<rfloor> \<squnion> \<A> e"
 | "\<A> (e\<bullet>F{D}) = \<A> e"
 | "\<A> (C\<bullet>\<^sub>sF{D}) = \<lfloor>{}\<rfloor>"
 | "\<A> (e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = \<A> e\<^sub>1 \<squnion> \<A> e\<^sub>2"
 | "\<A> (C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = \<A> e\<^sub>2"
 | "\<A> (e\<bullet>M(es)) = \<A> e \<squnion> \<A>s es"
 | "\<A> (C\<bullet>\<^sub>sM(es)) = \<A>s es"
 | "\<A> ({V:T; e}) = \<A> e \<ominus> V"
 | "\<A> (e\<^sub>1;;e\<^sub>2) = \<A> e\<^sub>1 \<squnion> \<A> e\<^sub>2"
 | "\<A> (if (e) e\<^sub>1 else e\<^sub>2) =  \<A> e \<squnion> (\<A> e\<^sub>1 \<sqinter> \<A> e\<^sub>2)"
 | "\<A> (while (b) e) = \<A> b"
 | "\<A> (throw e) = None"
 | "\<A> (try e\<^sub>1 catch(C V) e\<^sub>2) = \<A> e\<^sub>1 \<sqinter> (\<A> e\<^sub>2 \<ominus> V)"
 | "\<A> (INIT C (Cs,b) \<leftarrow> e) = \<lfloor>{}\<rfloor>"
 | "\<A> (RI (C,e);Cs \<leftarrow> e') = \<A> e"
 
 | "\<A>s ([]) = \<lfloor>{}\<rfloor>"
 | "\<A>s (e#es) = \<A> e \<squnion> \<A>s es"
 
 primrec
   \<D>  :: "'a exp \<Rightarrow> 'a hyperset \<Rightarrow> bool"
   and \<D>s :: "'a exp list \<Rightarrow> 'a hyperset \<Rightarrow> bool"
 where
   "\<D> (new C) A = True"
 | "\<D> (Cast C e) A = \<D> e A"
 | "\<D> (Val v) A = True"
 | "\<D> (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e\<^sub>1))"
 | "\<D> (Var V) A = (V \<in>\<in> A)"
 | "\<D> (LAss V e) A = \<D> e A"
 | "\<D> (e\<bullet>F{D}) A = \<D> e A"
 | "\<D> (C\<bullet>\<^sub>sF{D}) A = True"
 | "\<D> (e\<^sub>1\<bullet>F{D}:=e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e\<^sub>1))"
 | "\<D> (C\<bullet>\<^sub>sF{D}:=e\<^sub>2) A = \<D> e\<^sub>2 A"
 | "\<D> (e\<bullet>M(es)) A = (\<D> e A \<and> \<D>s es (A \<squnion> \<A> e))"
 | "\<D> (C\<bullet>\<^sub>sM(es)) A = \<D>s es A"
 | "\<D> ({V:T; e}) A = \<D> e (A \<ominus> V)"
 | "\<D> (e\<^sub>1;;e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e\<^sub>1))"
 | "\<D> (if (e) e\<^sub>1 else e\<^sub>2) A =
   (\<D> e A \<and> \<D> e\<^sub>1 (A \<squnion> \<A> e) \<and> \<D> e\<^sub>2 (A \<squnion> \<A> e))"
 | "\<D> (while (e) c) A = (\<D> e A \<and> \<D> c (A \<squnion> \<A> e))"
 | "\<D> (throw e) A = \<D> e A"
 | "\<D> (try e\<^sub>1 catch(C V) e\<^sub>2) A = (\<D> e\<^sub>1 A \<and> \<D> e\<^sub>2 (A \<squnion> \<lfloor>{V}\<rfloor>))"
 | "\<D> (INIT C (Cs,b) \<leftarrow> e) A = \<D> e A"
 | "\<D> (RI (C,e);Cs \<leftarrow> e') A = (\<D> e A \<and> \<D> e' A)"
 
 | "\<D>s ([]) A = True"
 | "\<D>s (e#es) A = (\<D> e A \<and> \<D>s es (A \<squnion> \<A> e))"
 
 lemma As_map_Val[simp]: "\<A>s (map Val vs) = \<lfloor>{}\<rfloor>"
 (*<*)by (induct vs) simp_all(*>*)
 
 lemma D_append[iff]: "\<And>A. \<D>s (es @ es') A = (\<D>s es A \<and> \<D>s es' (A \<squnion> \<A>s es))"
 (*<*)by (induct es type:list) (auto simp:hyperUn_assoc)(*>*)
 
 
 lemma A_fv: "\<And>A. \<A> e = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> fv e"
 and  "\<And>A. \<A>s es = \<lfloor>A\<rfloor> \<Longrightarrow> A \<subseteq> fvs es"
 (*<*)
-apply(induct e and es rule: \<A>.induct \<A>s.induct)
-apply (simp_all add:hyperset_defs)
-apply blast+
-done
+by (induct e and es rule: \<A>.induct \<A>s.induct)
+   (fastforce simp add:hyperset_defs)+
 (*>*)
 
 
 lemma sqUn_lem: "A \<sqsubseteq> A' \<Longrightarrow> A \<squnion> B \<sqsubseteq> A' \<squnion> B"
 (*<*)by(simp add:hyperset_defs) blast(*>*)
 
 lemma diff_lem: "A \<sqsubseteq> A' \<Longrightarrow> A \<ominus> b \<sqsubseteq> A' \<ominus> b"
 (*<*)by(simp add:hyperset_defs) blast(*>*)
 
 (* This order of the premises avoids looping of the simplifier *)
 lemma D_mono: "\<And>A A'. A \<sqsubseteq> A' \<Longrightarrow> \<D> e A \<Longrightarrow> \<D> (e::'a exp) A'"
 and Ds_mono: "\<And>A A'. A \<sqsubseteq> A' \<Longrightarrow> \<D>s es A \<Longrightarrow> \<D>s (es::'a exp list) A'"
 (*<*)
-apply(induct e and es rule: \<D>.induct \<D>s.induct)
-apply simp
-apply simp
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-apply (fastforce simp add:hyperset_defs)
-apply simp
-apply simp
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-apply simp
-apply simp apply (iprover dest:diff_lem)
-apply simp apply (iprover dest:sqUn_lem)
-apply simp apply (iprover dest:sqUn_lem)
-apply simp apply (iprover dest:sqUn_lem)
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-apply simp
-apply simp
-apply simp
-apply simp apply (iprover dest:sqUn_lem)
-done
+proof(induct e and es rule: \<D>.induct \<D>s.induct)
+  case BinOp then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Var then show ?case by (fastforce simp add:hyperset_defs)
+next
+  case FAss then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Call then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Block then show ?case by simp (iprover dest:diff_lem)
+next
+  case Seq then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Cond then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case While then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case TryCatch then show ?case by simp (iprover dest:sqUn_lem)
+next
+  case Cons_exp then show ?case by simp (iprover dest:sqUn_lem)
+qed simp_all
 (*>*)
 
 (* And this is the order of premises preferred during application: *)
 lemma D_mono': "\<D> e A \<Longrightarrow> A \<sqsubseteq> A' \<Longrightarrow> \<D> e A'"
 and Ds_mono': "\<D>s es A \<Longrightarrow> A \<sqsubseteq> A' \<Longrightarrow> \<D>s es A'"
 (*<*)by(blast intro:D_mono, blast intro:Ds_mono)(*>*)
 
 
 lemma Ds_Vals: "\<D>s (map Val vs) A" by(induct vs, auto)
 
 end
diff --git a/thys/JinjaDCI/J/EConform.thy b/thys/JinjaDCI/J/EConform.thy
--- a/thys/JinjaDCI/J/EConform.thy
+++ b/thys/JinjaDCI/J/EConform.thy
@@ -1,350 +1,337 @@
 (*  Title:      JinjaDCI/J/EConform.thy
     Author:     Susannah Mansky
     2019-20 UIUC
 *)
 
 section \<open> Expression conformance properties \<close>
 
 theory EConform
 imports SmallStep BigStep
 begin
 
 lemma cons_to_append: "list \<noteq> [] \<longrightarrow> (\<exists>ls. a # list = ls @ [last list])"
  by (metis append_butlast_last_id last_ConsR list.simps(3))
 
 subsection "Initialization conformance"
 
 \<comment> \<open> returns class that can be initialized (if any) by top-level expression \<close>
 fun init_class :: "'m prog \<Rightarrow> 'a exp \<Rightarrow> cname option" where
 "init_class P (new C) = Some C" |
 "init_class P (C\<bullet>\<^sub>sF{D}) = Some D" |
 "init_class P (C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = Some D" |
 "init_class P (C\<bullet>\<^sub>sM(es)) = seeing_class P C M" |
 "init_class _ _ = None"
 
 lemma icheck_init_class: "icheck P C e \<Longrightarrow> init_class P e = \<lfloor>C\<rfloor>"
-apply(induct e, auto) apply(rename_tac x1 x2 x3 x4)
-apply(case_tac x4, auto)
-done
+proof(induct e)
+  case (SFAss x1 x2 x3 e')
+  then show ?case by(case_tac e') auto
+qed auto
 
 \<comment> \<open> exp to take next small step (in particular, subexp that may contain initialization) \<close>
 fun ss_exp :: "'a exp \<Rightarrow> 'a exp" and ss_exps :: "'a exp list \<Rightarrow> 'a exp option" where
   "ss_exp (new C) = new C"
 | "ss_exp (Cast C e) = (case val_of e of Some v \<Rightarrow> Cast C e | _ \<Rightarrow> ss_exp e)"
 | "ss_exp (Val v) = Val v"
 | "ss_exp (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = (case val_of e\<^sub>1 of Some v \<Rightarrow> (case val_of e\<^sub>2 of Some v \<Rightarrow> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 | _ \<Rightarrow> ss_exp e\<^sub>2)
                                     | _ \<Rightarrow> ss_exp e\<^sub>1)"
 | "ss_exp (Var V) = Var V"
 | "ss_exp (LAss V e) = (case val_of e of Some v \<Rightarrow> LAss V e | _ \<Rightarrow> ss_exp e)"
 | "ss_exp (e\<bullet>F{D}) = (case val_of e of Some v \<Rightarrow> e\<bullet>F{D} | _ \<Rightarrow> ss_exp e)"
 | "ss_exp (C\<bullet>\<^sub>sF{D}) = C\<bullet>\<^sub>sF{D}"
 | "ss_exp (e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = (case val_of e\<^sub>1 of Some v \<Rightarrow> (case val_of e\<^sub>2 of Some v \<Rightarrow> e\<^sub>1\<bullet>F{D}:=e\<^sub>2 | _ \<Rightarrow> ss_exp e\<^sub>2)
                                     | _ \<Rightarrow> ss_exp e\<^sub>1)"
 | "ss_exp (C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = (case val_of e\<^sub>2 of Some v \<Rightarrow> C\<bullet>\<^sub>sF{D}:=e\<^sub>2 | _ \<Rightarrow> ss_exp e\<^sub>2)"
 | "ss_exp (e\<bullet>M(es)) = (case val_of e of Some v \<Rightarrow> (case map_vals_of es of Some t \<Rightarrow> e\<bullet>M(es) | _ \<Rightarrow> the(ss_exps es))
                                     | _ \<Rightarrow> ss_exp e)"
 | "ss_exp (C\<bullet>\<^sub>sM(es)) = (case map_vals_of es of Some t \<Rightarrow> C\<bullet>\<^sub>sM(es) | _ \<Rightarrow> the(ss_exps es))"
 | "ss_exp ({V:T; e}) = ss_exp e"
 | "ss_exp (e\<^sub>1;;e\<^sub>2) = (case val_of e\<^sub>1 of Some v \<Rightarrow> ss_exp e\<^sub>2
            | None \<Rightarrow> (case lass_val_of e\<^sub>1 of Some p \<Rightarrow> ss_exp e\<^sub>2
                                            | None \<Rightarrow> ss_exp e\<^sub>1))"
 | "ss_exp (if (b) e\<^sub>1 else e\<^sub>2) = (case bool_of b of Some True \<Rightarrow> if (b) e\<^sub>1 else e\<^sub>2
                                         | Some False \<Rightarrow> if (b) e\<^sub>1 else e\<^sub>2
                                         | _ \<Rightarrow> ss_exp b)"
 | "ss_exp (while (b) e) = while (b) e"
 | "ss_exp (throw e) = (case val_of e of Some v \<Rightarrow> throw e | _ \<Rightarrow> ss_exp e)"
 | "ss_exp (try e\<^sub>1 catch(C V) e\<^sub>2) = (case val_of e\<^sub>1 of Some v \<Rightarrow> try e\<^sub>1 catch(C V) e\<^sub>2
                                             | _ \<Rightarrow> ss_exp e\<^sub>1)"
 | "ss_exp (INIT C (Cs,b) \<leftarrow> e) = INIT C (Cs,b) \<leftarrow> e"
 | "ss_exp (RI (C,e);Cs \<leftarrow> e') = (case val_of e of Some v \<Rightarrow> RI (C,e);Cs \<leftarrow> e | _ \<Rightarrow> ss_exp e)"
 | "ss_exps([]) = None"
 | "ss_exps(e#es) = (case val_of e of Some v \<Rightarrow> ss_exps es | _ \<Rightarrow> Some (ss_exp e))"
 
 (*<*)
 lemmas ss_exp_ss_exps_induct = ss_exp_ss_exps.induct
  [ case_names New Cast Val BinOp Var LAss FAcc SFAcc FAss SFAss Call SCall
   Block Seq Cond While Throw Try Init RI Nil Cons ]
 (*>*)
 
 lemma icheck_ss_exp:
 assumes "icheck P C e" shows "ss_exp e = e"
 using assms
 proof(cases e)
   case (SFAss C F D e) then show ?thesis using assms
   proof(cases e)qed(auto)
 qed(auto)
 
 lemma ss_exps_Vals_None[simp]:
  "ss_exps (map Val vs) = None"
- by(induct vs, auto)
+ by(induct vs) (auto)
 
 lemma ss_exps_Vals_NoneI:
  "ss_exps es = None \<Longrightarrow> \<exists>vs. es = map Val vs"
-using val_of_spec by(induct es, auto)
+using val_of_spec by(induct es) (auto)
 
 lemma ss_exps_throw_nVal:
  "\<lbrakk> val_of e = None; ss_exps (map Val vs @ throw e # es') = \<lfloor>e'\<rfloor> \<rbrakk>
    \<Longrightarrow> e' = ss_exp e"
- by(induct vs, auto)
+ by(induct vs) (auto)
 
 lemma ss_exps_throw_Val:
  "\<lbrakk> val_of e = \<lfloor>a\<rfloor>; ss_exps (map Val vs @ throw e # es') = \<lfloor>e'\<rfloor> \<rbrakk>
    \<Longrightarrow> e' = throw e"
- by(induct vs, auto)
+ by(induct vs) (auto)
 
 
 abbreviation curr_init :: "'m prog \<Rightarrow> 'a exp \<Rightarrow> cname option" where
 "curr_init P e \<equiv> init_class P (ss_exp e)"
 abbreviation curr_inits :: "'m prog \<Rightarrow> 'a exp list \<Rightarrow> cname option" where
 "curr_inits P es \<equiv> case ss_exps es of Some e \<Rightarrow> init_class P e | _ \<Rightarrow> None"
 
 lemma icheck_curr_init': "\<And>e'. ss_exp e = e' \<Longrightarrow> icheck P C e' \<Longrightarrow> curr_init P e = \<lfloor>C\<rfloor>"
  and icheck_curr_inits': "\<And>e. ss_exps es = \<lfloor>e\<rfloor> \<Longrightarrow> icheck P C e \<Longrightarrow> curr_inits P es = \<lfloor>C\<rfloor>"
 proof(induct rule: ss_exp_ss_exps_induct)
 qed(simp_all add: icheck_init_class)
 
 lemma icheck_curr_init: "icheck P C e' \<Longrightarrow> ss_exp e = e' \<Longrightarrow> curr_init P e = \<lfloor>C\<rfloor>"
  by(rule icheck_curr_init')
 
 lemma icheck_curr_inits: "icheck P C e \<Longrightarrow> ss_exps es = \<lfloor>e\<rfloor> \<Longrightarrow> curr_inits P es = \<lfloor>C\<rfloor>"
  by(rule icheck_curr_inits')
 
 definition initPD :: "sheap \<Rightarrow> cname \<Rightarrow> bool" where
 "initPD sh C \<equiv> \<exists>sfs i. sh C = Some (sfs, i) \<and> (i = Done \<or> i = Processing)"
 
 \<comment> \<open> checks that @{text INIT} and @{text RI} conform and are only in the main computation \<close>
 fun iconf :: "sheap \<Rightarrow> 'a exp \<Rightarrow> bool" and iconfs :: " sheap \<Rightarrow> 'a exp list \<Rightarrow> bool" where
   "iconf sh (new C) = True"
 | "iconf sh (Cast C e) = iconf sh e"
 | "iconf sh (Val v) = True"
 | "iconf sh (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = (case val_of e\<^sub>1 of Some v \<Rightarrow> iconf sh e\<^sub>2 | _ \<Rightarrow> iconf sh e\<^sub>1 \<and> \<not>sub_RI e\<^sub>2)"
 | "iconf sh (Var V) = True"
 | "iconf sh (LAss V e) = iconf sh e"
 | "iconf sh (e\<bullet>F{D}) = iconf sh e"
 | "iconf sh (C\<bullet>\<^sub>sF{D}) = True"
 | "iconf sh (e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = (case val_of e\<^sub>1 of Some v \<Rightarrow> iconf sh e\<^sub>2 | _ \<Rightarrow> iconf sh e\<^sub>1 \<and> \<not>sub_RI e\<^sub>2)"
 | "iconf sh (C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = iconf sh e\<^sub>2"
 | "iconf sh (e\<bullet>M(es)) = (case val_of e of Some v \<Rightarrow> iconfs sh es | _ \<Rightarrow> iconf sh e \<and> \<not>sub_RIs es)"
 | "iconf sh (C\<bullet>\<^sub>sM(es)) = iconfs sh es"
 | "iconf sh ({V:T; e}) = iconf sh e"
 | "iconf sh (e\<^sub>1;;e\<^sub>2) = (case val_of e\<^sub>1 of Some v \<Rightarrow> iconf sh e\<^sub>2
            | None \<Rightarrow> (case lass_val_of e\<^sub>1 of Some p \<Rightarrow> iconf sh e\<^sub>2
                                            | None \<Rightarrow> iconf sh e\<^sub>1 \<and> \<not>sub_RI e\<^sub>2))"
 | "iconf sh (if (b) e\<^sub>1 else e\<^sub>2) = (iconf sh b \<and> \<not>sub_RI e\<^sub>1 \<and> \<not>sub_RI e\<^sub>2)"
 | "iconf sh (while (b) e) = (\<not>sub_RI b \<and> \<not>sub_RI e)"
 | "iconf sh (throw e) = iconf sh e"
 | "iconf sh (try e\<^sub>1 catch(C V) e\<^sub>2) = (iconf sh e\<^sub>1 \<and> \<not>sub_RI e\<^sub>2)"
 | "iconf sh (INIT C (Cs,b) \<leftarrow> e) = ((case Cs of Nil \<Rightarrow> initPD sh C | C'#Cs' \<Rightarrow> last Cs = C) \<and> \<not>sub_RI e)"
 | "iconf sh (RI (C,e);Cs \<leftarrow> e') = (iconf sh e \<and> \<not>sub_RI e')"
 | "iconfs sh ([]) = True"
 | "iconfs sh (e#es) = (case val_of e of Some v \<Rightarrow> iconfs sh es | _ \<Rightarrow> iconf sh e \<and> \<not>sub_RIs es)"
 
 lemma iconfs_map_throw: "iconfs sh (map Val vs @ throw e # es') \<Longrightarrow> iconf sh e"
  by(induct vs,auto)
 
 lemma nsub_RI_iconf_aux:
  "(\<not>sub_RI (e::'a exp) \<longrightarrow> (\<forall>e'. e' \<in> subexp e \<longrightarrow> \<not>sub_RI e' \<longrightarrow> iconf sh e') \<longrightarrow> iconf sh e)
  \<and> (\<not>sub_RIs (es::'a exp list) \<longrightarrow> (\<forall>e'. e' \<in> subexps es \<longrightarrow> \<not>sub_RI e' \<longrightarrow> iconf sh e') \<longrightarrow> iconfs sh es)"
 proof(induct rule: sub_RI_sub_RIs.induct) qed(auto)
 
 lemma nsub_RI_iconf_aux':
  "(\<And>e'. subexp_of e' e \<Longrightarrow> \<not>sub_RI e' \<longrightarrow> iconf sh e') \<Longrightarrow> (\<not>sub_RI e \<Longrightarrow> iconf sh e)"
  by(simp add: nsub_RI_iconf_aux)
 
 lemma nsub_RI_iconf: "\<not>sub_RI e \<Longrightarrow> iconf sh e"
-apply(cut_tac e = e and R = "\<lambda>e. \<not>sub_RI e \<longrightarrow> iconf sh e" in subexp_induct)
-   apply(rename_tac ea) apply(case_tac ea, simp_all)
-apply(clarsimp simp: nsub_RI_iconf_aux)
-done
-
-lemma nsub_RIs_iconfs: "\<not>sub_RIs es \<Longrightarrow> iconfs sh es"
-apply(cut_tac es = es and R = "\<lambda>e. \<not>sub_RI e \<longrightarrow> iconf sh e"
-  and Rs = "\<lambda>es. \<not>sub_RIs es \<longrightarrow> iconfs sh es" in subexps_induct)
-   apply(rename_tac esa) apply(case_tac esa, simp_all)
- apply(clarsimp simp: nsub_RI_iconf_aux)+
-done
+  and nsub_RIs_iconfs: "\<not>sub_RIs es \<Longrightarrow> iconfs sh es"
+proof -
+  let ?R = "\<lambda>e. \<not>sub_RI e \<longrightarrow> iconf sh e"
+  let ?Rs = "\<lambda>es. \<not>sub_RIs es \<longrightarrow> iconfs sh es"
+  have "(\<forall>e'. subexp_of e' e \<longrightarrow> ?R e') \<and> ?R e"
+   and "(\<forall>e'. e' \<in> subexps es \<longrightarrow> ?R e') \<and> ?Rs es"
+    by(rule subexp_induct[where ?Rs = ?Rs]; clarsimp simp: nsub_RI_iconf_aux)
+      (rule subexps_induct; clarsimp simp: nsub_RI_iconf_aux)
+  then show "\<not>sub_RI e \<Longrightarrow> iconf sh e"
+        and "\<not>sub_RIs es \<Longrightarrow> iconfs sh es" by simp+
+qed
 
 lemma lass_val_of_iconf: "lass_val_of e = \<lfloor>a\<rfloor> \<Longrightarrow> iconf sh e"
  by(drule lass_val_of_nsub_RI, erule nsub_RI_iconf)
 
 lemma icheck_iconf:
 assumes "icheck P C e" shows "iconf sh e"
 using assms
 proof(cases e)
   case (SFAss C F D e) then show ?thesis using assms
   proof(cases e)qed(auto)
 next
   case (SCall C M es) then show ?thesis using assms
     by (auto simp: nsub_RIs_iconfs)
 next
 qed(auto)
 
 
 subsection "Indicator boolean conformance"
 
 \<comment> \<open> checks that the given expression, indicator boolean pair is allowed in small-step
   (i.e., if @{term b} is True, then @{term e} is an initialization-calling expression to
   a class that is marked either @{term Processing} or @{term Done}) \<close>
 definition bconf :: "'m prog \<Rightarrow> sheap \<Rightarrow> 'a exp \<Rightarrow> bool \<Rightarrow> bool"  ("_,_ \<turnstile>\<^sub>b '(_,_') \<surd>" [51,51,0,0] 50)
 where
   "P,sh \<turnstile>\<^sub>b (e,b) \<surd>  \<equiv> b \<longrightarrow> (\<exists>C. icheck P C (ss_exp e) \<and> initPD sh C)"
 
 definition bconfs :: "'m prog \<Rightarrow> sheap \<Rightarrow> 'a exp list \<Rightarrow> bool \<Rightarrow> bool"  ("_,_ \<turnstile>\<^sub>b '(_,_') \<surd>" [51,51,0,0] 50)
 where
   "P,sh \<turnstile>\<^sub>b (es,b) \<surd>  \<equiv> b \<longrightarrow> (\<exists>C. (icheck P C (the(ss_exps es))
                            \<and> (curr_inits P es = Some C) \<and> initPD sh C))"
 
 
 \<comment> \<open> bconf helper lemmas \<close>
 
 lemma bconf_nonVal[simp]:
  "P,sh \<turnstile>\<^sub>b (e,True) \<surd> \<Longrightarrow> val_of e = None"
- by(cases e, auto simp: bconf_def)
+ by(cases e) (auto simp: bconf_def)
 
 lemma bconfs_nonVals[simp]:
  "P,sh \<turnstile>\<^sub>b (es,True) \<surd> \<Longrightarrow> map_vals_of es = None"
- by(induct es, auto simp: bconfs_def)
+ by(induct es) (auto simp: bconfs_def)
 
 lemma bconf_Cast[iff]:
  "P,sh \<turnstile>\<^sub>b (Cast C e,b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconf_BinOp[iff]:
  "P,sh \<turnstile>\<^sub>b (e1 \<guillemotleft>bop\<guillemotright> e2,b) \<surd>
    \<longleftrightarrow> (case val_of e1 of Some v \<Rightarrow> P,sh \<turnstile>\<^sub>b (e2,b) \<surd> | _ \<Rightarrow> P,sh \<turnstile>\<^sub>b (e1,b) \<surd>)"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconf_LAss[iff]:
  "P,sh \<turnstile>\<^sub>b (LAss V e,b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconf_FAcc[iff]:
  "P,sh \<turnstile>\<^sub>b (e\<bullet>F{D},b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconf_FAss[iff]:
  "P,sh \<turnstile>\<^sub>b (FAss e1 F D e2,b) \<surd>
    \<longleftrightarrow> (case val_of e1 of Some v \<Rightarrow> P,sh \<turnstile>\<^sub>b (e2,b) \<surd> | _ \<Rightarrow> P,sh \<turnstile>\<^sub>b (e1,b) \<surd>)"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconf_SFAss[iff]:
 "val_of e2 = None \<Longrightarrow> P,sh \<turnstile>\<^sub>b (SFAss C F D e2,b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e2,b) \<surd>"
- by(unfold bconf_def, cases b, auto)
+ by(cases b) (auto simp: bconf_def)
 
 lemma bconfs_Vals[iff]:
  "P,sh \<turnstile>\<^sub>b (map Val vs, b) \<surd> \<longleftrightarrow> \<not> b"
- by(unfold bconfs_def, simp)
+ by(unfold bconfs_def) simp
 
 lemma bconf_Call[iff]:
  "P,sh \<turnstile>\<^sub>b (e\<bullet>M(es),b) \<surd>
    \<longleftrightarrow> (case val_of e of Some v \<Rightarrow> P,sh \<turnstile>\<^sub>b (es,b) \<surd> | _ \<Rightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>)"
 proof(cases b)
   case True
   then show ?thesis
   proof(cases "ss_exps es")
     case None
     then obtain vs where "es = map Val vs" using ss_exps_Vals_NoneI by auto
     then have mv: "map_vals_of es = \<lfloor>vs\<rfloor>" by simp
     then show ?thesis by(auto simp: bconf_def) (simp add: bconfs_def)
   next
     case (Some a)
-    then show ?thesis by(auto simp: bconf_def, auto simp: bconfs_def icheck_init_class)
+    then show ?thesis by(auto simp: bconf_def) (auto simp: bconfs_def icheck_init_class)
   qed
 qed(simp add: bconf_def bconfs_def)
 
 lemma bconf_SCall[iff]:
 assumes mvn: "map_vals_of es = None"
 shows "P,sh \<turnstile>\<^sub>b (C\<bullet>\<^sub>sM(es),b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (es,b) \<surd>"
 proof(cases b)
   case True
   then show ?thesis
   proof(cases "ss_exps es")
     case None
       then have "\<exists>vs. es = map Val vs" using ss_exps_Vals_NoneI by auto
       then show ?thesis using mvn finals_def by clarsimp
     next
     case (Some a)
-      then show ?thesis by(auto simp: bconf_def, auto simp: bconfs_def icheck_init_class)
+      then show ?thesis by(auto simp: bconf_def) (auto simp: bconfs_def icheck_init_class)
     qed
 qed(simp add: bconf_def bconfs_def)
 
 lemma bconf_Cons[iff]:
  "P,sh \<turnstile>\<^sub>b (e#es,b) \<surd>
    \<longleftrightarrow> (case val_of e of Some v \<Rightarrow> P,sh \<turnstile>\<^sub>b (es,b) \<surd> | _ \<Rightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>)"
 proof(cases b)
   case True
   then show ?thesis
   proof(cases "ss_exps es")
     case None
       then have "\<exists>vs. es = map Val vs" using ss_exps_Vals_NoneI by auto
       then show ?thesis using None by(auto simp: bconf_def bconfs_def icheck_init_class)
     next
     case (Some a)
       then show ?thesis by(auto simp: bconf_def bconfs_def icheck_init_class)
     qed
 qed(simp add: bconf_def bconfs_def)
 
 lemma bconf_InitBlock[iff]:
  "P,sh \<turnstile>\<^sub>b ({V:T; V:=Val v;; e\<^sub>2},b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e\<^sub>2,b) \<surd>"
- by(unfold bconf_def, cases b, auto simp: assigned_def)
+ by(cases b) (auto simp: bconf_def assigned_def)
 
 lemma bconf_Block[iff]:
  "P,sh \<turnstile>\<^sub>b ({V:T; e},b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>"
- by(unfold bconf_def, cases b, auto)
+ by(cases b) (auto simp: bconf_def)
 
 lemma bconf_Seq[iff]:
  "P,sh \<turnstile>\<^sub>b (e1;;e2,b) \<surd>
    \<longleftrightarrow> (case val_of e1 of Some v \<Rightarrow> P,sh \<turnstile>\<^sub>b (e2,b) \<surd>
                              | _ \<Rightarrow> (case lass_val_of e1 of Some p \<Rightarrow> P,sh \<turnstile>\<^sub>b (e2,b) \<surd>
-                                                          | None \<Rightarrow> P,sh \<turnstile>\<^sub>b (e1,b) \<surd>))" (* \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e1,b) \<surd>"*)
-by(unfold bconf_def, cases b, auto dest: val_of_spec lass_val_of_spec)
+                                                          | None \<Rightarrow> P,sh \<turnstile>\<^sub>b (e1,b) \<surd>))"
+ by(cases b) (auto simp: bconf_def dest: val_of_spec lass_val_of_spec)
 
 lemma bconf_Cond[iff]:
  "P,sh \<turnstile>\<^sub>b (if (b) e\<^sub>1 else e\<^sub>2,b') \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (b,b') \<surd>"
-apply(unfold bconf_def, cases "bool_of b") apply auto[1]
-apply(rename_tac a) apply(case_tac a)
- apply(simp, drule bool_of_specT) apply auto[1]
-apply(simp, drule bool_of_specF) apply auto[1]
-done
+proof(cases "bool_of b")
+  case None
+  then show ?thesis by(auto simp: bconf_def)
+next
+  case (Some a)
+  then show ?thesis by(case_tac a) (auto simp: bconf_def dest: bool_of_specT bool_of_specF)
+qed
 
 lemma bconf_While[iff]:
  "P,sh \<turnstile>\<^sub>b (while (b) e,b') \<surd> \<longleftrightarrow> \<not>b'"
- by(unfold bconf_def, cases b, auto)
+ by(cases b) (auto simp: bconf_def)
 
 lemma bconf_Throw[iff]:
  "P,sh \<turnstile>\<^sub>b (throw e,b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconf_Try[iff]:
  "P,sh \<turnstile>\<^sub>b (try e\<^sub>1 catch(C V) e\<^sub>2,b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e\<^sub>1,b) \<surd>"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconf_INIT[iff]:
  "P,sh \<turnstile>\<^sub>b (INIT C (Cs,b') \<leftarrow> e,b) \<surd> \<longleftrightarrow> \<not>b"
- by(unfold bconf_def, cases b, auto)
+ by(cases b) (auto simp: bconf_def)
 
 lemma bconf_RI[iff]:
  "P,sh \<turnstile>\<^sub>b (RI(C,e);Cs \<leftarrow> e',b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>"
-apply(unfold bconf_def, cases b, auto)
-apply(drule val_of_spec, simp)
-done
+ by(cases b) (auto simp: bconf_def dest: val_of_spec)
 
 lemma bconfs_map_throw[iff]:
  "P,sh \<turnstile>\<^sub>b (map Val vs @ throw e # es',b) \<surd> \<longleftrightarrow> P,sh \<turnstile>\<^sub>b (e,b) \<surd>"
- by(induct vs, auto)
+ by(induct vs) auto
 
 end
diff --git a/thys/JinjaDCI/J/JWellForm.thy b/thys/JinjaDCI/J/JWellForm.thy
--- a/thys/JinjaDCI/J/JWellForm.thy
+++ b/thys/JinjaDCI/J/JWellForm.thy
@@ -1,82 +1,73 @@
 (*  Title:      JinjaDCI/J/JWellForm.thy
 
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/JWellForm.thy by Tobias Nipkow
 *)
 
 section \<open> Well-formedness Constraints \<close>
 
 theory JWellForm
 imports "../Common/WellForm" WWellForm WellType DefAss
 begin
 
 definition wf_J_mdecl :: "J_prog \<Rightarrow> cname \<Rightarrow> J_mb mdecl \<Rightarrow> bool"
 where
   "wf_J_mdecl P C  \<equiv>  \<lambda>(M,b,Ts,T,(pns,body)).
   length Ts = length pns \<and>
   distinct pns \<and>
   \<not>sub_RI body \<and>
  (case b of
     NonStatic \<Rightarrow> this \<notin> set pns \<and>
         (\<exists>T'. P,[this\<mapsto>Class C,pns[\<mapsto>]Ts] \<turnstile> body :: T' \<and> P \<turnstile> T' \<le> T) \<and>
         \<D> body \<lfloor>{this} \<union> set pns\<rfloor>
   | Static \<Rightarrow> (\<exists>T'. P,[pns[\<mapsto>]Ts] \<turnstile> body :: T' \<and> P \<turnstile> T' \<le> T) \<and>
         \<D> body \<lfloor>set pns\<rfloor>)"
 
 lemma wf_J_mdecl_NonStatic[simp]:
   "wf_J_mdecl P C (M,NonStatic,Ts,T,pns,body) \<equiv>
   (length Ts = length pns \<and>
   distinct pns \<and>
   \<not>sub_RI body \<and>
   this \<notin> set pns \<and>
   (\<exists>T'. P,[this\<mapsto>Class C,pns[\<mapsto>]Ts] \<turnstile> body :: T' \<and> P \<turnstile> T' \<le> T) \<and>
   \<D> body \<lfloor>{this} \<union> set pns\<rfloor>)"
 (*<*)by(simp add:wf_J_mdecl_def)(*>*)
 
 lemma wf_J_mdecl_Static[simp]:
   "wf_J_mdecl P C (M,Static,Ts,T,pns,body) \<equiv>
   (length Ts = length pns \<and>
   distinct pns \<and>
   \<not>sub_RI body \<and>
   (\<exists>T'. P,[pns[\<mapsto>]Ts] \<turnstile> body :: T' \<and> P \<turnstile> T' \<le> T) \<and>
   \<D> body \<lfloor>set pns\<rfloor>)"
 (*<*)by(simp add:wf_J_mdecl_def)(*>*)
 
 
 abbreviation
   wf_J_prog :: "J_prog \<Rightarrow> bool" where
   "wf_J_prog == wf_prog wf_J_mdecl"
 
 lemma wf_J_prog_wf_J_mdecl:
   "\<lbrakk> wf_J_prog P; (C, D, fds, mths) \<in> set P; jmdcl \<in> set mths \<rbrakk>
   \<Longrightarrow> wf_J_mdecl P C jmdcl"
-(*<*)
-apply (simp add: wf_prog_def)
-apply (simp add: wf_cdecl_def)
-apply (erule conjE)+
-apply (drule bspec, assumption)
-apply simp
-apply (erule conjE)+
-apply (drule bspec, assumption)
-apply (simp add: wf_mdecl_def split_beta)
-done
-(*>*)
+(*<*)by(fastforce simp: wf_prog_def wf_cdecl_def wf_mdecl_def)(*>*)
                                   
 lemma wf_mdecl_wwf_mdecl: "wf_J_mdecl P C Md \<Longrightarrow> wwf_J_mdecl P C Md"
 (*<*)
-apply(clarsimp simp:wwf_J_mdecl_def) apply(rename_tac M b Ts T pns body)
-apply (case_tac b)
- by (fastforce dest!:WT_fv)+
+proof -
+  obtain M b Ts T pns body where "Md = (M, b, Ts, T, pns, body)" by(cases Md) simp
+  then show "wf_J_mdecl P C Md \<Longrightarrow> wwf_J_mdecl P C Md"
+    by(case_tac b) (fastforce simp:wwf_J_mdecl_def dest!:WT_fv)+
+qed
 (*>*)
 
 lemma wf_prog_wwf_prog: "wf_J_prog P \<Longrightarrow> wwf_J_prog P"
 (*<*)
-apply(simp add:wf_prog_def wf_cdecl_def wf_mdecl_def)
-apply(fast intro:wf_mdecl_wwf_mdecl)
-done
+by (simp add:wf_prog_def wf_cdecl_def wf_mdecl_def)
+   (fast intro:wf_mdecl_wwf_mdecl)
 (*>*)
 
 
 end
diff --git a/thys/JinjaDCI/J/Progress.thy b/thys/JinjaDCI/J/Progress.thy
--- a/thys/JinjaDCI/J/Progress.thy
+++ b/thys/JinjaDCI/J/Progress.thy
@@ -1,887 +1,880 @@
 (*  Title:      JinjaDCI/J/Progress.thy
 
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/Progress.thy by Tobias Nipkow
 *)
 
 section \<open> Progress of Small Step Semantics \<close>
 
 theory Progress
 imports WellTypeRT DefAss "../Common/Conform" EConform
 begin
 
 lemma final_addrE:
   "\<lbrakk> P,E,h,sh \<turnstile> e : Class C; final e;
     \<And>a. e = addr a \<Longrightarrow> R;
     \<And>a. e = Throw a \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
 (*<*)by(auto simp:final_def)(*>*)
 
 
 lemma finalRefE:
  "\<lbrakk> P,E,h,sh \<turnstile> e : T; is_refT T; final e;
    e = null \<Longrightarrow> R;
    \<And>a C. \<lbrakk> e = addr a; T = Class C \<rbrakk> \<Longrightarrow> R;
    \<And>a. e = Throw a \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
 (*<*)by(auto simp:final_def is_refT_def)(*>*)
 
 
 text\<open> Derivation of new induction scheme for well typing: \<close>
 
 inductive
   WTrt' :: "[J_prog,heap,sheap,env,expr,ty] \<Rightarrow> bool"
   and WTrts' :: "[J_prog,heap,sheap,env,expr list, ty list] \<Rightarrow> bool"
   and WTrt2' :: "[J_prog,env,heap,sheap,expr,ty] \<Rightarrow> bool"
         ("_,_,_,_ \<turnstile> _ :'' _"   [51,51,51,51]50)
   and WTrts2' :: "[J_prog,env,heap,sheap,expr list, ty list] \<Rightarrow> bool"
         ("_,_,_,_ \<turnstile> _ [:''] _" [51,51,51,51]50)
   for P :: J_prog and h :: heap and sh :: sheap
 where
   "P,E,h,sh \<turnstile> e :' T \<equiv> WTrt' P h sh E e T"
 | "P,E,h,sh \<turnstile> es [:'] Ts \<equiv> WTrts' P h sh E es Ts"
 
 | "is_class P C  \<Longrightarrow>  P,E,h,sh \<turnstile> new C :' Class C"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' T; is_refT T; is_class P C \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> Cast C e :' Class C"
 | "typeof\<^bsub>h\<^esub> v = Some T \<Longrightarrow> P,E,h,sh \<turnstile> Val v :' T"
 | "E v = Some T  \<Longrightarrow>  P,E,h,sh \<turnstile> Var v :' T"
 | "\<lbrakk> P,E,h,sh \<turnstile> e\<^sub>1 :' T\<^sub>1;  P,E,h,sh \<turnstile> e\<^sub>2 :' T\<^sub>2 \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> e\<^sub>1 \<guillemotleft>Eq\<guillemotright> e\<^sub>2 :' Boolean"
 | "\<lbrakk> P,E,h,sh \<turnstile> e\<^sub>1 :' Integer;  P,E,h,sh \<turnstile> e\<^sub>2 :' Integer \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> e\<^sub>1 \<guillemotleft>Add\<guillemotright> e\<^sub>2 :' Integer"
 | "\<lbrakk> P,E,h,sh \<turnstile> Var V :' T;  P,E,h,sh \<turnstile> e :' T';  P \<turnstile> T' \<le> T \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> V:=e :' Void"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' Class C; P \<turnstile> C has F,NonStatic:T in D \<rbrakk> \<Longrightarrow> P,E,h,sh \<turnstile> e\<bullet>F{D} :' T"
 | "P,E,h,sh \<turnstile> e :' NT \<Longrightarrow> P,E,h,sh \<turnstile> e\<bullet>F{D} :' T"
 | "\<lbrakk> P \<turnstile> C has F,Static:T in D \<rbrakk> \<Longrightarrow> P,E,h,sh \<turnstile> C\<bullet>\<^sub>sF{D} :' T"
 | "\<lbrakk> P,E,h,sh \<turnstile> e\<^sub>1 :' Class C;  P \<turnstile> C has F,NonStatic:T in D;
     P,E,h,sh \<turnstile> e\<^sub>2 :' T\<^sub>2;  P \<turnstile> T\<^sub>2 \<le> T \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> e\<^sub>1\<bullet>F{D}:=e\<^sub>2 :' Void"
 | "\<lbrakk> P,E,h,sh \<turnstile> e\<^sub>1:'NT; P,E,h,sh \<turnstile> e\<^sub>2 :' T\<^sub>2 \<rbrakk> \<Longrightarrow> P,E,h,sh \<turnstile> e\<^sub>1\<bullet>F{D}:=e\<^sub>2 :' Void"
 | "\<lbrakk> P \<turnstile> C has F,Static:T in D;
     P,E,h,sh \<turnstile> e\<^sub>2 :' T\<^sub>2;  P \<turnstile> T\<^sub>2 \<le> T \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> C\<bullet>\<^sub>sF{D}:=e\<^sub>2 :' Void"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' Class C; P \<turnstile> C sees M,NonStatic:Ts \<rightarrow> T = (pns,body) in D;
     P,E,h,sh \<turnstile> es [:'] Ts'; P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> e\<bullet>M(es) :' T"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' NT; P,E,h,sh \<turnstile> es [:'] Ts \<rbrakk> \<Longrightarrow> P,E,h,sh \<turnstile> e\<bullet>M(es) :' T"
 | "\<lbrakk> P \<turnstile> C sees M,Static:Ts \<rightarrow> T = (pns,body) in D;
     P,E,h,sh \<turnstile> es [:'] Ts'; P \<turnstile> Ts' [\<le>] Ts;
     M = clinit \<longrightarrow> sh D = \<lfloor>(sfs,Processing)\<rfloor> \<and> es = map Val vs \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> C\<bullet>\<^sub>sM(es) :' T"
 | "P,E,h,sh \<turnstile> [] [:'] []"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' T;  P,E,h,sh \<turnstile> es [:'] Ts \<rbrakk> \<Longrightarrow>  P,E,h,sh \<turnstile> e#es [:'] T#Ts"
 | "\<lbrakk> typeof\<^bsub>h\<^esub> v = Some T\<^sub>1; P \<turnstile> T\<^sub>1 \<le> T; P,E(V\<mapsto>T),h,sh \<turnstile> e\<^sub>2 :' T\<^sub>2 \<rbrakk>
   \<Longrightarrow>  P,E,h,sh \<turnstile> {V:T := Val v; e\<^sub>2} :' T\<^sub>2"
 | "\<lbrakk> P,E(V\<mapsto>T),h,sh \<turnstile> e :' T'; \<not> assigned V e \<rbrakk> \<Longrightarrow>  P,E,h,sh \<turnstile> {V:T; e} :' T'"
 | "\<lbrakk> P,E,h,sh \<turnstile> e\<^sub>1:' T\<^sub>1;  P,E,h,sh \<turnstile> e\<^sub>2:'T\<^sub>2 \<rbrakk>  \<Longrightarrow>  P,E,h,sh \<turnstile> e\<^sub>1;;e\<^sub>2 :' T\<^sub>2"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' Boolean;  P,E,h,sh \<turnstile> e\<^sub>1:' T\<^sub>1;  P,E,h,sh \<turnstile> e\<^sub>2:' T\<^sub>2;
     P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<or> P \<turnstile> T\<^sub>2 \<le> T\<^sub>1;
     P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<longrightarrow> T = T\<^sub>2; P \<turnstile> T\<^sub>2 \<le> T\<^sub>1 \<longrightarrow> T = T\<^sub>1 \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :' T"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' Boolean;  P,E,h,sh \<turnstile> c:' T \<rbrakk>
   \<Longrightarrow>  P,E,h,sh \<turnstile> while(e) c :' Void"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' T\<^sub>r; is_refT T\<^sub>r \<rbrakk>  \<Longrightarrow>  P,E,h,sh \<turnstile> throw e :' T"
 | "\<lbrakk> P,E,h,sh \<turnstile> e\<^sub>1 :' T\<^sub>1;  P,E(V \<mapsto> Class C),h,sh \<turnstile> e\<^sub>2 :' T\<^sub>2; P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 :' T\<^sub>2"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' T; \<forall>C' \<in> set (C#Cs). is_class P C'; \<not>sub_RI e;
      \<forall>C' \<in> set (tl Cs). \<exists>sfs. sh C' = \<lfloor>(sfs,Processing)\<rfloor>;
      b \<longrightarrow> (\<forall>C' \<in> set Cs. \<exists>sfs. sh C' = \<lfloor>(sfs,Processing)\<rfloor>);
      distinct Cs; supercls_lst P Cs \<rbrakk> \<Longrightarrow> P,E,h,sh \<turnstile> INIT C (Cs, b) \<leftarrow> e :' T"
 | "\<lbrakk> P,E,h,sh \<turnstile> e :' T; P,E,h,sh \<turnstile> e' :' T'; \<forall>C' \<in> set (C#Cs). is_class P C'; \<not>sub_RI e';
      \<forall>C' \<in> set (C#Cs). not_init C' e;
      \<forall>C' \<in> set Cs. \<exists>sfs. sh C' = \<lfloor>(sfs,Processing)\<rfloor>;
      \<exists>sfs. sh C = \<lfloor>(sfs, Processing)\<rfloor> \<or> (sh C = \<lfloor>(sfs, Error)\<rfloor> \<and> e = THROW NoClassDefFoundError);
      distinct (C#Cs); supercls_lst P (C#Cs) \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> RI(C, e);Cs \<leftarrow> e' :' T'"
 
 (*<*)
 lemmas WTrt'_induct = WTrt'_WTrts'.induct [split_format (complete)]
   and WTrt'_inducts = WTrt'_WTrts'.inducts [split_format (complete)]
 
 inductive_cases WTrt'_elim_cases[elim!]:
   "P,E,h,sh \<turnstile> V :=e :' T"
 (*>*)
 
 lemma [iff]: "P,E,h,sh \<turnstile> e\<^sub>1;;e\<^sub>2 :' T\<^sub>2 = (\<exists>T\<^sub>1. P,E,h,sh \<turnstile> e\<^sub>1:' T\<^sub>1 \<and> P,E,h,sh \<turnstile> e\<^sub>2:' T\<^sub>2)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)
 
 lemma [iff]: "P,E,h,sh \<turnstile> Val v :' T = (typeof\<^bsub>h\<^esub> v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)
 
 lemma [iff]: "P,E,h,sh \<turnstile> Var v :' T = (E v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)
 
 
 lemma wt_wt': "P,E,h,sh \<turnstile> e : T \<Longrightarrow> P,E,h,sh \<turnstile> e :' T"
 and wts_wts': "P,E,h,sh \<turnstile> es [:] Ts \<Longrightarrow> P,E,h,sh \<turnstile> es [:'] Ts"
 (*<*)
-apply (induct rule:WTrt_inducts)
-prefer 17
-apply(case_tac "assigned V e")
-apply(clarsimp simp add:fun_upd_same assigned_def simp del:fun_upd_apply)
-apply(erule (2) WTrt'_WTrts'.intros)
-apply(erule (1) WTrt'_WTrts'.intros)
-apply(blast intro:WTrt'_WTrts'.intros)+
-done
+proof(induct rule:WTrt_inducts)
+  case (WTrtBlock E V T e T')
+  then show ?case
+  proof(cases "assigned V e")
+    case True then show ?thesis using WTrtBlock.hyps(2)
+      by(clarsimp simp add:fun_upd_same assigned_def WTrt'_WTrts'.intros
+                  simp del:fun_upd_apply)
+  next
+    case False then show ?thesis
+      by (simp add: WTrtBlock.hyps(2) WTrt'_WTrts'.intros)
+  qed
+qed (blast intro:WTrt'_WTrts'.intros)+
 (*>*)
 
 
 lemma wt'_wt: "P,E,h,sh \<turnstile> e :' T \<Longrightarrow> P,E,h,sh \<turnstile> e : T"
 and wts'_wts: "P,E,h,sh \<turnstile> es [:'] Ts \<Longrightarrow> P,E,h,sh \<turnstile> es [:] Ts"
 (*<*)
-apply (induct rule:WTrt'_inducts)
-prefer 19
-apply(rule WTrt_WTrts.intros)
-apply(rule WTrt_WTrts.intros)
-apply(rule WTrt_WTrts.intros)
-apply simp
-apply(erule (2) WTrt_WTrts.intros)
-apply(blast intro:WTrt_WTrts.intros)+
-done
+proof(induct rule:WTrt'_inducts)
+  case Block: (19 v T\<^sub>1 T E V e\<^sub>2 T\<^sub>2)
+  let ?E = "E(V \<mapsto> T)"
+  have "P,?E,h,sh \<turnstile> Val v : T\<^sub>1" using Block.hyps(1) by simp
+  moreover have "P \<turnstile> T\<^sub>1 \<le> T" by(rule Block.hyps(2))
+  ultimately have "P,?E,h,sh \<turnstile> V:=Val v : Void" using WTrtLAss by simp
+  moreover have "P,?E,h,sh \<turnstile> e\<^sub>2 : T\<^sub>2" by(rule Block.hyps(4))
+  ultimately have "P,?E,h,sh \<turnstile> V:=Val v;; e\<^sub>2 : T\<^sub>2" by blast
+  then show ?case by simp
+qed (blast intro:WTrt_WTrts.intros)+
 (*>*)
 
 
 corollary wt'_iff_wt: "(P,E,h,sh \<turnstile> e :' T) = (P,E,h,sh \<turnstile> e : T)"
 (*<*)by(blast intro:wt_wt' wt'_wt)(*>*)
 
 
 corollary wts'_iff_wts: "(P,E,h,sh \<turnstile> es [:'] Ts) = (P,E,h,sh \<turnstile> es [:] Ts)"
 (*<*)by(blast intro:wts_wts' wts'_wts)(*>*)
 
 (*<*)
 lemmas WTrt_inducts2 = WTrt'_inducts [unfolded wt'_iff_wt wts'_iff_wts,
  case_names WTrtNew WTrtCast WTrtVal WTrtVar WTrtBinOpEq WTrtBinOpAdd WTrtLAss
  WTrtFAcc WTrtFAccNT WTrtSFAcc WTrtFAss WTrtFAssNT WTrtSFAss WTrtCall WTrtCallNT WTrtSCall
  WTrtNil WTrtCons WTrtInitBlock WTrtBlock WTrtSeq WTrtCond WTrtWhile WTrtThrow WTrtTry
  WTrtInit WTrtRI, consumes 1]
 (*>*)
 
 theorem assumes wf: "wwf_J_prog P" and hconf: "P \<turnstile> h \<surd>" and shconf: "P,h \<turnstile>\<^sub>s sh \<surd>"
 shows progress: "P,E,h,sh \<turnstile> e : T \<Longrightarrow>
  (\<And>l. \<lbrakk> \<D> e \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (e,b) \<surd>; \<not> final e \<rbrakk> \<Longrightarrow> \<exists>e' s' b'. P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>)"
 and "P,E,h,sh \<turnstile> es [:] Ts \<Longrightarrow>
  (\<And>l. \<lbrakk> \<D>s es \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (es,b) \<surd>; \<not> finals es \<rbrakk> \<Longrightarrow> \<exists>es' s' b'. P \<turnstile> \<langle>es,(h,l,sh),b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>)"
 (*<*)
 proof (induct rule:WTrt_inducts2)
   case (WTrtNew C) show ?case
   proof (cases b)
     case True then show ?thesis
     proof cases
       assume "\<exists>a. h a = None"
       with assms WTrtNew True show ?thesis
         by (fastforce del:exE intro!:RedNew simp add:new_Addr_def
                      elim!:wf_Fields_Ex[THEN exE])
     next
       assume "\<not>(\<exists>a. h a = None)"
       with assms WTrtNew True show ?thesis
         by(fastforce intro:RedNewFail simp:new_Addr_def)
     qed
   next
     case False then show ?thesis
     proof cases
       assume "\<exists>sfs. sh C = Some (sfs, Done)"
       with assms WTrtNew False show ?thesis
         by(fastforce intro:NewInitDoneRed simp:new_Addr_def)
     next
       assume "\<nexists>sfs. sh C = Some (sfs, Done)"
       with assms WTrtNew False show ?thesis
         by(fastforce intro:NewInitRed simp:new_Addr_def)
     qed
   qed
 next
   case (WTrtCast E e T C)
   have wte: "P,E,h,sh \<turnstile> e : T" and ref: "is_refT T"
    and IH: "\<And>l. \<lbrakk>\<D> e \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (e,b) \<surd>; \<not> final e\<rbrakk>
                 \<Longrightarrow> \<exists>e' s' b'. P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
    and D: "\<D> (Cast C e) \<lfloor>dom l\<rfloor>"
    and castconf: "P,sh \<turnstile>\<^sub>b (Cast C e,b) \<surd>" by fact+
   from D have De: "\<D> e \<lfloor>dom l\<rfloor>" by auto
   have bconf: "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using castconf bconf_Cast by fast
   show ?case
   proof cases
     assume "final e"
     with wte ref show ?thesis
     proof (rule finalRefE)
       assume "e = null" thus ?case by(fastforce intro:RedCastNull)
     next
       fix D a assume A: "T = Class D" "e = addr a"
       show ?thesis
       proof cases
         assume "P \<turnstile> D \<preceq>\<^sup>* C"
         thus ?thesis using A wte by(fastforce intro:RedCast)
       next
         assume "\<not> P \<turnstile> D \<preceq>\<^sup>* C"
         thus ?thesis using A wte by(fastforce elim!:RedCastFail)
       qed
     next
       fix a assume "e = Throw a"
       thus ?thesis by(blast intro!:red_reds.CastThrow)
     qed
   next
     assume nf: "\<not> final e"
     from IH[OF De bconf nf] show ?thesis by (blast intro:CastRed)
   qed
 next
   case WTrtVal thus ?case by(simp add:final_def)
 next
   case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def)
 next
   case (WTrtBinOpEq E e1 T1 e2 T2) show ?case
   proof cases
     assume "final e1"
     thus ?thesis
     proof (rule finalE)
       fix v1 assume eV[simp]: "e1 = Val v1"
       show ?thesis
       proof cases
         assume "final e2"
         thus ?thesis
         proof (rule finalE)
           fix v2 assume "e2 = Val v2"
           thus ?thesis using WTrtBinOpEq by(fastforce intro:RedBinOp)
         next
           fix a assume "e2 = Throw a"
           thus ?thesis using eV by(blast intro:red_reds.BinOpThrow2)
         qed
       next
         assume nf: "\<not> final e2"
         then have "P,sh \<turnstile>\<^sub>b (e2,b) \<surd>" using WTrtBinOpEq.prems(2) by(simp add:bconf_BinOp)
         with WTrtBinOpEq nf show ?thesis
           by simp (fast intro!:BinOpRed2)
       qed
     next
       fix a assume "e1 = Throw a"
       thus ?thesis by (fast intro:red_reds.BinOpThrow1)
     qed
   next
     assume nf: "\<not> final e1"
     then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e1,b) \<surd>" using WTrtBinOpEq.prems(2) by(simp add:bconf_BinOp)
     with WTrtBinOpEq nf e1 show ?thesis
       by simp (fast intro:BinOpRed1)
   qed
 next
   case (WTrtBinOpAdd E e1 e2) show ?case
   proof cases
     assume "final e1"
     thus ?thesis
     proof (rule finalE)
       fix v1 assume eV[simp]: "e1 = Val v1"
       show ?thesis
       proof cases
         assume "final e2"
         thus ?thesis
         proof (rule finalE)
           fix v2 assume eV2:"e2 = Val v2"
           then obtain i1 i2 where "v1 = Intg i1 \<and> v2 = Intg i2" using WTrtBinOpAdd by clarsimp
           thus ?thesis using WTrtBinOpAdd eV eV2 by(fastforce intro:RedBinOp)
         next
           fix a assume "e2 = Throw a"
           thus ?thesis using eV by(blast intro:red_reds.BinOpThrow2)
         qed
       next
         assume nf:"\<not> final e2"
         then have "P,sh \<turnstile>\<^sub>b (e2,b) \<surd>" using WTrtBinOpAdd.prems(2) by(simp add:bconf_BinOp)
         with WTrtBinOpAdd nf show ?thesis
           by simp (fast intro!:BinOpRed2)
       qed
     next
       fix a assume "e1 = Throw a"
       thus ?thesis by(fast intro:red_reds.BinOpThrow1)
     qed
   next
     assume nf: "\<not> final e1"
     then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e1,b) \<surd>" using WTrtBinOpAdd.prems(2) by(simp add:bconf_BinOp)
     with WTrtBinOpAdd nf e1 show ?thesis
       by simp (fast intro:BinOpRed1)
   qed
 next
   case (WTrtLAss E V T e T')
   then have bconf: "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using bconf_LAss by fast
   show ?case
   proof cases
     assume "final e" with WTrtLAss show ?thesis
       by(fastforce simp:final_def intro: red_reds.RedLAss red_reds.LAssThrow)
   next
     assume "\<not> final e" with WTrtLAss bconf show ?thesis
       by simp (fast intro:LAssRed)
   qed
 next
   case (WTrtFAcc E e C F T D)
   then have bconf: "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using bconf_FAcc by fast
   have wte: "P,E,h,sh \<turnstile> e : Class C"
    and field: "P \<turnstile> C has F,NonStatic:T in D" by fact+
   show ?case
   proof cases
     assume "final e"
     with wte show ?thesis
     proof (rule final_addrE)
       fix a assume e: "e = addr a"
       with wte obtain fs where hp: "h a = Some(C,fs)" by auto
       with hconf have "P,h \<turnstile> (C,fs) \<surd>" using hconf_def by fastforce
       then obtain v where "fs(F,D) = Some v" using field
         by(fastforce dest:has_fields_fun simp:oconf_def has_field_def)
       with hp e show ?thesis by (meson field red_reds.RedFAcc)
     next
       fix a assume "e = Throw a"
       thus ?thesis by(fastforce intro:red_reds.FAccThrow)
     qed
   next
     assume "\<not> final e" with WTrtFAcc bconf show ?thesis
       by(fastforce intro!:FAccRed)
   qed
 next
   case (WTrtFAccNT E e F D T)
   then have bconf: "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using bconf_FAcc by fast
   show ?case
   proof cases
     assume "final e"  \<comment> \<open>@{term e} is @{term null} or @{term throw}\<close>
     with WTrtFAccNT show ?thesis
       by(fastforce simp:final_def intro: red_reds.RedFAccNull red_reds.FAccThrow)
   next
     assume "\<not> final e" \<comment> \<open>@{term e} reduces by IH\<close>
     with WTrtFAccNT bconf show ?thesis by simp (fast intro:FAccRed)
   qed
 next
 case (WTrtSFAcc C F T D E) then show ?case
   proof (cases b)
     case True
     then obtain sfs i where shD: "sh D = \<lfloor>(sfs,i)\<rfloor>"
       using bconf_def[of P sh "C\<bullet>\<^sub>sF{D}" b] WTrtSFAcc.prems(2) initPD_def by auto
     with shconf have "P,h,D \<turnstile>\<^sub>s sfs \<surd>" using shconf_def[of P h sh] by auto
     then obtain v where sfsF: "sfs F = Some v" using WTrtSFAcc.hyps
       by(unfold soconf_def) (auto dest:has_field_idemp)
     then show ?thesis using WTrtSFAcc.hyps shD sfsF True
       by(fastforce elim:RedSFAcc)
   next
     case False
     with assms WTrtSFAcc show ?thesis
       by(metis (full_types) SFAccInitDoneRed SFAccInitRed)
   qed
 next
   case (WTrtFAss E e1 C F T D e2 T2)
   have wte1: "P,E,h,sh \<turnstile> e1 : Class C" and field: "P \<turnstile> C has F,NonStatic:T in D" by fact+
   show ?case
   proof cases
     assume "final e1"
     with wte1 show ?thesis
     proof (rule final_addrE)
       fix a assume e1: "e1 = addr a"
       show ?thesis
       proof cases
         assume "final e2"
         thus ?thesis
         proof (rule finalE)
           fix v assume "e2 = Val v"
           thus ?thesis using e1 wte1 by(fastforce intro: RedFAss[OF field])
         next
           fix a assume "e2 = Throw a"
           thus ?thesis using e1 by(fastforce intro:red_reds.FAssThrow2)
         qed
       next
         assume nf: "\<not> final e2"
         then have "P,sh \<turnstile>\<^sub>b (e2,b) \<surd>" using WTrtFAss.prems(2) e1 by(simp add:bconf_FAss)
         with WTrtFAss e1 nf show ?thesis
           by simp (fast intro!:FAssRed2)
       qed
     next
       fix a assume "e1 = Throw a"
       thus ?thesis by(fastforce intro:red_reds.FAssThrow1)
     qed
   next
     assume nf: "\<not> final e1"
     then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e1,b) \<surd>" using WTrtFAss.prems(2) by(simp add:bconf_FAss)
     with WTrtFAss nf e1 show ?thesis
       by simp (blast intro!:FAssRed1)
   qed
 next
   case (WTrtFAssNT E e\<^sub>1 e\<^sub>2 T\<^sub>2 F D)
   show ?case
   proof cases
     assume e1: "final e\<^sub>1"  \<comment> \<open>@{term e\<^sub>1} is @{term null} or @{term throw}\<close>
     show ?thesis
     proof cases
       assume "final e\<^sub>2"  \<comment> \<open>@{term e\<^sub>2} is @{term Val} or @{term throw}\<close>
       with WTrtFAssNT e1 show ?thesis
         by(fastforce simp:final_def
                     intro: red_reds.RedFAssNull red_reds.FAssThrow1 red_reds.FAssThrow2)
     next
       assume nf: "\<not> final e\<^sub>2" \<comment> \<open>@{term e\<^sub>2} reduces by IH\<close>
       show ?thesis
       proof (rule finalE[OF e1])
         fix v assume ev: "e\<^sub>1 = Val v"
         then have "P,sh \<turnstile>\<^sub>b (e\<^sub>2,b) \<surd>" using WTrtFAssNT.prems(2) nf by(simp add:bconf_FAss)
         with WTrtFAssNT ev nf show ?thesis by auto (meson red_reds.FAssRed2)
       next
         fix a assume et: "e\<^sub>1 = Throw a"
         then have "P,sh \<turnstile>\<^sub>b (e\<^sub>1,b) \<surd>" using WTrtFAssNT.prems(2) nf by(simp add:bconf_FAss)
         with WTrtFAssNT et nf show ?thesis by(fastforce intro: red_reds.FAssThrow1)
       qed
     qed
   next
     assume nf: "\<not> final e\<^sub>1" \<comment> \<open>@{term e\<^sub>1} reduces by IH\<close>
     then have e1: "val_of e\<^sub>1 = None" proof(cases e\<^sub>1)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e\<^sub>1,b) \<surd>" using WTrtFAssNT.prems(2) by(simp add:bconf_FAss)
     with WTrtFAssNT nf e1 show ?thesis
       by simp (blast intro!:FAssRed1)
   qed
 next
   case (WTrtSFAss C F T D E e2 T\<^sub>2)
   have field: "P \<turnstile> C has F,Static:T in D" by fact+
   show ?case
   proof cases
     assume "final e2"
     thus ?thesis
     proof (rule finalE)
       fix v assume ev: "e2 = Val v"
       then show ?case
       proof (cases b)
         case True
         then obtain sfs i where shD: "sh D = \<lfloor>(sfs,i)\<rfloor>"
           using bconf_def[of P _ "C\<bullet>\<^sub>sF{D} := e2"] WTrtSFAss.prems(2) initPD_def ev by auto
         with shconf have "P,h,D \<turnstile>\<^sub>s sfs \<surd>" using shconf_def[of P] by auto
         then obtain v where sfsF: "sfs F = Some v" using field
           by(unfold soconf_def) (auto dest:has_field_idemp)
         then show ?thesis using WTrtSFAss.hyps shD sfsF True ev
           by(fastforce elim:RedSFAss)
       next
         case False
         with assms WTrtSFAss ev show ?thesis
           by(metis (full_types) SFAssInitDoneRed SFAssInitRed)
       qed
     next
       fix a assume "e2 = Throw a"
       thus ?thesis by(fastforce intro:red_reds.SFAssThrow)
     qed
   next
     assume nf: "\<not> final e2"
     then have "val_of e2 = None" using final_def val_of_spec by fastforce
     then have "P,sh \<turnstile>\<^sub>b (e2,b) \<surd>" using WTrtSFAss.prems(2) by(simp add:bconf_SFAss)
     with WTrtSFAss nf show ?thesis
       by simp (fast intro!:SFAssRed)
   qed
 next
   case (WTrtCall E e C M Ts T pns body D es Ts')
   have wte: "P,E,h,sh \<turnstile> e : Class C"
    and "method": "P \<turnstile> C sees M,NonStatic:Ts\<rightarrow>T = (pns,body) in D"
    and wtes: "P,E,h,sh \<turnstile> es [:] Ts'"and sub: "P \<turnstile> Ts' [\<le>] Ts"
    and IHes: "\<And>l.
              \<lbrakk>\<D>s es \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (es,b) \<surd>; \<not> finals es\<rbrakk>
              \<Longrightarrow> \<exists>es' s' b'. P \<turnstile> \<langle>es,(h,l,sh),b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
    and D: "\<D> (e\<bullet>M(es)) \<lfloor>dom l\<rfloor>" by fact+
   show ?case
   proof cases
     assume "final e"
     with wte show ?thesis
     proof (rule final_addrE)
       fix a assume e_addr: "e = addr a"
       show ?thesis
       proof cases
         assume es: "\<exists>vs. es = map Val vs"
         from wte e_addr obtain fs where ha: "h a = Some(C,fs)" by auto
         show ?thesis
           using e_addr ha "method" WTrts_same_length[OF wtes] sub es sees_wf_mdecl[OF wf "method"]
           by(fastforce intro!: RedCall simp:list_all2_iff wf_mdecl_def)
       next
         assume "\<not>(\<exists>vs. es = map Val vs)"
         hence not_all_Val: "\<not>(\<forall>e \<in> set es. \<exists>v. e = Val v)"
           by(simp add:ex_map_conv)
         let ?ves = "takeWhile (\<lambda>e. \<exists>v. e = Val v) es"
         let ?rest = "dropWhile (\<lambda>e. \<exists>v. e = Val v) es"
         let ?ex = "hd ?rest" let ?rst = "tl ?rest"
         from not_all_Val have nonempty: "?rest \<noteq> []" by auto
         hence es: "es = ?ves @ ?ex # ?rst" by simp
         have "\<forall>e \<in> set ?ves. \<exists>v. e = Val v" by(fastforce dest:set_takeWhileD)
         then obtain vs where ves: "?ves = map Val vs"
           using ex_map_conv by blast
         show ?thesis
         proof cases
           assume "final ?ex"
           moreover from nonempty have "\<not>(\<exists>v. ?ex = Val v)"
             by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
               (simp add:dropWhile_eq_Cons_conv)
           ultimately obtain b where ex_Throw: "?ex = Throw b"
             by(fast elim!:finalE)
           show ?thesis using e_addr es ex_Throw ves
             by(fastforce intro:CallThrowParams)
         next
           assume not_fin: "\<not> final ?ex"
           have "finals es = finals(?ves @ ?ex # ?rst)" using es
             by(rule arg_cong)
           also have "\<dots> = finals(?ex # ?rst)" using ves by simp
           finally have "finals es = finals(?ex # ?rst)" .
           hence fes: "\<not> finals es" using not_finals_ConsI[OF not_fin] by blast
           have "P,sh \<turnstile>\<^sub>b (es,b) \<surd>" using bconf_Call WTrtCall.prems(2)
             by (metis e_addr option.simps(5) val_of.simps(1))
           thus ?thesis using fes e_addr D IHes by(fastforce intro!:CallParams)
         qed
       qed
     next
       fix a assume "e = Throw a"
       with WTrtCall.prems show ?thesis by(fast intro!:CallThrowObj)
     qed
   next
     assume nf: "\<not> final e"
     then have e1: "val_of e = None" proof(cases e)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using WTrtCall.prems(2) by(simp add:bconf_Call)
     with WTrtCall nf e1 show ?thesis by simp (blast intro!:CallObj)
   qed
 next
   case (WTrtCallNT E e es Ts M T) show ?case
   proof cases
     assume "final e"
     moreover
     { fix v assume e: "e = Val v"
       hence "e = null" using WTrtCallNT by simp
       have ?case
       proof cases
         assume "finals es"
         moreover
         { fix vs assume "es = map Val vs"
           with WTrtCallNT e have ?thesis by(fastforce intro: RedCallNull) }
         moreover
         { fix vs a es' assume "es = map Val vs @ Throw a # es'"
           with WTrtCallNT e have ?thesis by(fastforce intro: CallThrowParams) }
         ultimately show ?thesis by(fastforce simp:finals_def)
       next
         assume nf: "\<not> finals es" \<comment> \<open>@{term es} reduces by IH\<close>
         have "P,sh \<turnstile>\<^sub>b (es,b) \<surd>" using WTrtCallNT.prems(2) e by (simp add: bconf_Call)
         with WTrtCallNT e nf show ?thesis by(fastforce intro: CallParams)
       qed
     }
     moreover
     { fix a assume "e = Throw a"
       with WTrtCallNT have ?case by(fastforce intro: CallThrowObj) }
     ultimately show ?thesis by(fastforce simp:final_def)
   next
     assume nf: "\<not> final e" \<comment> \<open>@{term e} reduces by IH\<close>
     then have "val_of e = None" proof(cases e)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using WTrtCallNT.prems(2) by(simp add:bconf_Call)
     with WTrtCallNT nf show ?thesis by (fastforce intro:CallObj)
   qed
 next
   case (WTrtSCall C M Ts T pns body D E es Ts' sfs vs)
   have "method": "P \<turnstile> C sees M,Static:Ts\<rightarrow>T = (pns,body) in D"
    and wtes: "P,E,h,sh \<turnstile> es [:] Ts'"and sub: "P \<turnstile> Ts' [\<le>] Ts"
    and IHes: "\<And>l.
              \<lbrakk>\<D>s es \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (es,b) \<surd>; \<not> finals es\<rbrakk>
              \<Longrightarrow> \<exists>es' s' b'. P \<turnstile> \<langle>es,(h,l,sh),b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
    and clinit: "M = clinit \<longrightarrow> sh D = \<lfloor>(sfs, Processing)\<rfloor> \<and> es = map Val vs"
    and D: "\<D> (C\<bullet>\<^sub>sM(es)) \<lfloor>dom l\<rfloor>" by fact+
   show ?case
   proof cases
     assume es: "\<exists>vs. es = map Val vs"
     show ?thesis
     proof (cases b)
       case True
       then show ?thesis
       using "method" WTrts_same_length[OF wtes] sub es sees_wf_mdecl[OF wf "method"] True
       by(fastforce intro!: RedSCall simp:list_all2_iff wf_mdecl_def)
     next
       case False
       show ?thesis
       using "method" clinit WTrts_same_length[OF wtes] sub es False
         by (metis (full_types) red_reds.SCallInitDoneRed red_reds.SCallInitRed)
     qed
   next
     assume nmap: "\<not>(\<exists>vs. es = map Val vs)"
     hence not_all_Val: "\<not>(\<forall>e \<in> set es. \<exists>v. e = Val v)"
       by(simp add:ex_map_conv)
     let ?ves = "takeWhile (\<lambda>e. \<exists>v. e = Val v) es"
     let ?rest = "dropWhile (\<lambda>e. \<exists>v. e = Val v) es"
     let ?ex = "hd ?rest" let ?rst = "tl ?rest"
     from not_all_Val have nonempty: "?rest \<noteq> []" by auto
     hence es: "es = ?ves @ ?ex # ?rst" by simp
     have "\<forall>e \<in> set ?ves. \<exists>v. e = Val v" by(fastforce dest:set_takeWhileD)
     then obtain vs where ves: "?ves = map Val vs"
       using ex_map_conv by blast
     show ?thesis
     proof cases
       assume "final ?ex"
       moreover from nonempty have "\<not>(\<exists>v. ?ex = Val v)"
         by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
           (simp add:dropWhile_eq_Cons_conv)
       ultimately obtain b where ex_Throw: "?ex = Throw b"
         by(fast elim!:finalE)
       show ?thesis using es ex_Throw ves
         by(fastforce intro:SCallThrowParams)
     next
       assume not_fin: "\<not> final ?ex"
       have "finals es = finals(?ves @ ?ex # ?rst)" using es
         by(rule arg_cong)
       also have "\<dots> = finals(?ex # ?rst)" using ves by simp
       finally have "finals es = finals(?ex # ?rst)" .
       hence fes: "\<not> finals es" using not_finals_ConsI[OF not_fin] by blast
       have "P,sh \<turnstile>\<^sub>b (es,b) \<surd>"
         by (meson WTrtSCall.prems(2) nmap bconf_SCall map_vals_of_spec not_None_eq)
       thus ?thesis using fes D IHes by(fastforce intro!:SCallParams)
     qed
   qed
 next
   case WTrtNil thus ?case by simp
 next
   case (WTrtCons E e T es Ts)
   have IHe: "\<And>l. \<lbrakk>\<D> e \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (e,b) \<surd>; \<not> final e\<rbrakk>
                 \<Longrightarrow> \<exists>e' s' b'. P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
    and IHes: "\<And>l. \<lbrakk>\<D>s es \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (es,b) \<surd>; \<not> finals es\<rbrakk>
              \<Longrightarrow> \<exists>es' s' b'. P \<turnstile> \<langle>es,(h,l,sh),b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
    and D: "\<D>s (e#es) \<lfloor>dom l\<rfloor>" and not_fins: "\<not> finals(e # es)" by fact+
   have De: "\<D> e \<lfloor>dom l\<rfloor>" and Des: "\<D>s es (\<lfloor>dom l\<rfloor> \<squnion> \<A> e)"
     using D by auto
   show ?case
   proof cases
     assume "final e"
     thus ?thesis
     proof (rule finalE)
       fix v assume e: "e = Val v"
       hence Des': "\<D>s es \<lfloor>dom l\<rfloor>" using De Des by auto
       have bconfs: "P,sh \<turnstile>\<^sub>b (es,b) \<surd>" using WTrtCons.prems(2) e by(simp add: bconf_Cons)
       have not_fins_tl: "\<not> finals es" using not_fins e by simp
       show ?thesis using e IHes[OF Des' bconfs not_fins_tl]
         by (blast intro!:ListRed2)
     next
       fix a assume "e = Throw a"
       hence False using not_fins by simp
       thus ?thesis ..
     qed
   next
     assume nf:"\<not> final e"
     then have "val_of e = None" proof(cases e)qed(auto)
     then have bconf: "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using WTrtCons.prems(2) by(simp add: bconf_Cons)
     with IHe[OF De bconf nf] show ?thesis by(fast intro!:ListRed1)
   qed
 next
   case (WTrtInitBlock v T\<^sub>1 T E V e\<^sub>2 T\<^sub>2)
   have IH2: "\<And>l. \<lbrakk>\<D> e\<^sub>2 \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (e\<^sub>2,b) \<surd>; \<not> final e\<^sub>2\<rbrakk>
                   \<Longrightarrow> \<exists>e' s' b'. P \<turnstile> \<langle>e\<^sub>2,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
    and D: "\<D> {V:T := Val v; e\<^sub>2} \<lfloor>dom l\<rfloor>" by fact+
   show ?case
   proof cases
     assume "final e\<^sub>2"
     then show ?thesis
     proof (rule finalE)
       fix v\<^sub>2 assume "e\<^sub>2 = Val v\<^sub>2"
       thus ?thesis by(fast intro:RedInitBlock)
     next
       fix a assume "e\<^sub>2 = Throw a"
       thus ?thesis by(fast intro:red_reds.InitBlockThrow)
     qed
   next
     assume not_fin2: "\<not> final e\<^sub>2"
     then have "val_of e\<^sub>2 = None" proof(cases e\<^sub>2)qed(auto)
     from D have D2: "\<D> e\<^sub>2 \<lfloor>dom(l(V\<mapsto>v))\<rfloor>" by (auto simp:hyperset_defs)
     have e2conf: "P,sh \<turnstile>\<^sub>b (e\<^sub>2,b) \<surd>" using WTrtInitBlock.prems(2) by(simp add: bconf_InitBlock)
     from IH2[OF D2 e2conf not_fin2]
     obtain h' l' sh' e' b' where red2: "P \<turnstile> \<langle>e\<^sub>2,(h, l(V\<mapsto>v),sh),b\<rangle> \<rightarrow> \<langle>e',(h', l',sh'),b'\<rangle>"
       by auto
     from red_lcl_incr[OF red2] have "V \<in> dom l'" by auto
     with red2 show ?thesis by(fastforce intro:InitBlockRed)
   qed
 next
   case (WTrtBlock E V T e T')
   have IH: "\<And>l. \<lbrakk>\<D> e \<lfloor>dom l\<rfloor>; P,sh \<turnstile>\<^sub>b (e,b) \<surd>; \<not> final e\<rbrakk>
                  \<Longrightarrow> \<exists>e' s' b'. P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
    and unass: "\<not> assigned V e" and D: "\<D> {V:T; e} \<lfloor>dom l\<rfloor>" by fact+
   show ?case
   proof cases
     assume "final e"
     thus ?thesis
     proof (rule finalE)
       fix v assume "e = Val v" thus ?thesis by(fast intro:RedBlock)
     next
       fix a assume "e = Throw a"
       thus ?thesis by(fast intro:red_reds.BlockThrow)
     qed
   next
     assume not_fin: "\<not> final e"
     then have "val_of e = None" proof(cases e)qed(auto)
     from D have De: "\<D> e \<lfloor>dom(l(V:=None))\<rfloor>" by(simp add:hyperset_defs)
     have bconf: "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using WTrtBlock by(simp add: bconf_Block)
     from IH[OF De bconf not_fin]
     obtain h' l' sh' e' b' where red: "P \<turnstile> \<langle>e,(h,l(V:=None),sh),b\<rangle> \<rightarrow> \<langle>e',(h',l',sh'),b'\<rangle>"
       by auto
     show ?thesis
     proof (cases "l' V")
       assume "l' V = None"
       with red unass show ?thesis by(blast intro: BlockRedNone)
     next
       fix v assume "l' V = Some v"
       with red unass show ?thesis by(blast intro: BlockRedSome)
     qed
   qed
 next
   case (WTrtSeq E e1 T1 e2 T2) show ?case
   proof cases
     assume "final e1"
     thus ?thesis
       by(fast elim:finalE intro:RedSeq red_reds.SeqThrow)
   next
     assume nf: "\<not> final e1"
     then have e1: "val_of e1 = None" proof(cases e1)qed(auto)
     then show ?thesis
     proof(cases "lass_val_of e1")
       case None
       then have "P,sh \<turnstile>\<^sub>b (e1,b) \<surd>" using WTrtSeq.prems(2) e1 by(simp add: bconf_Seq)
       with WTrtSeq nf e1 None show ?thesis by simp (blast intro:SeqRed)
     next
       case (Some p)
       obtain V v where "e1 = V:=Val v" using lass_val_of_spec[OF Some] by simp
       then show ?thesis using SeqRed[OF RedLAss] by blast
     qed
   qed
 next
   case (WTrtCond E e e\<^sub>1 T\<^sub>1 e\<^sub>2 T\<^sub>2 T)
   have wt: "P,E,h,sh \<turnstile> e : Boolean" by fact
   show ?case
   proof cases
     assume "final e"
     thus ?thesis
     proof (rule finalE)
       fix v assume val: "e = Val v"
       then obtain b where v: "v = Bool b" using wt by auto
       show ?thesis
       proof (cases b)
         case True with val v show ?thesis by(fastforce intro:RedCondT simp: prod_cases3)
       next
         case False with val v show ?thesis by(fastforce intro:RedCondF simp: prod_cases3)
       qed
     next
       fix a assume "e = Throw a"
       thus ?thesis by(fast intro:red_reds.CondThrow)
     qed
   next
     assume nf: "\<not> final e"
     then have "bool_of e = None" proof(cases e)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using WTrtCond.prems(2) by(simp add: bconf_Cond)
     with WTrtCond nf show ?thesis by simp (blast intro:CondRed)
   qed
 next
   case WTrtWhile show ?case by(fast intro:RedWhile)
 next
   case (WTrtThrow E e T\<^sub>r T) show ?case
   proof cases
     assume "final e" \<comment> \<open>Then @{term e} must be @{term throw} or @{term null}\<close>
     with WTrtThrow show ?thesis
       by(fastforce simp:final_def is_refT_def
                   intro:red_reds.ThrowThrow red_reds.RedThrowNull)
   next
     assume nf: "\<not> final e" \<comment> \<open>Then @{term e} must reduce\<close>
     then have "val_of e = None" proof(cases e)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using WTrtThrow.prems(2) by(simp add: bconf_Throw)
     with WTrtThrow nf show ?thesis by simp (blast intro:ThrowRed)
   qed
 next
   case (WTrtTry E e1 T1 V C e2 T2)
   have wt1: "P,E,h,sh \<turnstile> e1 : T1" by fact
   show ?case
   proof cases
     assume "final e1"
     thus ?thesis
     proof (rule finalE)
       fix v assume "e1 = Val v"
       thus ?thesis by(fast intro:RedTry)
     next
       fix a assume e1_Throw: "e1 = Throw a"
       with wt1 obtain D fs where ha: "h a = Some(D,fs)" by fastforce
       show ?thesis
       proof cases
         assume "P \<turnstile> D \<preceq>\<^sup>* C"
         with e1_Throw ha show ?thesis by(fastforce intro!:RedTryCatch)
       next
         assume "\<not> P \<turnstile> D \<preceq>\<^sup>* C"
         with e1_Throw ha show ?thesis by(fastforce intro!:RedTryFail)
       qed
     qed
   next
     assume nf: "\<not> final e1"
     then have "val_of e1 = None" proof(cases e1)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e1,b) \<surd>" using WTrtTry.prems(2) by(simp add: bconf_Try)
     with WTrtTry nf show ?thesis by simp (fast intro:TryRed)
   qed
 next
   case (WTrtInit E e T\<^sub>r C Cs b) show ?case
   proof(cases Cs)
     case Nil then show ?thesis using WTrtInit by(fastforce intro!: RedInit)
   next
     case (Cons C' Cs')
     show ?thesis
     proof(cases b)
       case True then show ?thesis using Cons by(fastforce intro!: RedInitRInit)
     next
       case False
       show ?thesis
       proof(cases "sh C'")
         case None
         then show ?thesis using False Cons by(fastforce intro!: InitNoneRed)
       next
         case (Some sfsi)
         then obtain sfs i where sfsi:"sfsi = (sfs,i)" by(cases sfsi)
         show ?thesis
         proof(cases i)
           case Done
           then show ?thesis using False Some sfsi Cons by(fastforce intro!: RedInitDone)
         next
           case Processing
           then show ?thesis using False Some sfsi Cons by(fastforce intro!: RedInitProcessing)
         next
           case Error
           then show ?thesis using False Some sfsi Cons by(fastforce intro!: RedInitError)
         next
           case Prepared
           show ?thesis
           proof cases
             assume "C' = Object"
             then show ?thesis using False Some sfsi Prepared Cons by(fastforce intro: InitObjectRed)
           next
             assume "C' \<noteq> Object"
             then show ?thesis using False Some sfsi Prepared WTrtInit.hyps(3) Cons
               by(simp only: is_class_def)(fastforce intro!: InitNonObjectSuperRed)
           qed
         qed
       qed
     qed
   qed
 next
   case (WTrtRI E e T\<^sub>r e' T\<^sub>r' C Cs)
   obtain sfs i where shC: "sh C = \<lfloor>(sfs, i)\<rfloor>" using WTrtRI.hyps(9) by blast
   show ?case
   proof cases
     assume fin: "final e" then show ?thesis
     proof (rule finalE)
       fix v assume e: "e = Val v"
       then show ?thesis using shC e by(fast intro:RedRInit)
     next
       fix a assume eThrow: "e = Throw a"
       show ?thesis
       proof(cases Cs)
         case Nil then show ?thesis using eThrow shC by(fastforce intro!: RInitThrow)
       next
         case Cons then show ?thesis using eThrow shC by(fastforce intro!: RInitInitThrow)
       qed
     qed
   next
     assume nf: "\<not> final e"
     then have "val_of e = None" proof(cases e)qed(auto)
     then have "P,sh \<turnstile>\<^sub>b (e,b) \<surd>" using WTrtRI.prems(2) by(simp add: bconf_RI)
     with WTrtRI nf show ?thesis by simp (meson red_reds.RInitRed)
   qed
 qed
 (*>*)
 
 end