diff --git a/thys/Jinja/J/BigStep.thy b/thys/Jinja/J/BigStep.thy
--- a/thys/Jinja/J/BigStep.thy
+++ b/thys/Jinja/J/BigStep.thy
@@ -1,406 +1,422 @@
 (*  Title:      Jinja/J/BigStep.thy
 
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Big Step Semantics\<close>
 
 theory BigStep imports Expr State begin
 
 inductive
   eval :: "J_prog \<Rightarrow> expr \<Rightarrow> state \<Rightarrow> expr \<Rightarrow> state \<Rightarrow> bool"
           ("_ \<turnstile> ((1\<langle>_,/_\<rangle>) \<Rightarrow>/ (1\<langle>_,/_\<rangle>))" [51,0,0,0,0] 81)
   and evals :: "J_prog \<Rightarrow> expr list \<Rightarrow> state \<Rightarrow> expr list \<Rightarrow> state \<Rightarrow> bool"
            ("_ \<turnstile> ((1\<langle>_,/_\<rangle>) [\<Rightarrow>]/ (1\<langle>_,/_\<rangle>))" [51,0,0,0,0] 81)
   for P :: J_prog
 where
 
   New:
   "\<lbrakk> new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>(C,init_fields FDTs)) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>new C,(h,l)\<rangle> \<Rightarrow> \<langle>addr a,(h',l)\<rangle>"
 
 | NewFail:
   "new_Addr h = None \<Longrightarrow>
   P \<turnstile> \<langle>new C, (h,l)\<rangle> \<Rightarrow> \<langle>THROW OutOfMemory,(h,l)\<rangle>"
 
 | Cast:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>addr a,(h,l)\<rangle>; h a = Some(D,fs); P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>Cast C e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>addr a,(h,l)\<rangle>"
 
 | CastNull:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>null,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>Cast C e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>null,s\<^sub>1\<rangle>"
 
 | CastFail:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle>\<Rightarrow> \<langle>addr a,(h,l)\<rangle>; h a = Some(D,fs); \<not> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>Cast C e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>THROW ClassCast,(h,l)\<rangle>"
 
 | CastThrow:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>Cast C e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | Val:
   "P \<turnstile> \<langle>Val v,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>"
 
 | BinOp:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v\<^sub>1,s\<^sub>1\<rangle>; P \<turnstile> \<langle>e\<^sub>2,s\<^sub>1\<rangle> \<Rightarrow> \<langle>Val v\<^sub>2,s\<^sub>2\<rangle>; binop(bop,v\<^sub>1,v\<^sub>2) = Some v \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2,s\<^sub>0\<rangle>\<Rightarrow>\<langle>Val v,s\<^sub>2\<rangle>"
 
 | BinOpThrow1:
   "P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2, s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e,s\<^sub>1\<rangle>"
 
 | BinOpThrow2:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v\<^sub>1,s\<^sub>1\<rangle>; P \<turnstile> \<langle>e\<^sub>2,s\<^sub>1\<rangle> \<Rightarrow> \<langle>throw e,s\<^sub>2\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e,s\<^sub>2\<rangle>"
 
 | Var:
   "l V = Some v \<Longrightarrow>
   P \<turnstile> \<langle>Var V,(h,l)\<rangle> \<Rightarrow> \<langle>Val v,(h,l)\<rangle>"
 
 | LAss:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v,(h,l)\<rangle>; l' = l(V\<mapsto>v) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>V:=e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>unit,(h,l')\<rangle>"
 
 | LAssThrow:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>V:=e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | FAcc:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>addr a,(h,l)\<rangle>; h a = Some(C,fs); fs(F,D) = Some v \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<bullet>F{D},s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v,(h,l)\<rangle>"
 
 | FAccNull:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>null,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<bullet>F{D},s\<^sub>0\<rangle> \<Rightarrow> \<langle>THROW NullPointer,s\<^sub>1\<rangle>"
 
 | FAccThrow:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<bullet>F{D},s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | FAss:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>addr a,s\<^sub>1\<rangle>; P \<turnstile> \<langle>e\<^sub>2,s\<^sub>1\<rangle> \<Rightarrow> \<langle>Val v,(h\<^sub>2,l\<^sub>2)\<rangle>;
      h\<^sub>2 a = Some(C,fs); fs' = fs((F,D)\<mapsto>v); h\<^sub>2' = h\<^sub>2(a\<mapsto>(C,fs')) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<^sub>1\<bullet>F{D}:=e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>unit,(h\<^sub>2',l\<^sub>2)\<rangle>"
 
 | FAssNull:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>null,s\<^sub>1\<rangle>;  P \<turnstile> \<langle>e\<^sub>2,s\<^sub>1\<rangle> \<Rightarrow> \<langle>Val v,s\<^sub>2\<rangle> \<rbrakk> \<Longrightarrow>
   P \<turnstile> \<langle>e\<^sub>1\<bullet>F{D}:=e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>THROW NullPointer,s\<^sub>2\<rangle>"
 
 | FAssThrow1:
   "P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<^sub>1\<bullet>F{D}:=e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | FAssThrow2:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v,s\<^sub>1\<rangle>; P \<turnstile> \<langle>e\<^sub>2,s\<^sub>1\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>2\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<^sub>1\<bullet>F{D}:=e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>2\<rangle>"
 
 | CallObjThrow:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<bullet>M(ps),s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | CallParamsThrow:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v,s\<^sub>1\<rangle>; P \<turnstile> \<langle>es,s\<^sub>1\<rangle> [\<Rightarrow>] \<langle>map Val vs @ throw ex # es',s\<^sub>2\<rangle> \<rbrakk>
    \<Longrightarrow> P \<turnstile> \<langle>e\<bullet>M(es),s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw ex,s\<^sub>2\<rangle>"
 
 | CallNull:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>null,s\<^sub>1\<rangle>;  P \<turnstile> \<langle>ps,s\<^sub>1\<rangle> [\<Rightarrow>] \<langle>map Val vs,s\<^sub>2\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<bullet>M(ps),s\<^sub>0\<rangle> \<Rightarrow> \<langle>THROW NullPointer,s\<^sub>2\<rangle>"
 
 | Call:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>addr a,s\<^sub>1\<rangle>;  P \<turnstile> \<langle>ps,s\<^sub>1\<rangle> [\<Rightarrow>] \<langle>map Val vs,(h\<^sub>2,l\<^sub>2)\<rangle>;
      h\<^sub>2 a = Some(C,fs);  P \<turnstile> C sees M:Ts\<rightarrow>T = (pns,body) in D;
      length vs = length pns;  l\<^sub>2' = [this\<mapsto>Addr a, pns[\<mapsto>]vs];
      P \<turnstile> \<langle>body,(h\<^sub>2,l\<^sub>2')\<rangle> \<Rightarrow> \<langle>e',(h\<^sub>3,l\<^sub>3)\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<bullet>M(ps),s\<^sub>0\<rangle> \<Rightarrow> \<langle>e',(h\<^sub>3,l\<^sub>2)\<rangle>"
 
 | Block:
   "P \<turnstile> \<langle>e\<^sub>0,(h\<^sub>0,l\<^sub>0(V:=None))\<rangle> \<Rightarrow> \<langle>e\<^sub>1,(h\<^sub>1,l\<^sub>1)\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>{V:T; e\<^sub>0},(h\<^sub>0,l\<^sub>0)\<rangle> \<Rightarrow> \<langle>e\<^sub>1,(h\<^sub>1,l\<^sub>1(V:=l\<^sub>0 V))\<rangle>"
 
 | Seq:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>0,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v,s\<^sub>1\<rangle>; P \<turnstile> \<langle>e\<^sub>1,s\<^sub>1\<rangle> \<Rightarrow> \<langle>e\<^sub>2,s\<^sub>2\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e\<^sub>0;;e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>e\<^sub>2,s\<^sub>2\<rangle>"
 
 | SeqThrow:
   "P \<turnstile> \<langle>e\<^sub>0,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<^sub>0;;e\<^sub>1,s\<^sub>0\<rangle>\<Rightarrow>\<langle>throw e,s\<^sub>1\<rangle>"
 
 | CondT:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>true,s\<^sub>1\<rangle>; P \<turnstile> \<langle>e\<^sub>1,s\<^sub>1\<rangle> \<Rightarrow> \<langle>e',s\<^sub>2\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>if (e) e\<^sub>1 else e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>e',s\<^sub>2\<rangle>"
 
 | CondF:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>false,s\<^sub>1\<rangle>; P \<turnstile> \<langle>e\<^sub>2,s\<^sub>1\<rangle> \<Rightarrow> \<langle>e',s\<^sub>2\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>if (e) e\<^sub>1 else e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>e',s\<^sub>2\<rangle>"
 
 | CondThrow:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>if (e) e\<^sub>1 else e\<^sub>2, s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | WhileF:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>false,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>while (e) c,s\<^sub>0\<rangle> \<Rightarrow> \<langle>unit,s\<^sub>1\<rangle>"
 
 | WhileT:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>true,s\<^sub>1\<rangle>; P \<turnstile> \<langle>c,s\<^sub>1\<rangle> \<Rightarrow> \<langle>Val v\<^sub>1,s\<^sub>2\<rangle>; P \<turnstile> \<langle>while (e) c,s\<^sub>2\<rangle> \<Rightarrow> \<langle>e\<^sub>3,s\<^sub>3\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>while (e) c,s\<^sub>0\<rangle> \<Rightarrow> \<langle>e\<^sub>3,s\<^sub>3\<rangle>"
 
 | WhileCondThrow:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle> throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>while (e) c,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | WhileBodyThrow:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>true,s\<^sub>1\<rangle>; P \<turnstile> \<langle>c,s\<^sub>1\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>2\<rangle>\<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>while (e) c,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>2\<rangle>"
 
 | Throw:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>addr a,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>throw e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Throw a,s\<^sub>1\<rangle>"
 
 | ThrowNull:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>null,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>throw e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>THROW NullPointer,s\<^sub>1\<rangle>"
 
 | ThrowThrow:
   "P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>throw e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e',s\<^sub>1\<rangle>"
 
 | Try:
   "P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v\<^sub>1,s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>try e\<^sub>1 catch(C V) e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v\<^sub>1,s\<^sub>1\<rangle>"
 
 | TryCatch:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Throw a,(h\<^sub>1,l\<^sub>1)\<rangle>;  h\<^sub>1 a = Some(D,fs);  P \<turnstile> D \<preceq>\<^sup>* C;
      P \<turnstile> \<langle>e\<^sub>2,(h\<^sub>1,l\<^sub>1(V\<mapsto>Addr a))\<rangle> \<Rightarrow> \<langle>e\<^sub>2',(h\<^sub>2,l\<^sub>2)\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>try e\<^sub>1 catch(C V) e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>e\<^sub>2',(h\<^sub>2,l\<^sub>2(V:=l\<^sub>1 V))\<rangle>"
 
 | TryThrow:
   "\<lbrakk> P \<turnstile> \<langle>e\<^sub>1,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Throw a,(h\<^sub>1,l\<^sub>1)\<rangle>;  h\<^sub>1 a = Some(D,fs);  \<not> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>try e\<^sub>1 catch(C V) e\<^sub>2,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Throw a,(h\<^sub>1,l\<^sub>1)\<rangle>"
 
 | Nil:
   "P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>[],s\<rangle>"
 
 | Cons:
   "\<lbrakk> P \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow> \<langle>Val v,s\<^sub>1\<rangle>; P \<turnstile> \<langle>es,s\<^sub>1\<rangle> [\<Rightarrow>] \<langle>es',s\<^sub>2\<rangle> \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>e#es,s\<^sub>0\<rangle> [\<Rightarrow>] \<langle>Val v # es',s\<^sub>2\<rangle>"
 
 | ConsThrow:
   "P \<turnstile> \<langle>e, s\<^sub>0\<rangle> \<Rightarrow> \<langle>throw e', s\<^sub>1\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e#es, s\<^sub>0\<rangle> [\<Rightarrow>] \<langle>throw e' # es, s\<^sub>1\<rangle>"
 
 (*<*)
 lemmas eval_evals_induct = eval_evals.induct [split_format (complete)]
   and eval_evals_inducts = eval_evals.inducts [split_format (complete)]
 
 inductive_cases eval_cases [cases set]:
  "P \<turnstile> \<langle>Cast C e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>Val v,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>V:=e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>e\<bullet>F{D},s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>e\<^sub>1\<bullet>F{D}:=e\<^sub>2,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>e\<bullet>M{D}(es),s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>{V:T;e\<^sub>1},s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>e\<^sub>1;;e\<^sub>2,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>if (e) e\<^sub>1 else e\<^sub>2,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>while (b) c,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>throw e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>try e\<^sub>1 catch(C V) e\<^sub>2,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
  
 inductive_cases evals_cases [cases set]:
  "P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>e',s'\<rangle>"
  "P \<turnstile> \<langle>e#es,s\<rangle> [\<Rightarrow>] \<langle>e',s'\<rangle>"
 (*>*) 
 
 
 subsection"Final expressions"
 
 definition final :: "'a exp \<Rightarrow> bool"
 where
   "final e  \<equiv>  (\<exists>v. e = Val v) \<or> (\<exists>a. e = Throw a)"
 
 definition finals:: "'a exp list \<Rightarrow> bool"
 where
   "finals es  \<equiv>  (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')"
 
 lemma [simp]: "final(Val v)"
 (*<*)by(simp add:final_def)(*>*)
 
 lemma [simp]: "final(throw e) = (\<exists>a. e = addr a)"
 (*<*)by(simp add:final_def)(*>*)
 
 lemma finalE: "\<lbrakk> final e;  \<And>v. e = Val v \<Longrightarrow> R;  \<And>a. e = Throw a \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
 (*<*)by(auto simp:final_def)(*>*)
 
 lemma [iff]: "finals []"
 (*<*)by(simp add:finals_def)(*>*)
 
 lemma [iff]: "finals (Val v # es) = finals es"
 (*<*)
-apply(clarsimp simp add: finals_def)
-apply(rule iffI)
- apply(erule disjE)
-  apply simp
- apply(rule disjI2)
- apply clarsimp
- apply(case_tac vs)
-  apply simp
- apply fastforce
-apply(erule disjE)
- apply clarsimp
-apply(rule disjI2)
-apply clarsimp
-apply(rule_tac x = "v#vs" in exI)
-apply simp
-done
+proof(rule iffI)
+  assume "finals (Val v # es)"
+  moreover {
+    fix vs a es'
+    assume "\<forall>vs a es'. es \<noteq> map Val vs @ Throw a # es'"
+      and "Val v # es = map Val vs @ Throw a # es'"
+    then have "\<exists>vs. es = map Val vs" by(case_tac vs; simp)
+  }
+  ultimately show "finals es" by(clarsimp simp add: finals_def)
+next
+  assume "finals es"
+  moreover {
+    fix vs a es'
+    assume "es = map Val vs @ Throw a # es'"
+    then have "\<exists>vs' a' es''. Val v # map Val vs @ Throw a # es' = map Val vs' @ Throw a' # es''"
+      by(rule_tac x = "v#vs" in exI) simp
+  }
+  ultimately show "finals (Val v # es)" by(clarsimp simp add: finals_def)
+qed
 (*>*)
 
 lemma finals_app_map[iff]: "finals (map Val vs @ es) = finals es"
 (*<*)by(induct_tac vs, auto)(*>*)
 
 lemma [iff]: "finals (map Val vs)"
 (*<*)using finals_app_map[of vs "[]"]by(simp)(*>*)
 
 lemma [iff]: "finals (throw e # es) = (\<exists>a. e = addr a)"
 (*<*)
-apply(simp add:finals_def)
-apply(rule iffI)
- apply clarsimp
- apply(case_tac vs)
-  apply simp
- apply fastforce
-apply clarsimp
-apply(rule_tac x = "[]" in exI)
-apply simp
-done
+proof(rule iffI)
+  assume "finals (throw e # es)"
+  moreover {
+    fix vs a es'
+    assume "throw e # es = map Val vs @ Throw a # es'"
+    then have "\<exists>a. e = addr a" by(case_tac vs; simp)
+  }
+  ultimately show "\<exists>a. e = addr a" by(clarsimp simp add: finals_def)
+next
+  assume "\<exists>a. e = addr a"
+  moreover {
+    fix vs a es'
+    assume "e = addr a"
+    then have "\<exists>vs aa es'. Throw a # es = map Val vs @ Throw aa # es'"
+      by(rule_tac x = "[]" in exI) simp
+  }
+  ultimately show "finals (throw e # es)" by(clarsimp simp add: finals_def)
+qed
 (*>*)
 
 lemma not_finals_ConsI: "\<not> final e \<Longrightarrow> \<not> finals(e#es)"
- (*<*)
-apply(clarsimp simp add:finals_def final_def)
-apply(case_tac vs)
-apply auto
-done
+(*<*)
+proof -
+  assume "\<not> final e"
+  moreover {
+    fix vs a es'
+    assume "\<forall>v. e \<noteq> Val v" and "\<forall>a. e \<noteq> Throw a"
+    then have "e # es \<noteq> map Val vs @ Throw a # es'" by(case_tac vs; simp)
+  }
+  ultimately show ?thesis by(clarsimp simp add:finals_def final_def)
+qed
 (*>*)
 
 
 lemma eval_final: "P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> final e'"
  and evals_final: "P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> finals es'"
 (*<*)by(induct rule:eval_evals.inducts, simp_all)(*>*)
 
 
 lemma eval_lcl_incr: "P \<turnstile> \<langle>e,(h\<^sub>0,l\<^sub>0)\<rangle> \<Rightarrow> \<langle>e',(h\<^sub>1,l\<^sub>1)\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1"
  and evals_lcl_incr: "P \<turnstile> \<langle>es,(h\<^sub>0,l\<^sub>0)\<rangle> [\<Rightarrow>] \<langle>es',(h\<^sub>1,l\<^sub>1)\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1"
 (*<*)
 proof (induct rule: eval_evals_inducts)
   case BinOp show ?case by(rule subset_trans)(rule BinOp.hyps)+
 next
   case Call thus ?case
     by(simp del: fun_upd_apply) 
 next
   case Seq show ?case by(rule subset_trans)(rule Seq.hyps)+
 next
   case CondT show ?case by(rule subset_trans)(rule CondT.hyps)+
 next
   case CondF show ?case by(rule subset_trans)(rule CondF.hyps)+
 next
   case WhileT thus ?case by(blast)
 next
   case TryCatch thus ?case by(clarsimp simp:dom_def split:if_split_asm) blast
 next
   case Cons show ?case by(rule subset_trans)(rule Cons.hyps)+
 next
   case Block thus ?case by(auto simp del:fun_upd_apply)
 qed auto
 (*>*)
 
 text\<open>Only used later, in the small to big translation, but is already a
 good sanity check:\<close>
 
 lemma eval_finalId:  "final e \<Longrightarrow> P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>e,s\<rangle>"
 (*<*)by (erule finalE) (iprover intro: eval_evals.intros)+(*>*)
 
 
 lemma eval_finalsId:
 assumes finals: "finals es" shows "P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es,s\<rangle>"
 (*<*)
   using finals
 proof (induct es type: list)
   case Nil show ?case by (rule eval_evals.intros)
 next
   case (Cons e es)
   have hyp: "finals es \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es,s\<rangle>"
    and finals: "finals (e # es)" by fact+
   show "P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>e # es,s\<rangle>"
   proof cases
     assume "final e"
     thus ?thesis
     proof (cases rule: finalE)
       fix v assume e: "e = Val v"
       have "P \<turnstile> \<langle>Val v,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>" by (simp add: eval_finalId)
       moreover from finals e have "P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>es,s\<rangle>" by(fast intro:hyp)
       ultimately have "P \<turnstile> \<langle>Val v#es,s\<rangle> [\<Rightarrow>] \<langle>Val v#es,s\<rangle>"
         by (rule eval_evals.intros)
       with e show ?thesis by simp
     next
       fix a assume e: "e = Throw a"
       have "P \<turnstile> \<langle>Throw a,s\<rangle> \<Rightarrow> \<langle>Throw a,s\<rangle>" by (simp add: eval_finalId)
       hence "P \<turnstile> \<langle>Throw a#es,s\<rangle> [\<Rightarrow>] \<langle>Throw a#es,s\<rangle>" by (rule eval_evals.intros)
       with e show ?thesis by simp
     qed
   next
     assume "\<not> final e"
     with not_finals_ConsI finals have False by blast
     thus ?thesis ..
   qed
 qed
 (*>*)
 
 
 theorem eval_hext: "P \<turnstile> \<langle>e,(h,l)\<rangle> \<Rightarrow> \<langle>e',(h',l')\<rangle> \<Longrightarrow> h \<unlhd> h'"
 and evals_hext:  "P \<turnstile> \<langle>es,(h,l)\<rangle> [\<Rightarrow>] \<langle>es',(h',l')\<rangle> \<Longrightarrow> h \<unlhd> h'"
 (*<*)
 proof (induct rule: eval_evals_inducts)
   case New thus ?case
     by(fastforce intro!: hext_new intro:LeastI simp:new_Addr_def
                 split:if_split_asm simp del:fun_upd_apply)
 next
   case BinOp thus ?case by (fast elim!:hext_trans)
 next
   case BinOpThrow2 thus ?case by(fast elim!: hext_trans)
 next
   case FAss thus ?case
     by(auto simp:sym[THEN hext_upd_obj] simp del:fun_upd_apply
             elim!: hext_trans)
 next
   case FAssNull thus ?case by (fast elim!:hext_trans)
 next
   case FAssThrow2 thus ?case by (fast elim!:hext_trans)
 next
   case CallParamsThrow thus ?case by(fast elim!: hext_trans)
 next
   case CallNull thus ?case by(fast elim!: hext_trans)
 next
   case Call thus ?case by(fast elim!: hext_trans)
 next
   case Seq thus ?case by(fast elim!: hext_trans)
 next
   case CondT thus ?case by(fast elim!: hext_trans)
 next
   case CondF thus ?case by(fast elim!: hext_trans)
 next
   case WhileT thus ?case by(fast elim!: hext_trans)
 next
   case WhileBodyThrow thus ?case by (fast elim!: hext_trans)
 next
   case TryCatch thus ?case  by(fast elim!: hext_trans)
 next
   case Cons thus ?case by (fast intro: hext_trans)
 qed auto
 (*>*)
 
 
 end
diff --git a/thys/Jinja/J/Expr.thy b/thys/Jinja/J/Expr.thy
--- a/thys/Jinja/J/Expr.thy
+++ b/thys/Jinja/J/Expr.thy
@@ -1,104 +1,98 @@
 (*  Title:      Jinja/J/Expr.thy
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Expressions\<close>
 
 theory Expr
 imports "../Common/Exceptions"
 begin
 
 datatype bop = Eq | Add     \<comment> \<open>names of binary operations\<close>
 
 datatype 'a exp
   = new cname      \<comment> \<open>class instance creation\<close>
   | Cast cname "('a exp)"      \<comment> \<open>type cast\<close>
   | Val val      \<comment> \<open>value\<close>
   | BinOp "('a exp)" bop "('a exp)"     ("_ \<guillemotleft>_\<guillemotright> _" [80,0,81] 80)      \<comment> \<open>binary operation\<close>
   | Var 'a                                               \<comment> \<open>local variable (incl. parameter)\<close>
   | LAss 'a "('a exp)"     ("_:=_" [90,90]90)                    \<comment> \<open>local assignment\<close>
   | FAcc "('a exp)" vname cname     ("_\<bullet>_{_}" [10,90,99]90)      \<comment> \<open>field access\<close>
   | FAss "('a exp)" vname cname "('a exp)"     ("_\<bullet>_{_} := _" [10,90,99,90]90)      \<comment> \<open>field assignment\<close>
   | Call "('a exp)" mname "('a exp list)"     ("_\<bullet>_'(_')" [90,99,0] 90)            \<comment> \<open>method call\<close>
   | Block 'a ty "('a exp)"     ("'{_:_; _}")
   | Seq "('a exp)" "('a exp)"     ("_;;/ _"             [61,60]60)
   | Cond "('a exp)" "('a exp)" "('a exp)"     ("if '(_') _/ else _" [80,79,79]70)
   | While "('a exp)" "('a exp)"     ("while '(_') _"     [80,79]70)
   | throw "('a exp)"
   | TryCatch "('a exp)" cname 'a "('a exp)"     ("try _/ catch'(_ _') _"  [0,99,80,79] 70)
 
 type_synonym
   expr = "vname exp"            \<comment> \<open>Jinja expression\<close>
 type_synonym
   J_mb = "vname list \<times> expr"    \<comment> \<open>Jinja method body: parameter names and expression\<close>
 type_synonym
   J_prog = "J_mb prog"          \<comment> \<open>Jinja program\<close>
 
 text\<open>The semantics of binary operators:\<close>
 
 fun binop :: "bop \<times> val \<times> val \<Rightarrow> val option" where
   "binop(Eq,v\<^sub>1,v\<^sub>2) = Some(Bool (v\<^sub>1 = v\<^sub>2))"
 | "binop(Add,Intg i\<^sub>1,Intg i\<^sub>2) = Some(Intg(i\<^sub>1+i\<^sub>2))"
 | "binop(bop,v\<^sub>1,v\<^sub>2) = None"
 
 lemma [simp]:
   "(binop(Add,v\<^sub>1,v\<^sub>2) = Some v) = (\<exists>i\<^sub>1 i\<^sub>2. v\<^sub>1 = Intg i\<^sub>1 \<and> v\<^sub>2 = Intg i\<^sub>2 \<and> v = Intg(i\<^sub>1+i\<^sub>2))"
-(*<*)
-apply(cases v\<^sub>1)
-apply auto
-apply(cases v\<^sub>2)
-apply auto
-done
-(*>*)
+(*<*)by(cases v\<^sub>1; cases v\<^sub>2) auto(*>*)
 
 
 subsection "Syntactic sugar"
 
 abbreviation (input)
   InitBlock:: "'a \<Rightarrow> ty \<Rightarrow> 'a exp \<Rightarrow> 'a exp \<Rightarrow> 'a exp"   ("(1'{_:_ := _;/ _})") where
   "InitBlock V T e1 e2 == {V:T; V := e1;; e2}"
 
 abbreviation unit where "unit == Val Unit"
 abbreviation null where "null == Val Null"
 abbreviation "addr a == Val(Addr a)"
 abbreviation "true == Val(Bool True)"
 abbreviation "false == Val(Bool False)"
 
 abbreviation
   Throw :: "addr \<Rightarrow> 'a exp" where
   "Throw a == throw(Val(Addr a))"
 
 abbreviation
   THROW :: "cname \<Rightarrow> 'a exp" where
   "THROW xc == Throw(addr_of_sys_xcpt xc)"
 
 
 subsection\<open>Free Variables\<close>
 
 primrec fv :: "expr \<Rightarrow> vname set" and fvs :: "expr list \<Rightarrow> vname set" where
   "fv(new C) = {}"
 | "fv(Cast C e) = fv e"
 | "fv(Val v) = {}"
 | "fv(e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(Var V) = {V}"
 | "fv(LAss V e) = {V} \<union> fv e"
 | "fv(e\<bullet>F{D}) = fv e"
 | "fv(e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(e\<bullet>M(es)) = fv e \<union> fvs es"
 | "fv({V:T; e}) = fv e - {V}"
 | "fv(e\<^sub>1;;e\<^sub>2) = fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(if (b) e\<^sub>1 else e\<^sub>2) = fv b \<union> fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(while (b) e) = fv b \<union> fv e"
 | "fv(throw e) = fv e"
 | "fv(try e\<^sub>1 catch(C V) e\<^sub>2) = fv e\<^sub>1 \<union> (fv e\<^sub>2 - {V})"
 | "fvs([]) = {}"
 | "fvs(e#es) = fv e \<union> fvs es"
 
 lemma [simp]: "fvs(es\<^sub>1 @ es\<^sub>2) = fvs es\<^sub>1 \<union> fvs es\<^sub>2"
 (*<*)by (induct es\<^sub>1 type:list) auto(*>*)
 
 lemma [simp]: "fvs(map Val vs) = {}"
 (*<*)by (induct vs) auto(*>*)
 
 end
diff --git a/thys/Jinja/J/WellType.thy b/thys/Jinja/J/WellType.thy
--- a/thys/Jinja/J/WellType.thy
+++ b/thys/Jinja/J/WellType.thy
@@ -1,235 +1,201 @@
 (*  Title:      Jinja/J/WellType.thy
 
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Well-typedness of Jinja expressions\<close>
 
 theory WellType
 imports "../Common/Objects" Expr
 begin
 
 type_synonym
   env  = "vname \<rightharpoonup> ty"
 
 inductive
   WT :: "[J_prog,env, expr     , ty     ] \<Rightarrow> bool"
          ("_,_ \<turnstile> _ :: _"   [51,51,51]50)
   and WTs :: "[J_prog,env, expr list, ty list] \<Rightarrow> bool"
          ("_,_ \<turnstile> _ [::] _" [51,51,51]50)
   for P :: J_prog
 where
   
   WTNew:
   "is_class P C  \<Longrightarrow>
   P,E \<turnstile> new C :: Class C"
 
 | WTCast:
   "\<lbrakk> P,E \<turnstile> e :: Class D;  is_class P C;  P \<turnstile> C \<preceq>\<^sup>* D \<or> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> Cast C e :: Class C"
 
 | WTVal:
   "typeof v = Some T \<Longrightarrow>
   P,E \<turnstile> Val v :: T"
 
 | WTVar:
   "E V = Some T \<Longrightarrow>
   P,E \<turnstile> Var V :: T"
 (*
 WTBinOp:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: T\<^sub>1;  P,E \<turnstile> e\<^sub>2 :: T\<^sub>2;
      case bop of Eq \<Rightarrow> (P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<or> P \<turnstile> T\<^sub>2 \<le> T\<^sub>1) \<and> T = Boolean
                | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 :: T"
 *)
 | WTBinOpEq:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: T\<^sub>1;  P,E \<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 \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<^sub>1 \<guillemotleft>Eq\<guillemotright> e\<^sub>2 :: Boolean"
 
 | WTBinOpAdd:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: Integer;  P,E \<turnstile> e\<^sub>2 :: Integer \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<^sub>1 \<guillemotleft>Add\<guillemotright> e\<^sub>2 :: Integer"
 
 | WTLAss:
   "\<lbrakk> E V = Some T;  P,E \<turnstile> e :: T';  P \<turnstile> T' \<le> T;  V \<noteq> this \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> V:=e :: Void"
 
 | WTFAcc:
   "\<lbrakk> P,E \<turnstile> e :: Class C;  P \<turnstile> C sees F:T in D \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<bullet>F{D} :: T"
 
 | WTFAss:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: Class C;  P \<turnstile> C sees F:T in D;  P,E \<turnstile> e\<^sub>2 :: T';  P \<turnstile> T' \<le> T \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<^sub>1\<bullet>F{D}:=e\<^sub>2 :: Void"
 
 | WTCall:
   "\<lbrakk> P,E \<turnstile> e :: Class C;  P \<turnstile> C sees M:Ts \<rightarrow> T = (pns,body) in D;
      P,E \<turnstile> es [::] Ts';  P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<bullet>M(es) :: T"
 
 | WTBlock:
   "\<lbrakk> is_type P T;  P,E(V \<mapsto> T) \<turnstile> e :: T' \<rbrakk>
   \<Longrightarrow>  P,E \<turnstile> {V:T; e} :: T'"
 
 | WTSeq:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1::T\<^sub>1;  P,E \<turnstile> e\<^sub>2::T\<^sub>2 \<rbrakk>
   \<Longrightarrow>  P,E \<turnstile> e\<^sub>1;;e\<^sub>2 :: T\<^sub>2"
 | WTCond:
   "\<lbrakk> P,E \<turnstile> e :: Boolean;  P,E \<turnstile> e\<^sub>1::T\<^sub>1;  P,E \<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 \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :: T"
 
 | WTWhile:
   "\<lbrakk> P,E \<turnstile> e :: Boolean;  P,E \<turnstile> c::T \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> while (e) c :: Void"
 
 | WTThrow:
   "P,E \<turnstile> e :: Class C  \<Longrightarrow> 
   P,E \<turnstile> throw e :: Void"
 
 | WTTry:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: T;  P,E(V \<mapsto> Class C) \<turnstile> e\<^sub>2 :: T; is_class P C \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 :: T"
 
 \<comment> \<open>well-typed expression lists\<close>
 
 | WTNil:
   "P,E \<turnstile> [] [::] []"
 
 | WTCons:
   "\<lbrakk> P,E \<turnstile> e :: T;  P,E \<turnstile> es [::] Ts \<rbrakk>
   \<Longrightarrow>  P,E \<turnstile> e#es [::] T#Ts"
 
 (*<*)
 (*
 lemmas [intro!] = WTNew WTCast WTVal WTVar WTBinOp WTLAss WTFAcc WTFAss WTCall WTBlock WTSeq
                   WTWhile WTThrow WTTry WTNil WTCons
 lemmas [intro]  = WTCond1 WTCond2
 *)
 declare WT_WTs.intros[intro!] (* WTNil[iff] *)
 
 lemmas WT_WTs_induct = WT_WTs.induct [split_format (complete)]
   and WT_WTs_inducts = WT_WTs.inducts [split_format (complete)]
 (*>*)
 
 lemma [iff]: "(P,E \<turnstile> [] [::] Ts) = (Ts = [])"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTs.cases)
-done
-(*>*)
+(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)
 
 lemma [iff]: "(P,E \<turnstile> e#es [::] T#Ts) = (P,E \<turnstile> e :: T \<and> P,E \<turnstile> es [::] Ts)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTs.cases)
-done
-(*>*)
+(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)
 
 lemma [iff]: "(P,E \<turnstile> (e#es) [::] Ts) =
   (\<exists>U Us. Ts = U#Us \<and> P,E \<turnstile> e :: U \<and> P,E \<turnstile> es [::] Us)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTs.cases)
-done
-(*>*)
+(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)
 
 lemma [iff]: "\<And>Ts. (P,E \<turnstile> es\<^sub>1 @ es\<^sub>2 [::] Ts) =
   (\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E \<turnstile> es\<^sub>1 [::] Ts\<^sub>1 \<and> P,E \<turnstile> es\<^sub>2[::]Ts\<^sub>2)"
 (*<*)
-apply(induct es\<^sub>1 type:list)
- apply simp
-apply clarsimp
-apply(erule thin_rl)
-apply (rule iffI)
- apply clarsimp
- apply(rule exI)+
- apply(rule conjI)
-  prefer 2 apply blast
- apply simp
-apply fastforce
-done
+proof(induct es\<^sub>1 type:list)
+  case (Cons a list)
+  let ?lhs = "(\<exists>U Us. Ts = U # Us \<and> P,E \<turnstile> a :: U \<and>
+        (\<exists>Ts\<^sub>1 Ts\<^sub>2. Us = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E \<turnstile> list [::] Ts\<^sub>1 \<and> P,E \<turnstile> es\<^sub>2 [::] Ts\<^sub>2))"
+  let ?rhs = "(\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and>
+        (\<exists>U Us. Ts\<^sub>1 = U # Us \<and> P,E \<turnstile> a :: U \<and> P,E \<turnstile> list [::] Us) \<and> P,E \<turnstile> es\<^sub>2 [::] Ts\<^sub>2)"
+  { assume ?lhs
+    then have ?rhs by (auto intro: Cons_eq_appendI)
+  }
+  moreover {
+    assume ?rhs
+    then have ?lhs by fastforce
+  }
+  ultimately have "?lhs = ?rhs" by(rule iffI)
+  then show ?case by (clarsimp simp: Cons)
+qed simp
 (*>*)
 
 lemma [iff]: "P,E \<turnstile> Val v :: T = (typeof v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 lemma [iff]: "P,E \<turnstile> Var V :: T = (E V = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 lemma [iff]: "P,E \<turnstile> e\<^sub>1;;e\<^sub>2 :: T\<^sub>2 = (\<exists>T\<^sub>1. P,E \<turnstile> e\<^sub>1::T\<^sub>1 \<and> P,E \<turnstile> e\<^sub>2::T\<^sub>2)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 lemma [iff]: "(P,E \<turnstile> {V:T; e} :: T') = (is_type P T \<and> P,E(V\<mapsto>T) \<turnstile> e :: T')"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 (*<*)
 inductive_cases WT_elim_cases[elim!]:
   "P,E \<turnstile> V :=e :: T"
   "P,E \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :: T"
   "P,E \<turnstile> while (e) c :: T"
   "P,E \<turnstile> throw e :: T"
   "P,E \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 :: T"
   "P,E \<turnstile> Cast D e :: T"
   "P,E \<turnstile> a\<bullet>F{D} :: T"
   "P,E \<turnstile> a\<bullet>F{D} := v :: T"
   "P,E \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 :: T"
   "P,E \<turnstile> new C :: T"
   "P,E \<turnstile> e\<bullet>M(ps) :: T"
 (*>*)
 
 
 lemma wt_env_mono:
   "P,E \<turnstile> e :: T \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E' \<turnstile> e :: T)" and 
   "P,E \<turnstile> es [::] Ts \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E' \<turnstile> es [::] Ts)"
 (*<*)
-apply(induct rule: WT_WTs_inducts)
-apply(simp add: WTNew)
-apply(fastforce simp: WTCast)
-apply(fastforce simp: WTVal)
-apply(simp add: WTVar map_le_def dom_def)
-apply(fastforce simp: WTBinOpEq)
-apply(fastforce simp: WTBinOpAdd)
-apply(force simp:map_le_def)
-apply(fastforce simp: WTFAcc)
-apply(fastforce simp: WTFAss del:WT_WTs.intros WT_elim_cases)
-apply(fastforce simp: WTCall)
-apply(fastforce simp: map_le_def WTBlock)
-apply(fastforce simp: WTSeq)
-apply(fastforce simp: WTCond)
-apply(fastforce simp: WTWhile)
-apply(fastforce simp: WTThrow)
-apply(fastforce simp: WTTry map_le_def dom_def)
-apply(simp add: WTNil)
-apply(simp add: WTCons)
-done
+proof(induct rule: WT_WTs_inducts)
+  case WTVar then show ?case by(simp add: map_le_def dom_def)
+next
+  case WTLAss then show ?case by(force simp:map_le_def)
+qed fastforce+
 (*>*)
 
 
 lemma WT_fv: "P,E \<turnstile> e :: T \<Longrightarrow> fv e \<subseteq> dom E"
 and "P,E \<turnstile> es [::] Ts \<Longrightarrow> fvs es \<subseteq> dom E"
 (*<*)
-apply(induct rule:WT_WTs.inducts)
-apply(simp_all del: fun_upd_apply)
-apply fast+
-done
+proof(induct rule:WT_WTs.inducts)
+  case WTVar then show ?case by fastforce
+next
+  case WTLAss then show ?case by fastforce
+next
+  case WTBlock then show ?case by fastforce
+next
+  case WTTry then show ?case by fastforce
+qed simp_all
 
 end
 (*>*)
diff --git a/thys/Jinja/J/WellTypeRT.thy b/thys/Jinja/J/WellTypeRT.thy
--- a/thys/Jinja/J/WellTypeRT.thy
+++ b/thys/Jinja/J/WellTypeRT.thy
@@ -1,317 +1,243 @@
 (*  Title:      Jinja/J/WellTypeRT.thy
 
     Author:     Tobias Nipkow
     Copyright   2003 Technische Universitaet Muenchen
 *)
 
 section \<open>Runtime Well-typedness\<close>
 
 theory WellTypeRT
 imports WellType
 begin
 
 inductive
   WTrt :: "J_prog \<Rightarrow> heap \<Rightarrow> env \<Rightarrow> expr \<Rightarrow> ty \<Rightarrow> bool"
   and WTrts :: "J_prog \<Rightarrow> heap \<Rightarrow> env \<Rightarrow> expr list \<Rightarrow> 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"
 
 | WTrtNew:
   "is_class P C  \<Longrightarrow>
   P,E,h \<turnstile> new C : Class C"
 
 | WTrtCast:
   "\<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"
 
 | WTrtVal:
   "typeof\<^bsub>h\<^esub> v = Some T \<Longrightarrow>
   P,E,h \<turnstile> Val v : T"
 
 | WTrtVar:
   "E V = Some T  \<Longrightarrow>
   P,E,h \<turnstile> Var V : T"
 (*
 WTrtBinOp:
   "\<lbrakk> P,E,h \<turnstile> e\<^sub>1 : T\<^sub>1;  P,E,h \<turnstile> e\<^sub>2 : T\<^sub>2;
     case bop of Eq \<Rightarrow> T = Boolean
               | Add \<Rightarrow> T\<^sub>1 = Integer \<and> T\<^sub>2 = Integer \<and> T = Integer \<rbrakk>
    \<Longrightarrow> P,E,h \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T"
 *)
 | WTrtBinOpEq:
   "\<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"
 
 | WTrtBinOpAdd:
   "\<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"
 
 | WTrtLAss:
   "\<lbrakk> E V = Some T;  P,E,h \<turnstile> e : T';  P \<turnstile> T' \<le> T \<rbrakk>
    \<Longrightarrow> P,E,h \<turnstile> V:=e : Void"
 
 | WTrtFAcc:
   "\<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"
 
 | WTrtFAccNT:
   "P,E,h \<turnstile> e : NT \<Longrightarrow>
   P,E,h \<turnstile> e\<bullet>F{D} : T"
 
 | WTrtFAss:
   "\<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"
 
 | WTrtFAssNT:
   "\<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"
 
 | WTrtCall:
   "\<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"
 
 | WTrtCallNT:
   "\<lbrakk> P,E,h \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts \<rbrakk>
   \<Longrightarrow> P,E,h \<turnstile> e\<bullet>M(es) : T"
 
 | WTrtBlock:
   "P,E(V\<mapsto>T),h \<turnstile> e : T'  \<Longrightarrow>
   P,E,h \<turnstile> {V:T; e} : T'"
 
 | WTrtSeq:
   "\<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"
 
 | WTrtCond:
   "\<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"
 
 | WTrtWhile:
   "\<lbrakk> P,E,h \<turnstile> e : Boolean;  P,E,h \<turnstile> c:T \<rbrakk>
   \<Longrightarrow>  P,E,h \<turnstile> while(e) c : Void"
 
 | WTrtThrow:
   "\<lbrakk> P,E,h \<turnstile> e : T\<^sub>r; is_refT T\<^sub>r \<rbrakk> \<Longrightarrow>
   P,E,h \<turnstile> throw e : T"
 
 | WTrtTry:
   "\<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"
 
 \<comment> \<open>well-typed expression lists\<close>
 
 | WTrtNil:
   "P,E,h \<turnstile> [] [:] []"
 
 | WTrtCons:
   "\<lbrakk> P,E,h \<turnstile> e : T;  P,E,h \<turnstile> es [:] Ts \<rbrakk>
   \<Longrightarrow>  P,E,h \<turnstile> e#es [:] T#Ts"
 
 (*<*)
 declare WTrt_WTrts.intros[intro!] WTrtNil[iff]
 declare
   WTrtFAcc[rule del] WTrtFAccNT[rule del]
   WTrtFAss[rule del] WTrtFAssNT[rule del]
   WTrtCall[rule del] WTrtCallNT[rule del]
 
 lemmas WTrt_induct = WTrt_WTrts.induct [split_format (complete)]
   and WTrt_inducts = WTrt_WTrts.inducts [split_format (complete)]
 (*>*)
 
 
 subsection\<open>Easy consequences\<close>
 
 lemma [iff]: "(P,E,h \<turnstile> [] [:] Ts) = (Ts = [])"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrts.cases)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)
 
 lemma [iff]: "(P,E,h \<turnstile> e#es [:] T#Ts) = (P,E,h \<turnstile> e : T \<and> P,E,h \<turnstile> es [:] Ts)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrts.cases)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)
 
 lemma [iff]: "(P,E,h \<turnstile> (e#es) [:] Ts) =
   (\<exists>U Us. Ts = U#Us \<and> P,E,h \<turnstile> e : U \<and> P,E,h \<turnstile> es [:] Us)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrts.cases)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)
 
 lemma [simp]: "\<forall>Ts. (P,E,h \<turnstile> es\<^sub>1 @ es\<^sub>2 [:] Ts) =
   (\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E,h \<turnstile> es\<^sub>1 [:] Ts\<^sub>1 & P,E,h \<turnstile> es\<^sub>2[:]Ts\<^sub>2)"
 (*<*)
-apply(induct_tac es\<^sub>1)
- apply simp
-apply clarsimp
-apply(erule thin_rl)
-apply (rule iffI)
- apply clarsimp
- apply(rule exI)+
- apply(rule conjI)
-  prefer 2 apply blast
- apply simp
-apply fastforce
-done
+proof(induct es\<^sub>1)
+  case (Cons a list)
+  let ?lhs = "\<lambda>Ts. (\<exists>U Us. Ts = U # Us \<and> P,E,h \<turnstile> a : U \<and>
+        (\<exists>Ts\<^sub>1 Ts\<^sub>2. Us = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E,h \<turnstile> list [:] Ts\<^sub>1 \<and> P,E,h \<turnstile> es\<^sub>2 [:] Ts\<^sub>2))"
+  let ?rhs = "\<lambda>Ts. (\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and>
+        (\<exists>U Us. Ts\<^sub>1 = U # Us \<and> P,E,h \<turnstile> a : U \<and> P,E,h \<turnstile> list [:] Us) \<and> P,E,h \<turnstile> es\<^sub>2 [:] Ts\<^sub>2)"
+  { fix Ts assume "?lhs Ts"
+    then have "?rhs Ts" by (auto intro: Cons_eq_appendI)
+  }
+  moreover {
+    fix Ts assume "?rhs Ts"
+    then have "?lhs Ts" by fastforce
+  }
+  ultimately have "\<And>Ts. ?lhs Ts = ?rhs Ts" by(rule iffI)
+  then show ?case by (clarsimp simp: Cons)
+qed simp
 (*>*)
 
 lemma [iff]: "P,E,h \<turnstile> Val v : T = (typeof\<^bsub>h\<^esub> v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
 
 lemma [iff]: "P,E,h \<turnstile> Var v : T = (E v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
 
 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)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
 
 lemma [iff]: "P,E,h \<turnstile> {V:T; e} : T'  =  (P,E(V\<mapsto>T),h \<turnstile> e : T')"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
+
 (*<*)
 inductive_cases WTrt_elim_cases[elim!]:
   "P,E,h \<turnstile> v :=e : T"
   "P,E,h \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T"
   "P,E,h \<turnstile> while(e) c : T"
   "P,E,h \<turnstile> throw e : T"
   "P,E,h \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 : T"
   "P,E,h \<turnstile> Cast D e : T"
   "P,E,h \<turnstile> e\<bullet>F{D} : T"
   "P,E,h \<turnstile> e\<bullet>F{D} := v : T"
   "P,E,h \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T"
   "P,E,h \<turnstile> new C : T"
   "P,E,h \<turnstile> e\<bullet>M{D}(es) : T"
 (*>*)
 
 subsection\<open>Some interesting lemmas\<close>
 
 lemma WTrts_Val[simp]:
  "\<And>Ts. (P,E,h \<turnstile> map Val vs [:] Ts) = (map (typeof\<^bsub>h\<^esub>) vs = map Some Ts)"
 (*<*)
-apply(induct vs)
- apply simp
-apply(case_tac Ts)
- apply simp
-apply simp
-done
+proof(induct vs)
+  case (Cons a vs)
+  then show ?case by(case_tac Ts; simp)
+qed simp
 (*>*)
 
 
 lemma WTrts_same_length: "\<And>Ts. P,E,h \<turnstile> es [:] Ts \<Longrightarrow> length es = length Ts"
 (*<*)by(induct es type:list)auto(*>*)
 
 
 lemma WTrt_env_mono:
   "P,E,h \<turnstile> e : T \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E',h \<turnstile> e : T)" and
   "P,E,h \<turnstile> es [:] Ts \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E',h \<turnstile> es [:] Ts)"
 (*<*)
-apply(induct rule: WTrt_inducts)
-apply(simp add: WTrtNew)
-apply(fastforce simp: WTrtCast)
-apply(fastforce simp: WTrtVal)
-apply(simp add: WTrtVar map_le_def dom_def)
-apply(fastforce simp add: WTrtBinOpEq)
-apply(fastforce simp add: WTrtBinOpAdd)
-apply(force simp: map_le_def)
-apply(fastforce simp: WTrtFAcc)
-apply(simp add: WTrtFAccNT)
-apply(fastforce simp: WTrtFAss)
-apply(fastforce simp: WTrtFAssNT)
-apply(fastforce simp: WTrtCall)
-apply(fastforce simp: WTrtCallNT)
-apply(simp add: WTrtNil)
-apply(simp add: WTrtCons)
-apply(fastforce simp: map_le_def)
-apply(fastforce)
-apply(fastforce simp: WTrtSeq)
-apply(fastforce simp: WTrtWhile)
-apply(fastforce simp: WTrtThrow)
-apply(auto simp: WTrtTry map_le_def dom_def)
-done
+proof(induct rule: WTrt_inducts)
+  case WTrtVar then show ?case by(simp add: map_le_def dom_def)
+next
+  case WTrtLAss then show ?case by(force simp:map_le_def)
+qed(fastforce intro: WTrt_WTrts.intros)+
 (*>*)
 
 
 lemma WTrt_hext_mono: "P,E,h \<turnstile> e : T \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> e : T"
 and WTrts_hext_mono: "P,E,h \<turnstile> es [:] Ts \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,E,h' \<turnstile> es [:] Ts"
 (*<*)
-apply(induct rule: WTrt_inducts)
-apply(simp add: WTrtNew)
-apply(fastforce simp: WTrtCast)
-apply(fastforce simp: WTrtVal dest:hext_typeof_mono)
-apply(simp add: WTrtVar)
-apply(fastforce simp add: WTrtBinOpEq)
-apply(fastforce simp add: WTrtBinOpAdd)
-apply(fastforce simp add: WTrtLAss)
-apply(fast intro: WTrtFAcc)
-apply(simp add: WTrtFAccNT)
-apply(fastforce simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
-apply(fastforce simp: WTrtFAssNT)
-apply(fastforce simp: WTrtCall)
-apply(fastforce simp: WTrtCallNT)
-apply(fastforce)
-apply(fastforce simp add: WTrtSeq)
-apply(fastforce simp add: WTrtCond)
-apply(fastforce simp add: WTrtWhile)
-apply(fastforce simp add: WTrtThrow)
-apply(fastforce simp: WTrtTry)
-apply(simp add: WTrtNil)
-apply(simp add: WTrtCons)
-done
+proof(induct rule: WTrt_inducts)
+  case WTrtVal then show ?case by(simp add: hext_typeof_mono)
+qed(fastforce intro: WTrt_WTrts.intros)+
 (*>*)
 
 
 lemma WT_implies_WTrt: "P,E \<turnstile> e :: T \<Longrightarrow> P,E,h \<turnstile> e : T"
 and WTs_implies_WTrts: "P,E \<turnstile> es [::] Ts \<Longrightarrow> P,E,h \<turnstile> es [:] Ts"
 (*<*)
-apply(induct rule: WT_WTs_inducts)
-apply fast
-apply (fast)
-apply(fastforce dest:typeof_lit_typeof)
-apply(simp)
-apply(fastforce)
-apply(fastforce)
-apply(fastforce)
-apply(fastforce simp: WTrtFAcc has_visible_field)
-apply(fastforce simp: WTrtFAss dest: has_visible_field)
-apply(fastforce simp: WTrtCall)
-apply(fastforce)
-apply(fastforce)
-apply(fastforce simp: WTrtCond)
-apply(fastforce)
-apply(fastforce)
-apply(fastforce)
-apply(simp)
-apply(simp)
-done
+proof(induct rule: WT_WTs_inducts)
+  case WTVal then show ?case by(fastforce dest: typeof_lit_typeof)
+next
+  case WTFAcc
+  then show ?case by(fastforce simp: WTrtFAcc has_visible_field)
+next
+  case WTFAss
+  then show ?case by(fastforce simp: WTrtFAss dest: has_visible_field)
+qed(fastforce intro: WTrt_WTrts.intros)+
 (*>*)
 
 
 end
diff --git a/thys/JinjaDCI/J/Expr.thy b/thys/JinjaDCI/J/Expr.thy
--- a/thys/JinjaDCI/J/Expr.thy
+++ b/thys/JinjaDCI/J/Expr.thy
@@ -1,572 +1,579 @@
 (*  Title:      JinjaDCI/J/Expr.thy
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/Expr.thy by Tobias Nipkow
 *)
 
 section \<open> Expressions \<close>
 
 theory Expr
 imports "../Common/Exceptions"
 begin
 
 datatype bop = Eq | Add     \<comment> \<open>names of binary operations\<close>
 
 datatype 'a exp
   = new cname      \<comment> \<open>class instance creation\<close>
   | Cast cname "('a exp)"      \<comment> \<open>type cast\<close>
   | Val val      \<comment> \<open>value\<close>
   | BinOp "('a exp)" bop "('a exp)"     ("_ \<guillemotleft>_\<guillemotright> _" [80,0,81] 80)      \<comment> \<open>binary operation\<close>
   | Var 'a                                               \<comment> \<open>local variable (incl. parameter)\<close>
   | LAss 'a "('a exp)"     ("_:=_" [90,90]90)                    \<comment> \<open>local assignment\<close>
   | FAcc "('a exp)" vname cname     ("_\<bullet>_{_}" [10,90,99]90)      \<comment> \<open>field access\<close>
   | SFAcc cname vname cname     ("_\<bullet>\<^sub>s_{_}" [10,90,99]90)      \<comment> \<open>static field access\<close>
   | FAss "('a exp)" vname cname "('a exp)"     ("_\<bullet>_{_} := _" [10,90,99,90]90)      \<comment> \<open>field assignment\<close>
   | SFAss cname vname cname "('a exp)"     ("_\<bullet>\<^sub>s_{_} := _" [10,90,99,90]90)      \<comment> \<open>static field assignment\<close>
   | Call "('a exp)" mname "('a exp list)"     ("_\<bullet>_'(_')" [90,99,0] 90)            \<comment> \<open>method call\<close>
   | SCall cname mname "('a exp list)"     ("_\<bullet>\<^sub>s_'(_')" [90,99,0] 90)            \<comment> \<open>static method call\<close>
   | Block 'a ty "('a exp)"     ("'{_:_; _}")
   | Seq "('a exp)" "('a exp)"     ("_;;/ _"             [61,60]60)
   | Cond "('a exp)" "('a exp)" "('a exp)"     ("if '(_') _/ else _" [80,79,79]70)
   | While "('a exp)" "('a exp)"     ("while '(_') _"     [80,79]70)
   | throw "('a exp)"
   | TryCatch "('a exp)" cname 'a "('a exp)"     ("try _/ catch'(_ _') _"  [0,99,80,79] 70)
   | INIT cname "cname list" bool "('a exp)" ("INIT _ '(_,_') \<leftarrow> _" [60,60,60,60] 60) \<comment> \<open>internal initialization command: class, list of superclasses to initialize, preparation flag; command on hold\<close>
   | RI cname "('a exp)" "cname list" "('a exp)" ("RI '(_,_') ; _ \<leftarrow> _" [60,60,60,60] 60) \<comment> \<open>running of the initialization procedure for class with expression, classes still to initialize command on hold\<close>
 
 type_synonym
   expr = "vname exp"            \<comment> \<open>Jinja expression\<close>
 type_synonym
   J_mb = "vname list \<times> expr"    \<comment> \<open>Jinja method body: parameter names and expression\<close>
 type_synonym
   J_prog = "J_mb prog"          \<comment> \<open>Jinja program\<close>
 
 type_synonym
   init_stack = "expr list \<times> bool"  \<comment> \<open>Stack of expressions waiting on initialization in small step; indicator boolean True if current expression has been init checked\<close>
 
 text\<open>The semantics of binary operators: \<close>
 
 fun binop :: "bop \<times> val \<times> val \<Rightarrow> val option" where
   "binop(Eq,v\<^sub>1,v\<^sub>2) = Some(Bool (v\<^sub>1 = v\<^sub>2))"
 | "binop(Add,Intg i\<^sub>1,Intg i\<^sub>2) = Some(Intg(i\<^sub>1+i\<^sub>2))"
 | "binop(bop,v\<^sub>1,v\<^sub>2) = None"
 
 lemma [simp]:
   "(binop(Add,v\<^sub>1,v\<^sub>2) = Some v) = (\<exists>i\<^sub>1 i\<^sub>2. v\<^sub>1 = Intg i\<^sub>1 \<and> v\<^sub>2 = Intg i\<^sub>2 \<and> v = Intg(i\<^sub>1+i\<^sub>2))"
-(*<*)
-apply(cases v\<^sub>1)
-apply auto
-apply(cases v\<^sub>2)
-apply auto
-done
-(*>*)
+(*<*)by(cases v\<^sub>1; cases v\<^sub>2) auto(*>*)
 
 
 lemma map_Val_throw_eq:
  "map Val vs @ throw ex # es = map Val vs' @ throw ex' # es' \<Longrightarrow> ex = ex'"
-apply(induct vs arbitrary: vs')
- apply(case_tac vs', auto)+
-done
+(*<*)by(induct vs arbitrary: vs'; case_tac vs') auto(*>*)
 
 lemma map_Val_nthrow_neq:
  "map Val vs = map Val vs' @ throw ex' # es' \<Longrightarrow> False"
-apply(induct vs arbitrary: vs')
- apply(case_tac vs', auto)+
-done
+(*<*)by(induct vs arbitrary: vs'; case_tac vs') auto(*>*)
 
 lemma map_Val_eq:
  "map Val vs = map Val vs' \<Longrightarrow> vs = vs'"
-apply(induct vs arbitrary: vs')
- apply(case_tac vs', auto)+
-done
+(*<*)by(induct vs arbitrary: vs'; case_tac vs') auto(*>*)
 
 
 lemma init_rhs_neq [simp]: "e \<noteq> INIT C (Cs,b) \<leftarrow> e"
 proof -
   have "size e \<noteq> size (INIT C (Cs,b) \<leftarrow> e)" by auto
   then show ?thesis by fastforce
 qed
 
 lemma init_rhs_neq' [simp]: "INIT C (Cs,b) \<leftarrow> e \<noteq> e"
 proof -
   have "size e \<noteq> size (INIT C (Cs,b) \<leftarrow> e)" by auto
   then show ?thesis by fastforce
 qed
 
 lemma ri_rhs_neq [simp]: "e \<noteq> RI(C,e');Cs \<leftarrow> e"
 proof -
   have "size e \<noteq> size (RI(C,e');Cs \<leftarrow> e)" by auto
   then show ?thesis by fastforce
 qed
 
 lemma ri_rhs_neq' [simp]: "RI(C,e');Cs \<leftarrow> e \<noteq> e"
 proof -
   have "size e \<noteq> size (RI(C,e');Cs \<leftarrow> e)" by auto
   then show ?thesis by fastforce
 qed
 
 subsection "Syntactic sugar"
 
 abbreviation (input)
   InitBlock:: "'a \<Rightarrow> ty \<Rightarrow> 'a exp \<Rightarrow> 'a exp \<Rightarrow> 'a exp"   ("(1'{_:_ := _;/ _})") where
   "InitBlock V T e1 e2 == {V:T; V := e1;; e2}"
 
 abbreviation unit where "unit == Val Unit"
 abbreviation null where "null == Val Null"
 abbreviation "addr a == Val(Addr a)"
 abbreviation "true == Val(Bool True)"
 abbreviation "false == Val(Bool False)"
 
 abbreviation
   Throw :: "addr \<Rightarrow> 'a exp" where
   "Throw a == throw(Val(Addr a))"
 
 abbreviation
   THROW :: "cname \<Rightarrow> 'a exp" where
   "THROW xc == Throw(addr_of_sys_xcpt xc)"
 
 
 subsection\<open>Free Variables\<close>
 
 primrec fv :: "expr \<Rightarrow> vname set" and fvs :: "expr list \<Rightarrow> vname set" where
   "fv(new C) = {}"
 | "fv(Cast C e) = fv e"
 | "fv(Val v) = {}"
 | "fv(e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(Var V) = {V}"
 | "fv(LAss V e) = {V} \<union> fv e"
 | "fv(e\<bullet>F{D}) = fv e"
 | "fv(C\<bullet>\<^sub>sF{D}) = {}"
 | "fv(e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = fv e\<^sub>2"
 | "fv(e\<bullet>M(es)) = fv e \<union> fvs es"
 | "fv(C\<bullet>\<^sub>sM(es)) = fvs es"
 | "fv({V:T; e}) = fv e - {V}"
 | "fv(e\<^sub>1;;e\<^sub>2) = fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(if (b) e\<^sub>1 else e\<^sub>2) = fv b \<union> fv e\<^sub>1 \<union> fv e\<^sub>2"
 | "fv(while (b) e) = fv b \<union> fv e"
 | "fv(throw e) = fv e"
 | "fv(try e\<^sub>1 catch(C V) e\<^sub>2) = fv e\<^sub>1 \<union> (fv e\<^sub>2 - {V})"
 | "fv(INIT C (Cs,b) \<leftarrow> e) = fv e"
 | "fv(RI (C,e);Cs \<leftarrow> e') = fv e \<union> fv e'"
 | "fvs([]) = {}"
 | "fvs(e#es) = fv e \<union> fvs es"
 
 lemma [simp]: "fvs(es\<^sub>1 @ es\<^sub>2) = fvs es\<^sub>1 \<union> fvs es\<^sub>2"
 (*<*)by (induct es\<^sub>1 type:list) auto(*>*)
 
 lemma [simp]: "fvs(map Val vs) = {}"
 (*<*)by (induct vs) auto(*>*)
 
 
 subsection\<open>Accessing expression constructor arguments\<close>
 
 fun val_of :: "'a exp \<Rightarrow> val option" where
 "val_of (Val v) = Some v" |
 "val_of _ = None"
 
 lemma val_of_spec: "val_of e = Some v \<Longrightarrow> e = Val v"
 proof(cases e) qed(auto)
 
 fun lass_val_of :: "'a exp \<Rightarrow> ('a \<times> val) option" where
 "lass_val_of (V:=Val v) = Some (V, v)" |
 "lass_val_of _ = None"
 
 lemma lass_val_of_spec:
 assumes "lass_val_of e = \<lfloor>a\<rfloor>"
 shows "e = (fst a:=Val (snd a))"
 using assms proof(cases e)
   case (LAss V e') then show ?thesis using assms proof(cases e')qed(auto)
 qed(auto)
 
 fun map_vals_of :: "'a exp list \<Rightarrow> val list option" where
 "map_vals_of (e#es) = (case val_of e of Some v \<Rightarrow> (case map_vals_of es of Some vs \<Rightarrow> Some (v#vs) 
                                                                         | _ \<Rightarrow> None)
                                       | _ \<Rightarrow> None)" |
 "map_vals_of [] = Some []"
 
 lemma map_vals_of_spec: "map_vals_of es = Some vs \<Longrightarrow> es = map Val vs"
 proof(induct es arbitrary: vs) qed(auto simp: val_of_spec)
 
 lemma map_vals_of_Vals[simp]: "map_vals_of (map Val vs) = \<lfloor>vs\<rfloor>" by(induct vs, auto)
 
 lemma map_vals_of_throw[simp]:
  "map_vals_of (map Val vs @ throw e # es') = None"
  by(induct vs, auto)
 
 
 fun bool_of :: "'a exp \<Rightarrow> bool option" where
 "bool_of true = Some True" |
 "bool_of false = Some False" |
 "bool_of _ = None"
 
 lemma bool_of_specT:
 assumes "bool_of e = Some True" shows "e = true"
 proof -
   have "bool_of e = Some True" by fact
   then show ?thesis
   proof(cases e)
     case (Val x3) with assms show ?thesis
     proof(cases x3)
       case (Bool x) with assms Val show ?thesis
       proof(cases x)qed(auto)
     qed(simp_all)
   qed(auto)
 qed
 
 lemma bool_of_specF:
 assumes "bool_of e = Some False" shows "e = false"
 proof -
   have "bool_of e = Some False" by fact
   then show ?thesis
   proof(cases e)
     case (Val x3) with assms show ?thesis
     proof(cases x3)
       case (Bool x) with assms Val show ?thesis
       proof(cases x)qed(auto)
     qed(simp_all)
   qed(auto)
 qed
 
 
 fun throw_of :: "'a exp \<Rightarrow> 'a exp option" where
 "throw_of (throw e') = Some e'" |
 "throw_of _ = None"
 
 lemma throw_of_spec: "throw_of e = Some e' \<Longrightarrow> e = throw e'"
 proof(cases e) qed(auto)
 
 fun init_exp_of :: "'a exp \<Rightarrow> 'a exp option" where
 "init_exp_of (INIT C (Cs,b) \<leftarrow> e) = Some e" |
 "init_exp_of (RI(C,e');Cs \<leftarrow> e) = Some e" |
 "init_exp_of _ = None"
 
 lemma init_exp_of_neq [simp]: "init_exp_of e = \<lfloor>e'\<rfloor> \<Longrightarrow> e' \<noteq> e" by(cases e, auto)
 lemma init_exp_of_neq'[simp]: "init_exp_of e = \<lfloor>e'\<rfloor> \<Longrightarrow> e \<noteq> e'" by(cases e, auto)
 
 
 subsection\<open>Class initialization\<close>
 
 text \<open> This section defines a few functions that return information
  about an expression's current initialization status. \<close>
 
  \<comment> \<open> True if expression contains @{text INIT}, @{text RI}, or a call to a static method @{term clinit} \<close>
 primrec sub_RI :: "'a exp \<Rightarrow> bool" and sub_RIs :: "'a exp list \<Rightarrow> bool" where
   "sub_RI(new C) = False"
 | "sub_RI(Cast C e) = sub_RI e"
 | "sub_RI(Val v) = False"
 | "sub_RI(e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = (sub_RI e\<^sub>1 \<or> sub_RI e\<^sub>2)"
 | "sub_RI(Var V) = False"
 | "sub_RI(LAss V e) = sub_RI e"
 | "sub_RI(e\<bullet>F{D}) = sub_RI e"
 | "sub_RI(C\<bullet>\<^sub>sF{D}) = False"
 | "sub_RI(e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = (sub_RI e\<^sub>1 \<or> sub_RI e\<^sub>2)"
 | "sub_RI(C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = sub_RI e\<^sub>2"
 | "sub_RI(e\<bullet>M(es)) = (sub_RI e \<or> sub_RIs es)"
 | "sub_RI(C\<bullet>\<^sub>sM(es)) = (M = clinit \<or> sub_RIs es)"
 | "sub_RI({V:T; e}) = sub_RI e"
 | "sub_RI(e\<^sub>1;;e\<^sub>2) = (sub_RI e\<^sub>1 \<or> sub_RI e\<^sub>2)"
 | "sub_RI(if (b) e\<^sub>1 else e\<^sub>2) = (sub_RI b \<or> sub_RI e\<^sub>1 \<or> sub_RI e\<^sub>2)"
 | "sub_RI(while (b) e) = (sub_RI b \<or> sub_RI e)"
 | "sub_RI(throw e) = sub_RI e"
 | "sub_RI(try e\<^sub>1 catch(C V) e\<^sub>2) = (sub_RI e\<^sub>1 \<or> sub_RI e\<^sub>2)"
 | "sub_RI(INIT C (Cs,b) \<leftarrow> e) = True"
 | "sub_RI(RI (C,e);Cs \<leftarrow> e') = True"
 | "sub_RIs([]) = False"
 | "sub_RIs(e#es) = (sub_RI e \<or> sub_RIs es)"
 
 
 lemmas sub_RI_sub_RIs_induct = sub_RI.induct sub_RIs.induct
 
 lemma nsub_RIs_def[simp]:
  "\<not>sub_RIs es \<Longrightarrow> \<forall>e \<in> set es. \<not>sub_RI e"
  by(induct es, auto)
 
 lemma sub_RI_base:
  "e = INIT C (Cs, b) \<leftarrow> e' \<or> e = RI(C,e\<^sub>0);Cs \<leftarrow> e' \<Longrightarrow> sub_RI e"
  by(cases e, auto)
 
 lemma nsub_RI_Vals[simp]: "\<not>sub_RIs (map Val vs)"
  by(induct vs, auto)
 
 lemma lass_val_of_nsub_RI: "lass_val_of e = \<lfloor>a\<rfloor> \<Longrightarrow> \<not>sub_RI e"
  by(drule lass_val_of_spec, simp)
 
 
  \<comment> \<open> is not currently initializing class @{text C'} (point past checking flag) \<close>
 primrec not_init :: "cname \<Rightarrow> 'a exp \<Rightarrow> bool" and not_inits :: "cname \<Rightarrow> 'a exp list \<Rightarrow> bool" where
   "not_init C' (new C) = True"
 | "not_init C' (Cast C e) = not_init C' e"
 | "not_init C' (Val v) = True"
 | "not_init C' (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = (not_init C' e\<^sub>1 \<and> not_init C' e\<^sub>2)"
 | "not_init C' (Var V) = True"
 | "not_init C' (LAss V e) = not_init C' e"
 | "not_init C' (e\<bullet>F{D}) = not_init C' e"
 | "not_init C' (C\<bullet>\<^sub>sF{D}) = True"
 | "not_init C' (e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = (not_init C' e\<^sub>1 \<and> not_init C' e\<^sub>2)"
 | "not_init C' (C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = not_init C' e\<^sub>2"
 | "not_init C' (e\<bullet>M(es)) = (not_init C' e \<and> not_inits C' es)"
 | "not_init C' (C\<bullet>\<^sub>sM(es)) = not_inits C' es"
 | "not_init C' ({V:T; e}) = not_init C' e"
 | "not_init C' (e\<^sub>1;;e\<^sub>2) = (not_init C' e\<^sub>1 \<and> not_init C' e\<^sub>2)"
 | "not_init C' (if (b) e\<^sub>1 else e\<^sub>2) = (not_init C' b \<and> not_init C' e\<^sub>1 \<and> not_init C' e\<^sub>2)"
 | "not_init C' (while (b) e) = (not_init C' b \<and> not_init C' e)"
 | "not_init C' (throw e) = not_init C' e"
 | "not_init C' (try e\<^sub>1 catch(C V) e\<^sub>2) = (not_init C' e\<^sub>1 \<and> not_init C' e\<^sub>2)"
 | "not_init C' (INIT C (Cs,b) \<leftarrow> e) = ((b \<longrightarrow> Cs = Nil \<or> C' \<noteq> hd Cs) \<and> C' \<notin> set(tl Cs) \<and> not_init C' e)"
 | "not_init C' (RI (C,e);Cs \<leftarrow> e') = (C' \<notin> set (C#Cs) \<and> not_init C' e \<and> not_init C' e')"
 | "not_inits C' ([]) = True"
 | "not_inits C' (e#es) = (not_init C' e \<and> not_inits C' es)"
 
 lemma not_inits_def'[simp]:
  "not_inits C es \<Longrightarrow> \<forall>e \<in> set es. not_init C e"
  by(induct es, auto)
 
 lemma nsub_RIs_not_inits_aux: "\<forall>e \<in> set es. \<not>sub_RI e \<longrightarrow> not_init C e
   \<Longrightarrow> \<not>sub_RIs es \<Longrightarrow> not_inits C es"
  by(induct es, auto)
 
 lemma nsub_RI_not_init: "\<not>sub_RI e \<Longrightarrow> not_init C e"
 proof(induct e) qed(auto intro: nsub_RIs_not_inits_aux)
 
 lemma nsub_RIs_not_inits: "\<not>sub_RIs es \<Longrightarrow> not_inits C es"
-apply(rule nsub_RIs_not_inits_aux)
- apply(simp_all add: nsub_RI_not_init)
-done
+by(rule nsub_RIs_not_inits_aux) (simp_all add: nsub_RI_not_init)
 
 subsection\<open>Subexpressions\<close>
 
  \<comment> \<open> all strictly smaller subexpressions; does not include self \<close>
  primrec subexp :: "'a exp \<Rightarrow> 'a exp set" and subexps :: "'a exp list \<Rightarrow> 'a exp set" where
   "subexp(new C) = {}"
 | "subexp(Cast C e) = {e} \<union> subexp e"
 | "subexp(Val v) = {}"
 | "subexp(e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) = {e\<^sub>1, e\<^sub>2} \<union> subexp e\<^sub>1 \<union> subexp e\<^sub>2"
 | "subexp(Var V) = {}"
 | "subexp(LAss V e) = {e} \<union> subexp e"
 | "subexp(e\<bullet>F{D}) = {e} \<union> subexp e"
 | "subexp(C\<bullet>\<^sub>sF{D}) = {}"
 | "subexp(e\<^sub>1\<bullet>F{D}:=e\<^sub>2) = {e\<^sub>1, e\<^sub>2} \<union> subexp e\<^sub>1 \<union> subexp e\<^sub>2"
 | "subexp(C\<bullet>\<^sub>sF{D}:=e\<^sub>2) = {e\<^sub>2} \<union>subexp e\<^sub>2"
 | "subexp(e\<bullet>M(es)) = {e} \<union> set es \<union> subexp e \<union> subexps es"
 | "subexp(C\<bullet>\<^sub>sM(es)) = set es \<union> subexps es"
 | "subexp({V:T; e}) = {e} \<union> subexp e"
 | "subexp(e\<^sub>1;;e\<^sub>2) = {e\<^sub>1, e\<^sub>2} \<union> subexp e\<^sub>1 \<union> subexp e\<^sub>2"
 | "subexp(if (b) e\<^sub>1 else e\<^sub>2) = {b, e\<^sub>1, e\<^sub>2} \<union> subexp b \<union> subexp e\<^sub>1 \<union> subexp e\<^sub>2"
 | "subexp(while (b) e) = {b, e} \<union> subexp b \<union> subexp e"
 | "subexp(throw e) = {e} \<union> subexp e"
 | "subexp(try e\<^sub>1 catch(C V) e\<^sub>2) = {e\<^sub>1, e\<^sub>2} \<union> subexp e\<^sub>1 \<union> subexp e\<^sub>2"
 | "subexp(INIT C (Cs,b) \<leftarrow> e) = {e} \<union> subexp e"
 | "subexp(RI (C,e);Cs \<leftarrow> e') = {e, e'} \<union> subexp e \<union> subexp e'"
 | "subexps([]) = {}"
 | "subexps(e#es) = {e} \<union> subexp e \<union> subexps es"
 
 
 lemmas subexp_subexps_induct = subexp.induct subexps.induct
 
 abbreviation subexp_of :: "'a exp \<Rightarrow> 'a exp \<Rightarrow> bool" where
  "subexp_of e e' \<equiv> e \<in> subexp e'"
 
 lemma subexp_size_le:
  "(e' \<in> subexp e \<longrightarrow> size e' < size e) \<and> (e' \<in> subexps es \<longrightarrow> size e' < size_list size es)"
 proof(induct rule: subexp_subexps.induct)
   case Call:11 then show ?case using not_less_eq size_list_estimation by fastforce
 next
   case SCall:12 then show ?case using not_less_eq size_list_estimation by fastforce
 qed(auto)
 
 lemma subexps_def2: "subexps es = set es \<union> (\<Union>e \<in> set es. subexp e)" by(induct es, auto)
 
  \<comment> \<open> strong induction \<close>
 lemma shows subexp_induct[consumes 1]: 
 "(\<And>e. subexp e = {} \<Longrightarrow> R e) \<Longrightarrow> (\<And>e. (\<And>e'. e' \<in> subexp e \<Longrightarrow> R e') \<Longrightarrow> R e)
    \<Longrightarrow> (\<And>es. (\<And>e'. e' \<in> subexps es \<Longrightarrow> R e') \<Longrightarrow> Rs es) \<Longrightarrow> (\<forall>e'. e' \<in> subexp e \<longrightarrow> R e') \<and> R e"
 and subexps_induct[consumes 1]:
  "(\<And>es. subexps es = {} \<Longrightarrow> Rs es) \<Longrightarrow> (\<And>e. (\<And>e'. e' \<in> subexp e \<Longrightarrow> R e') \<Longrightarrow> R e)
    \<Longrightarrow> (\<And>es. (\<And>e'. e' \<in> subexps es \<Longrightarrow> R e') \<Longrightarrow> Rs es) \<Longrightarrow> (\<forall>e'. e' \<in> subexps es \<longrightarrow> R e') \<and> Rs es"
 proof(induct rule: subexp_subexps_induct)
   case (Cast x1 x2)
   then have "(\<forall>e'. subexp_of e' x2 \<longrightarrow> R e') \<and> R x2" by fast
   then have "(\<forall>e'. subexp_of e' (Cast x1 x2) \<longrightarrow> R e')" by auto
   then show ?case using Cast.prems(2) by fast
 next
   case (BinOp x1 x2 x3)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. subexp_of e' x3 \<longrightarrow> R e') \<and> R x3"
    by fast+
   then have "(\<forall>e'. subexp_of e' (x1 \<guillemotleft>x2\<guillemotright> x3) \<longrightarrow> R e')" by auto
   then show ?case using BinOp.prems(2) by fast
 next
   case (LAss x1 x2)
   then have "(\<forall>e'. subexp_of e' x2 \<longrightarrow> R e') \<and> R x2" by fast
   then have "(\<forall>e'. subexp_of e' (LAss x1 x2) \<longrightarrow> R e')" by auto
   then show ?case using LAss.prems(2) by fast
 next
   case (FAcc x1 x2 x3)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" by fast
   then have "(\<forall>e'. subexp_of e' (x1\<bullet>x2{x3}) \<longrightarrow> R e')" by auto
   then show ?case using FAcc.prems(2) by fast
 next
   case (FAss x1 x2 x3 x4)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. subexp_of e' x4 \<longrightarrow> R e') \<and> R x4"
    by fast+
   then have "(\<forall>e'. subexp_of e' (x1\<bullet>x2{x3} := x4) \<longrightarrow> R e')" by auto
   then show ?case using FAss.prems(2) by fast
 next
   case (SFAss x1 x2 x3 x4)
   then have "(\<forall>e'. subexp_of e' x4 \<longrightarrow> R e') \<and> R x4" by fast
   then have "(\<forall>e'. subexp_of e' (x1\<bullet>\<^sub>sx2{x3} := x4) \<longrightarrow> R e')" by auto
   then show ?case using SFAss.prems(2) by fast
 next
   case (Call x1 x2 x3)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. e' \<in> subexps x3 \<longrightarrow> R e') \<and> Rs x3"
    by fast+
   then have "(\<forall>e'. subexp_of e' (x1\<bullet>x2(x3)) \<longrightarrow> R e')" using subexps_def2 by auto
   then show ?case using Call.prems(2) by fast
 next
   case (SCall x1 x2 x3)
   then have "(\<forall>e'. e' \<in> subexps x3 \<longrightarrow> R e') \<and> Rs x3" by fast
   then have "(\<forall>e'. subexp_of e' (x1\<bullet>\<^sub>sx2(x3)) \<longrightarrow> R e')" using subexps_def2 by auto
   then show ?case using SCall.prems(2) by fast
 next
   case (Block x1 x2 x3)
   then have "(\<forall>e'. subexp_of e' x3 \<longrightarrow> R e') \<and> R x3" by fast
   then have "(\<forall>e'. subexp_of e' {x1:x2; x3} \<longrightarrow> R e')" by auto
   then show ?case using Block.prems(2) by fast
 next
   case (Seq x1 x2)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. subexp_of e' x2 \<longrightarrow> R e') \<and> R x2"
    by fast+
   then have "(\<forall>e'. subexp_of e' (x1;; x2) \<longrightarrow> R e')" by auto
   then show ?case using Seq.prems(2) by fast
 next
   case (Cond x1 x2 x3)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. subexp_of e' x2 \<longrightarrow> R e') \<and> R x2"
     and "(\<forall>e'. subexp_of e' x3 \<longrightarrow> R e') \<and> R x3" by fast+
   then have "(\<forall>e'. subexp_of e' (if (x1) x2 else x3) \<longrightarrow> R e')" by auto
   then show ?case using Cond.prems(2) by fast
 next
   case (While x1 x2)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. subexp_of e' x2 \<longrightarrow> R e') \<and> R x2"
    by fast+
   then have "(\<forall>e'. subexp_of e' (while (x1) x2) \<longrightarrow> R e')" by auto
   then show ?case using While.prems(2) by fast
 next
   case (throw x)
   then have "(\<forall>e'. subexp_of e' x \<longrightarrow> R e') \<and> R x" by fast
   then have "(\<forall>e'. subexp_of e' (throw x) \<longrightarrow> R e')" by auto
   then show ?case using throw.prems(2) by fast
 next
   case (TryCatch x1 x2 x3 x4)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. subexp_of e' x4 \<longrightarrow> R e') \<and> R x4"
    by fast+
   then have "(\<forall>e'. subexp_of e' (try x1 catch(x2 x3) x4) \<longrightarrow> R e')" by auto
   then show ?case using TryCatch.prems(2) by fast
 next
   case (INIT x1 x2 x3 x4)
   then have "(\<forall>e'. subexp_of e' x4 \<longrightarrow> R e') \<and> R x4" by fast
   then have "(\<forall>e'. subexp_of e' (INIT x1 (x2,x3) \<leftarrow> x4) \<longrightarrow> R e')" by auto
   then show ?case using INIT.prems(2) by fast
 next
   case (RI x1 x2 x3 x4)
   then have "(\<forall>e'. subexp_of e' x2 \<longrightarrow> R e') \<and> R x2" and "(\<forall>e'. subexp_of e' x4 \<longrightarrow> R e') \<and> R x4"
    by fast+
   then have "(\<forall>e'. subexp_of e' (RI (x1,x2) ; x3 \<leftarrow> x4) \<longrightarrow> R e')" by auto
   then show ?case using RI.prems(2) by fast
 next
   case (Cons_exp x1 x2)
   then have "(\<forall>e'. subexp_of e' x1 \<longrightarrow> R e') \<and> R x1" and "(\<forall>e'. e' \<in> subexps x2 \<longrightarrow> R e') \<and> Rs x2"
    by fast+
   then have "(\<forall>e'. e' \<in> subexps (x1 # x2) \<longrightarrow> R e')" using subexps_def2 by auto
   then show ?case using Cons_exp.prems(3) by fast
 qed(auto)
 
 
 subsection"Final expressions"
 (* these definitions and most of the lemmas were in BigStep.thy in the original Jinja *)
 
 definition final :: "'a exp \<Rightarrow> bool"
 where
   "final e  \<equiv>  (\<exists>v. e = Val v) \<or> (\<exists>a. e = Throw a)"
 
 definition finals:: "'a exp list \<Rightarrow> bool"
 where
   "finals es  \<equiv>  (\<exists>vs. es = map Val vs) \<or> (\<exists>vs a es'. es = map Val vs @ Throw a # es')"
 
 lemma [simp]: "final(Val v)"
 (*<*)by(simp add:final_def)(*>*)
 
 lemma [simp]: "final(throw e) = (\<exists>a. e = addr a)"
 (*<*)by(simp add:final_def)(*>*)
 
 lemma finalE: "\<lbrakk> final e;  \<And>v. e = Val v \<Longrightarrow> R;  \<And>a. e = Throw a \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
 (*<*)by(auto simp:final_def)(*>*)
 
 lemma final_fv[iff]: "final e \<Longrightarrow> fv e = {}"
  by (auto simp: final_def)
 
 lemma finalsE:
  "\<lbrakk> finals es;  \<And>vs. es = map Val vs \<Longrightarrow> R;  \<And>vs a es'. es = map Val vs @ Throw a # es' \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
 (*<*)by(auto simp:finals_def)(*>*)
 
 lemma [iff]: "finals []"
 (*<*)by(simp add:finals_def)(*>*)
 
 lemma [iff]: "finals (Val v # es) = finals es"
 (*<*)
-apply(clarsimp simp add: finals_def)
-apply(rule iffI)
- apply(erule disjE)
-  apply simp
- apply(rule disjI2)
- apply clarsimp
- apply(case_tac vs)
-  apply simp
- apply fastforce
-apply(erule disjE)
- apply clarsimp
-apply(rule disjI2)
-apply clarsimp
-apply(rule_tac x = "v#vs" in exI)
-apply simp
-done
+proof(rule iffI)
+  assume "finals (Val v # es)"
+  moreover {
+    fix vs a es'
+    assume "\<forall>vs a es'. es \<noteq> map Val vs @ Throw a # es'"
+      and "Val v # es = map Val vs @ Throw a # es'"
+    then have "\<exists>vs. es = map Val vs" by(case_tac vs; simp)
+  }
+  ultimately show "finals es" by(clarsimp simp add: finals_def)
+next
+  assume "finals es"
+  moreover {
+    fix vs a es'
+    assume "es = map Val vs @ Throw a # es'"
+    then have "\<exists>vs' a' es''. Val v # map Val vs @ Throw a # es' = map Val vs' @ Throw a' # es''"
+      by(rule_tac x = "v#vs" in exI) simp
+  }
+  ultimately show "finals (Val v # es)" by(clarsimp simp add: finals_def)
+qed
 (*>*)
 
 lemma finals_app_map[iff]: "finals (map Val vs @ es) = finals es"
 (*<*)by(induct_tac vs, auto)(*>*)
 
 lemma [iff]: "finals (map Val vs)"
 (*<*)using finals_app_map[of vs "[]"]by(simp)(*>*)
 
 lemma [iff]: "finals (throw e # es) = (\<exists>a. e = addr a)"
 (*<*)
-apply(simp add:finals_def)
-apply(rule iffI)
- apply clarsimp
- apply(case_tac vs)
-  apply simp
- apply fastforce
-apply clarsimp
-apply(rule_tac x = "[]" in exI)
-apply simp
-done
+proof(rule iffI)
+  assume "finals (throw e # es)"
+  moreover {
+    fix vs a es'
+    assume "throw e # es = map Val vs @ Throw a # es'"
+    then have "\<exists>a. e = addr a" by(case_tac vs; simp)
+  }
+  ultimately show "\<exists>a. e = addr a" by(clarsimp simp add: finals_def)
+next
+  assume "\<exists>a. e = addr a"
+  moreover {
+    fix vs a es'
+    assume "e = addr a"
+    then have "\<exists>vs aa es'. Throw a # es = map Val vs @ Throw aa # es'"
+      by(rule_tac x = "[]" in exI) simp
+  }
+  ultimately show "finals (throw e # es)" by(clarsimp simp add: finals_def)
+qed
 (*>*)
 
 lemma not_finals_ConsI: "\<not> final e \<Longrightarrow> \<not> finals(e#es)"
- (*<*)
-apply(clarsimp simp add:finals_def final_def)
-apply(case_tac vs)
-apply auto
-done
+(*<*)
+proof -
+  assume "\<not> final e"
+  moreover {
+    fix vs a es'
+    assume "\<forall>v. e \<noteq> Val v" and "\<forall>a. e \<noteq> Throw a"
+    then have "e # es \<noteq> map Val vs @ Throw a # es'" by(case_tac vs; simp)
+  }
+  ultimately show ?thesis by(clarsimp simp add:finals_def final_def)
+qed
 (*>*)
 
 lemma not_finals_ConsI2: "e = Val v \<Longrightarrow> \<not> finals es \<Longrightarrow> \<not> finals(e#es)"
- (*<*)
-apply(clarsimp simp add:finals_def final_def)
-apply(case_tac vs)
-apply auto
-done
+(*<*)
+proof -
+  assume [simp]: "e = Val v" and "\<not> finals es"
+  moreover {
+    fix vs a es'
+    assume "\<forall>vs. es \<noteq> map Val vs" and "\<forall>vs a es'. es \<noteq> map Val vs @ Throw a # es'"
+    then have "e # es \<noteq> map Val vs @ Throw a # es'" by(case_tac vs; simp)
+  }
+  ultimately show ?thesis by(clarsimp simp add:finals_def final_def)
+qed
 (*>*)
 
 
 end
diff --git a/thys/JinjaDCI/J/SmallStep.thy b/thys/JinjaDCI/J/SmallStep.thy
--- a/thys/JinjaDCI/J/SmallStep.thy
+++ b/thys/JinjaDCI/J/SmallStep.thy
@@ -1,634 +1,646 @@
 (*  Title:      JinjaDCI/J/SmallStep.thy
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/SmallStep.thy by Tobias Nipkow
 *)
 
 section \<open> Small Step Semantics \<close>
 
 theory SmallStep
 imports Expr State WWellForm
 begin
 
 fun blocks :: "vname list * ty list * val list * expr \<Rightarrow> expr"
 where
  "blocks(V#Vs, T#Ts, v#vs, e) = {V:T := Val v; blocks(Vs,Ts,vs,e)}"
 |"blocks([],[],[],e) = e"
 
 lemmas blocks_induct = blocks.induct[split_format (complete)]
 
 lemma [simp]:
   "\<lbrakk> size vs = size Vs; size Ts = size Vs \<rbrakk> \<Longrightarrow> fv(blocks(Vs,Ts,vs,e)) = fv e - set Vs"
 (*<*)
 by (induct rule:blocks_induct) auto
 (*>*)
 
 
 lemma sub_RI_blocks_body[iff]: "length vs = length pns \<Longrightarrow> length Ts = length pns
  \<Longrightarrow> sub_RI (blocks (pns, Ts, vs, body)) \<longleftrightarrow> sub_RI body"
 proof(induct pns arbitrary: Ts vs)
   case Nil then show ?case by simp
 next
   case Cons then show ?case by(cases vs; cases Ts) auto
 qed
 
 
 definition assigned :: "'a \<Rightarrow> 'a exp \<Rightarrow> bool"
 where
   "assigned V e  \<equiv>  \<exists>v e'. e = (V := Val v;; e')"
 
 \<comment> \<open> expression is okay to go the right side of @{text INIT} or @{text "RI \<leftarrow>"}
  or to have indicator Boolean be True (in latter case, given that class is
  also verified initialized) \<close>
 fun icheck :: "'m prog \<Rightarrow> cname \<Rightarrow> 'a exp \<Rightarrow> bool" where
 "icheck P C' (new C) = (C' = C)" |
 "icheck P D' (C\<bullet>\<^sub>sF{D}) = ((D' = D) \<and> (\<exists>T. P \<turnstile> C has F,Static:T in D))" |
 "icheck P D' (C\<bullet>\<^sub>sF{D}:=(Val v)) = ((D' = D) \<and> (\<exists>T. P \<turnstile> C has F,Static:T in D))" |
 "icheck P D (C\<bullet>\<^sub>sM(es)) = ((\<exists>vs. es = map Val vs) \<and> (\<exists>Ts T m. P \<turnstile> C sees M,Static:Ts\<rightarrow>T = m in D))" |
 "icheck P _ _ = False"
 
 lemma nicheck_SFAss_nonVal: "val_of e\<^sub>2 = None \<Longrightarrow> \<not>icheck P C' (C\<bullet>\<^sub>sF{D} := (e\<^sub>2::'a exp))"
  by(rule notI, cases e\<^sub>2, auto)
 
 inductive_set
   red  :: "J_prog \<Rightarrow> ((expr \<times> state \<times> bool) \<times> (expr \<times> state \<times> bool)) set"
   and reds  :: "J_prog \<Rightarrow> ((expr list \<times> state \<times> bool) \<times> (expr list \<times> state \<times> bool)) set"
   and red' :: "J_prog \<Rightarrow> expr \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> expr \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool"
           ("_ \<turnstile> ((1\<langle>_,/_,/_\<rangle>) \<rightarrow>/ (1\<langle>_,/_,/_\<rangle>))" [51,0,0,0,0,0,0] 81)
   and reds' :: "J_prog \<Rightarrow> expr list \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> expr list \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool"
           ("_ \<turnstile> ((1\<langle>_,/_,/_\<rangle>) [\<rightarrow>]/ (1\<langle>_,/_,/_\<rangle>))" [51,0,0,0,0,0,0] 81)
   for P :: J_prog
 where
 
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<equiv> ((e,s,b), e',s',b') \<in> red P"
 | "P \<turnstile> \<langle>es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle> \<equiv> ((es,s,b), es',s',b') \<in> reds P"
 
 | RedNew:
   "\<lbrakk> new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>blank P C) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>new C, (h,l,sh), True\<rangle> \<rightarrow> \<langle>addr a, (h',l,sh), False\<rangle>"
 
 | RedNewFail:
   "\<lbrakk> new_Addr h = None; is_class P C \<rbrakk> \<Longrightarrow>
   P \<turnstile> \<langle>new C, (h,l,sh), True\<rangle> \<rightarrow> \<langle>THROW OutOfMemory, (h,l,sh), False\<rangle>"
 
 | NewInitDoneRed:
   "sh C = Some (sfs, Done) \<Longrightarrow>
   P \<turnstile> \<langle>new C, (h,l,sh), False\<rangle> \<rightarrow> \<langle>new C, (h,l,sh), True\<rangle>"
 
 | NewInitRed:
   "\<lbrakk> \<nexists>sfs. sh C = Some (sfs, Done); is_class P C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>new C,(h,l,sh),False\<rangle> \<rightarrow> \<langle>INIT C ([C],False) \<leftarrow> new C,(h,l,sh),False\<rangle>"
 
 | CastRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>Cast C e, s, b\<rangle> \<rightarrow> \<langle>Cast C e', s', b'\<rangle>"
 
 | RedCastNull:
   "P \<turnstile> \<langle>Cast C null, s, b\<rangle> \<rightarrow> \<langle>null,s,b\<rangle>"
 
 | RedCast:
  "\<lbrakk> h a = Some(D,fs); P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>Cast C (addr a), (h,l,sh), b\<rangle> \<rightarrow> \<langle>addr a, (h,l,sh), b\<rangle>"
 
 | RedCastFail:
   "\<lbrakk> h a = Some(D,fs); \<not> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>Cast C (addr a), (h,l,sh), b\<rangle> \<rightarrow> \<langle>THROW ClassCast, (h,l,sh), b\<rangle>"
 
 | BinOpRed1:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e \<guillemotleft>bop\<guillemotright> e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>e' \<guillemotleft>bop\<guillemotright> e\<^sub>2, s', b'\<rangle>"
 
 | BinOpRed2:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>(Val v\<^sub>1) \<guillemotleft>bop\<guillemotright> e, s, b\<rangle> \<rightarrow> \<langle>(Val v\<^sub>1) \<guillemotleft>bop\<guillemotright> e', s', b'\<rangle>"
 
 | RedBinOp:
   "binop(bop,v\<^sub>1,v\<^sub>2) = Some v \<Longrightarrow>
   P \<turnstile> \<langle>(Val v\<^sub>1) \<guillemotleft>bop\<guillemotright> (Val v\<^sub>2), s, b\<rangle> \<rightarrow> \<langle>Val v,s,b\<rangle>"
 
 | RedVar:
   "l V = Some v \<Longrightarrow>
   P \<turnstile> \<langle>Var V,(h,l,sh),b\<rangle> \<rightarrow> \<langle>Val v,(h,l,sh),b\<rangle>"
 
 | LAssRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>V:=e,s,b\<rangle> \<rightarrow> \<langle>V:=e',s',b'\<rangle>"
 
 | RedLAss:
   "P \<turnstile> \<langle>V:=(Val v), (h,l,sh), b\<rangle> \<rightarrow> \<langle>unit, (h,l(V\<mapsto>v),sh), b\<rangle>"
 
 | FAccRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<bullet>F{D}, s, b\<rangle> \<rightarrow> \<langle>e'\<bullet>F{D}, s', b'\<rangle>"
 
 | RedFAcc:
   "\<lbrakk> h a = Some(C,fs); fs(F,D) = Some v;
      P \<turnstile> C has F,NonStatic:t in D \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>F{D}, (h,l,sh), b\<rangle> \<rightarrow> \<langle>Val v,(h,l,sh),b\<rangle>"
 
 | RedFAccNull:
   "P \<turnstile> \<langle>null\<bullet>F{D}, s, b\<rangle> \<rightarrow> \<langle>THROW NullPointer, s, b\<rangle>"
 
 | RedFAccNone:
   "\<lbrakk> h a = Some(C,fs); \<not>(\<exists>b t. P \<turnstile> C has F,b:t in D) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>F{D},(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW NoSuchFieldError,(h,l,sh),b\<rangle>"
 
 | RedFAccStatic:
   "\<lbrakk> h a = Some(C,fs); P \<turnstile> C has F,Static:t in D \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>F{D},(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW IncompatibleClassChangeError,(h,l,sh),b\<rangle>"
 
 | RedSFAcc:
   "\<lbrakk> P \<turnstile> C has F,Static:t in D;
      sh D = Some (sfs,i);
      sfs F = Some v \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D},(h,l,sh),True\<rangle> \<rightarrow> \<langle>Val v,(h,l,sh),False\<rangle>"
 
 | SFAccInitDoneRed:
   "\<lbrakk> P \<turnstile> C has F,Static:t in D;
      sh D = Some (sfs,Done) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D},(h,l,sh),False\<rangle> \<rightarrow> \<langle>C\<bullet>\<^sub>sF{D},(h,l,sh),True\<rangle>"
 
 | SFAccInitRed:
   "\<lbrakk> P \<turnstile> C has F,Static:t in D;
      \<nexists>sfs. sh D = Some (sfs,Done) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D},(h,l,sh),False\<rangle> \<rightarrow> \<langle>INIT D ([D],False) \<leftarrow> C\<bullet>\<^sub>sF{D},(h,l,sh),False\<rangle>"
 
 | RedSFAccNone:
   "\<not>(\<exists>b t. P \<turnstile> C has F,b:t in D)
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D},(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW NoSuchFieldError,(h,l,sh),False\<rangle>"
 
 | RedSFAccNonStatic:
   "P \<turnstile> C has F,NonStatic:t in D
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D},(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW IncompatibleClassChangeError,(h,l,sh),False\<rangle>"
 
 | FAssRed1:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<bullet>F{D}:=e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>e'\<bullet>F{D}:=e\<^sub>2, s', b'\<rangle>"
 
 | FAssRed2:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>Val v\<bullet>F{D}:=e, s, b\<rangle> \<rightarrow> \<langle>Val v\<bullet>F{D}:=e', s', b'\<rangle>"
 
 | RedFAss:
   "\<lbrakk> P \<turnstile> C has F,NonStatic:t in D; h a = Some(C,fs) \<rbrakk> \<Longrightarrow>
   P \<turnstile> \<langle>(addr a)\<bullet>F{D}:=(Val v), (h,l,sh), b\<rangle> \<rightarrow> \<langle>unit, (h(a \<mapsto> (C,fs((F,D) \<mapsto> v))),l,sh), b\<rangle>"
 
 | RedFAssNull:
   "P \<turnstile> \<langle>null\<bullet>F{D}:=Val v, s, b\<rangle> \<rightarrow> \<langle>THROW NullPointer, s, b\<rangle>"
 
 | RedFAssNone:
   "\<lbrakk> h a = Some(C,fs); \<not>(\<exists>b t. P \<turnstile> C has F,b:t in D) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>F{D}:=(Val v),(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW NoSuchFieldError,(h,l,sh),b\<rangle>"
 
 | RedFAssStatic:
   "\<lbrakk> h a = Some(C,fs); P \<turnstile> C has F,Static:t in D \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>F{D}:=(Val v),(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW IncompatibleClassChangeError,(h,l,sh),b\<rangle>"
 
 | SFAssRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D}:=e, s, b\<rangle> \<rightarrow> \<langle>C\<bullet>\<^sub>sF{D}:=e', s', b'\<rangle>"
 
 | RedSFAss:
   "\<lbrakk> P \<turnstile> C has F,Static:t in D;
      sh D = Some(sfs,i);
      sfs' = sfs(F\<mapsto>v); sh' = sh(D\<mapsto>(sfs',i)) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D}:=(Val v),(h,l,sh),True\<rangle> \<rightarrow> \<langle>unit,(h,l,sh'),False\<rangle>"
 
 | SFAssInitDoneRed:
   "\<lbrakk> P \<turnstile> C has F,Static:t in D;
      sh D = Some(sfs,Done) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D}:=(Val v),(h,l,sh),False\<rangle> \<rightarrow> \<langle>C\<bullet>\<^sub>sF{D}:=(Val v),(h,l,sh),True\<rangle>"
 
 | SFAssInitRed:
   "\<lbrakk> P \<turnstile> C has F,Static:t in D;
      \<nexists>sfs. sh D = Some(sfs,Done) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D}:=(Val v),(h,l,sh),False\<rangle> \<rightarrow> \<langle>INIT D ([D],False)\<leftarrow> C\<bullet>\<^sub>sF{D}:=(Val v),(h,l,sh),False\<rangle>"
 
 | RedSFAssNone:
   "\<not>(\<exists>b t. P \<turnstile> C has F,b:t in D)
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D}:=(Val v),s,b\<rangle> \<rightarrow> \<langle>THROW NoSuchFieldError,s,False\<rangle>"
 
 | RedSFAssNonStatic:
   "P \<turnstile> C has F,NonStatic:t in D
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D}:=(Val v),s,b\<rangle> \<rightarrow> \<langle>THROW IncompatibleClassChangeError,s,False\<rangle>"
 
 | CallObj:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e\<bullet>M(es),s,b\<rangle> \<rightarrow> \<langle>e'\<bullet>M(es),s',b'\<rangle>"
 
 | CallParams:
   "P \<turnstile> \<langle>es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>(Val v)\<bullet>M(es),s,b\<rangle> \<rightarrow> \<langle>(Val v)\<bullet>M(es'),s',b'\<rangle>"
 
 | RedCall:
   "\<lbrakk> h a = Some(C,fs); P \<turnstile> C sees M,NonStatic:Ts\<rightarrow>T = (pns,body) in D; size vs = size pns; size Ts = size pns \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>M(map Val vs), (h,l,sh), b\<rangle> \<rightarrow> \<langle>blocks(this#pns, Class D#Ts, Addr a#vs, body), (h,l,sh), b\<rangle>"
 
 | RedCallNull:
   "P \<turnstile> \<langle>null\<bullet>M(map Val vs),s,b\<rangle> \<rightarrow> \<langle>THROW NullPointer,s,b\<rangle>"
 
 | RedCallNone:
   "\<lbrakk> h a = Some(C,fs); \<not>(\<exists>b Ts T m D. P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in D) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>M(map Val vs),(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW NoSuchMethodError,(h,l,sh),b\<rangle>"
 
 | RedCallStatic:
   "\<lbrakk> h a = Some(C,fs); P \<turnstile> C sees M,Static:Ts\<rightarrow>T = m in D \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>(addr a)\<bullet>M(map Val vs),(h,l,sh),b\<rangle> \<rightarrow> \<langle>THROW IncompatibleClassChangeError,(h,l,sh),b\<rangle>"
 
 | SCallParams:
   "P \<turnstile> \<langle>es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>C\<bullet>\<^sub>sM(es),s,b\<rangle> \<rightarrow> \<langle>C\<bullet>\<^sub>sM(es'),s',b'\<rangle>"
 
 | RedSCall:
   "\<lbrakk> P \<turnstile> C sees M,Static:Ts\<rightarrow>T = (pns,body) in D;
      length vs = length pns; size Ts = size pns \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sM(map Val vs),s,True\<rangle> \<rightarrow> \<langle>blocks(pns, Ts, vs, body), s, False\<rangle>"
 
 | SCallInitDoneRed:
   "\<lbrakk> P \<turnstile> C sees M,Static:Ts\<rightarrow>T = (pns,body) in D;
      sh D = Some(sfs,Done) \<or> (M = clinit \<and> sh D = Some(sfs,Processing)) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sM(map Val vs),(h,l,sh), False\<rangle> \<rightarrow> \<langle>C\<bullet>\<^sub>sM(map Val vs),(h,l,sh), True\<rangle>"
 
 | SCallInitRed:
   "\<lbrakk> P \<turnstile> C sees M,Static:Ts\<rightarrow>T = (pns,body) in D;
      \<nexists>sfs. sh D = Some(sfs,Done); M \<noteq> clinit \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sM(map Val vs),(h,l,sh), False\<rangle> \<rightarrow> \<langle>INIT D ([D],False) \<leftarrow> C\<bullet>\<^sub>sM(map Val vs),(h,l,sh),False\<rangle>"
 
 | RedSCallNone:
   "\<lbrakk> \<not>(\<exists>b Ts T m D. P \<turnstile> C sees M,b:Ts\<rightarrow>T = m in D) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sM(map Val vs),s,b\<rangle> \<rightarrow> \<langle>THROW NoSuchMethodError,s,False\<rangle>"
 
 | RedSCallNonStatic:
   "\<lbrakk> P \<turnstile> C sees M,NonStatic:Ts\<rightarrow>T = m in D \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sM(map Val vs),s,b\<rangle> \<rightarrow> \<langle>THROW IncompatibleClassChangeError,s,False\<rangle>"
 
 | BlockRedNone:
   "\<lbrakk> P \<turnstile> \<langle>e, (h,l(V:=None),sh), b\<rangle> \<rightarrow> \<langle>e', (h',l',sh'), b'\<rangle>; l' V = None; \<not> assigned V e \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>{V:T; e}, (h,l,sh), b\<rangle> \<rightarrow> \<langle>{V:T; e'}, (h',l'(V := l V),sh'), b'\<rangle>"
 
 | BlockRedSome:
   "\<lbrakk> P \<turnstile> \<langle>e, (h,l(V:=None),sh), b\<rangle> \<rightarrow> \<langle>e', (h',l',sh'), b'\<rangle>; l' V = Some v;\<not> assigned V e \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>{V:T; e}, (h,l,sh), b\<rangle> \<rightarrow> \<langle>{V:T := Val v; e'}, (h',l'(V := l V),sh'), b'\<rangle>"
 
 | InitBlockRed:
   "\<lbrakk> P \<turnstile> \<langle>e, (h,l(V\<mapsto>v),sh), b\<rangle> \<rightarrow> \<langle>e', (h',l',sh'), b'\<rangle>; l' V = Some v' \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>{V:T := Val v; e}, (h,l,sh), b\<rangle> \<rightarrow> \<langle>{V:T := Val v'; e'}, (h',l'(V := l V),sh'), b'\<rangle>"
 
 | RedBlock:
   "P \<turnstile> \<langle>{V:T; Val u}, s, b\<rangle> \<rightarrow> \<langle>Val u, s, b\<rangle>"
 
 | RedInitBlock:
   "P \<turnstile> \<langle>{V:T := Val v; Val u}, s, b\<rangle> \<rightarrow> \<langle>Val u, s, b\<rangle>"
 
 | SeqRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e;;e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>e';;e\<^sub>2, s', b'\<rangle>"
 
 | RedSeq:
   "P \<turnstile> \<langle>(Val v);;e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>e\<^sub>2, s, b\<rangle>"
 
 | CondRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>if (e) e\<^sub>1 else e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>if (e') e\<^sub>1 else e\<^sub>2, s', b'\<rangle>"
 
 | RedCondT:
   "P \<turnstile> \<langle>if (true) e\<^sub>1 else e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>e\<^sub>1, s, b\<rangle>"
 
 | RedCondF:
   "P \<turnstile> \<langle>if (false) e\<^sub>1 else e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>e\<^sub>2, s, b\<rangle>"
 
 | RedWhile:
   "P \<turnstile> \<langle>while(b) c, s, b'\<rangle> \<rightarrow> \<langle>if(b) (c;;while(b) c) else unit, s, b'\<rangle>"
 
 | ThrowRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>throw e, s, b\<rangle> \<rightarrow> \<langle>throw e', s', b'\<rangle>"
 
 | RedThrowNull:
   "P \<turnstile> \<langle>throw null, s, b\<rangle> \<rightarrow> \<langle>THROW NullPointer, s, b\<rangle>"
 
 | TryRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>try e catch(C V) e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>try e' catch(C V) e\<^sub>2, s', b'\<rangle>"
 
 | RedTry:
   "P \<turnstile> \<langle>try (Val v) catch(C V) e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>Val v, s, b\<rangle>"
 
 | RedTryCatch:
   "\<lbrakk> hp s a = Some(D,fs); P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>try (Throw a) catch(C V) e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>{V:Class C := addr a; e\<^sub>2}, s, b\<rangle>"
 
 | RedTryFail:
   "\<lbrakk> hp s a = Some(D,fs); \<not> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>try (Throw a) catch(C V) e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>Throw a, s, b\<rangle>"
 
 | ListRed1:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>e#es,s,b\<rangle> [\<rightarrow>] \<langle>e'#es,s',b'\<rangle>"
 
 | ListRed2:
   "P \<turnstile> \<langle>es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>Val v # es,s,b\<rangle> [\<rightarrow>] \<langle>Val v # es',s',b'\<rangle>"
 
 \<comment> \<open>Initialization procedure\<close>
 
 | RedInit:
   "\<not>sub_RI e \<Longrightarrow> P \<turnstile> \<langle>INIT C (Nil,b) \<leftarrow> e,s,b'\<rangle> \<rightarrow> \<langle>e,s,icheck P C e\<rangle>"
 
 | InitNoneRed:
   "sh C = None
   \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh(C \<mapsto> (sblank P C, Prepared))),b\<rangle>"
 
 | RedInitDone:
   "sh C = Some(sfs,Done)
   \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>INIT C' (Cs,True) \<leftarrow> e,(h,l,sh),b\<rangle>"
 
 | RedInitProcessing:
   "sh C = Some(sfs,Processing)
   \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>INIT C' (Cs,True) \<leftarrow> e,(h,l,sh),b\<rangle>"
 
 | RedInitError:
   "sh C = Some(sfs,Error)
   \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>RI (C,THROW NoClassDefFoundError);Cs \<leftarrow> e,(h,l,sh),b\<rangle>"
 
 | InitObjectRed:
   "\<lbrakk> sh C = Some(sfs,Prepared);
      C = Object;
      sh' = sh(C \<mapsto> (sfs,Processing)) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>INIT C' (C#Cs,True) \<leftarrow> e,(h,l,sh'),b\<rangle>"
 
 | InitNonObjectSuperRed:
   "\<lbrakk> sh C = Some(sfs,Prepared);
      C \<noteq> Object;
      class P C = Some (D,r);
      sh' = sh(C \<mapsto> (sfs,Processing)) \<rbrakk>
   \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>INIT C' (D#C#Cs,False) \<leftarrow> e,(h,l,sh'),b\<rangle>"
 
 | RedInitRInit:
   "P \<turnstile> \<langle>INIT C' (C#Cs,True) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>RI (C,C\<bullet>\<^sub>sclinit([]));Cs \<leftarrow> e,(h,l,sh),b\<rangle>"
 
 | RInitRed:
   "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle> \<Longrightarrow>
   P \<turnstile> \<langle>RI (C,e);Cs \<leftarrow> e\<^sub>0, s, b\<rangle> \<rightarrow> \<langle>RI (C,e');Cs \<leftarrow> e\<^sub>0, s', b'\<rangle>"
 
 | RedRInit:
   "\<lbrakk> sh C = Some (sfs, i);
      sh' = sh(C \<mapsto> (sfs,Done));
      C' = last(C#Cs) \<rbrakk> \<Longrightarrow>
   P \<turnstile> \<langle>RI (C, Val v);Cs \<leftarrow> e, (h,l,sh), b\<rangle> \<rightarrow> \<langle>INIT C' (Cs,True) \<leftarrow> e, (h,l,sh'), b\<rangle>"
 
 \<comment> \<open>Exception propagation\<close>
 
 | CastThrow: "P \<turnstile> \<langle>Cast C (throw e), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | BinOpThrow1: "P \<turnstile> \<langle>(throw e) \<guillemotleft>bop\<guillemotright> e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | BinOpThrow2: "P \<turnstile> \<langle>(Val v\<^sub>1) \<guillemotleft>bop\<guillemotright> (throw e), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | LAssThrow: "P \<turnstile> \<langle>V:=(throw e), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | FAccThrow: "P \<turnstile> \<langle>(throw e)\<bullet>F{D}, s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | FAssThrow1: "P \<turnstile> \<langle>(throw e)\<bullet>F{D}:=e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | FAssThrow2: "P \<turnstile> \<langle>Val v\<bullet>F{D}:=(throw e), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | SFAssThrow: "P \<turnstile> \<langle>C\<bullet>\<^sub>sF{D}:=(throw e), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | CallThrowObj: "P \<turnstile> \<langle>(throw e)\<bullet>M(es), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | CallThrowParams: "\<lbrakk> es = map Val vs @ throw e # es' \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>(Val v)\<bullet>M(es), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | SCallThrowParams: "\<lbrakk> es = map Val vs @ throw e # es' \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>C\<bullet>\<^sub>sM(es), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | BlockThrow: "P \<turnstile> \<langle>{V:T; Throw a}, s, b\<rangle> \<rightarrow> \<langle>Throw a, s, b\<rangle>"
 | InitBlockThrow: "P \<turnstile> \<langle>{V:T := Val v; Throw a}, s, b\<rangle> \<rightarrow> \<langle>Throw a, s, b\<rangle>"
 | SeqThrow: "P \<turnstile> \<langle>(throw e);;e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | CondThrow: "P \<turnstile> \<langle>if (throw e) e\<^sub>1 else e\<^sub>2, s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | ThrowThrow: "P \<turnstile> \<langle>throw(throw e), s, b\<rangle> \<rightarrow> \<langle>throw e, s, b\<rangle>"
 | RInitInitThrow: "\<lbrakk> sh C = Some(sfs,i); sh' = sh(C \<mapsto> (sfs,Error)) \<rbrakk> \<Longrightarrow>
   P \<turnstile> \<langle>RI (C,Throw a);D#Cs \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>RI (D,Throw a);Cs \<leftarrow> e,(h,l,sh'),b\<rangle>"
 | RInitThrow: "\<lbrakk> sh C = Some(sfs, i); sh' = sh(C \<mapsto> (sfs,Error)) \<rbrakk> \<Longrightarrow>
   P \<turnstile> \<langle>RI (C,Throw a);Nil \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>Throw a,(h,l,sh'),b\<rangle>"
 (*<*)
 lemmas red_reds_induct = red_reds.induct [split_format (complete)]
   and red_reds_inducts = red_reds.inducts [split_format (complete)]
 
 inductive_cases [elim!]:
  "P \<turnstile> \<langle>V:=e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
  "P \<turnstile> \<langle>e1;;e2,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
 (*>*)
 
 subsection\<open> The reflexive transitive closure \<close>
 
 abbreviation
   Step :: "J_prog \<Rightarrow> expr \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> expr \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool"
           ("_ \<turnstile> ((1\<langle>_,/_,/_\<rangle>) \<rightarrow>*/ (1\<langle>_,/_,/_\<rangle>))" [51,0,0,0,0,0,0] 81)
   where "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle> \<equiv> ((e,s,b), e',s',b') \<in> (red P)\<^sup>*"
 
 abbreviation
   Steps :: "J_prog \<Rightarrow> expr list \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> expr list \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool"
           ("_ \<turnstile> ((1\<langle>_,/_,/_\<rangle>) [\<rightarrow>]*/ (1\<langle>_,/_,/_\<rangle>))" [51,0,0,0,0,0,0] 81)
   where "P \<turnstile> \<langle>es,s,b\<rangle> [\<rightarrow>]* \<langle>es',s',b'\<rangle> \<equiv> ((es,s,b), es',s',b') \<in> (reds P)\<^sup>*"
 
 
 lemmas converse_rtrancl_induct3 =
   converse_rtrancl_induct [of "(ax, ay, az)" "(bx, by, bz)", split_format (complete),
     consumes 1, case_names refl step]
 
 lemma converse_rtrancl_induct_red[consumes 1]:
 assumes "P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow>* \<langle>e',(h',l',sh'),b'\<rangle>"
 and "\<And>e h l sh b. R e h l sh b e h l sh b"
 and "\<And>e\<^sub>0 h\<^sub>0 l\<^sub>0 sh\<^sub>0 b\<^sub>0 e\<^sub>1 h\<^sub>1 l\<^sub>1 sh\<^sub>1 b\<^sub>1 e' h' l' sh' b'.
        \<lbrakk> P \<turnstile> \<langle>e\<^sub>0,(h\<^sub>0,l\<^sub>0,sh\<^sub>0),b\<^sub>0\<rangle> \<rightarrow> \<langle>e\<^sub>1,(h\<^sub>1,l\<^sub>1,sh\<^sub>1),b\<^sub>1\<rangle>; R e\<^sub>1 h\<^sub>1 l\<^sub>1 sh\<^sub>1 b\<^sub>1 e' h' l' sh' b' \<rbrakk>
    \<Longrightarrow> R e\<^sub>0 h\<^sub>0 l\<^sub>0 sh\<^sub>0 b\<^sub>0 e' h' l' sh' b'"
 shows "R e h l sh b e' h' l' sh' b'"
 (*<*)
 proof -
   { fix s s'
     assume reds: "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>"
        and base: "\<And>e s b. R e (hp s) (lcl s) (shp s) b e (hp s) (lcl s) (shp s) b"
        and red\<^sub>1: "\<And>e\<^sub>0 s\<^sub>0 b\<^sub>0 e\<^sub>1 s\<^sub>1 b\<^sub>1 e' s' b'.
            \<lbrakk> P \<turnstile> \<langle>e\<^sub>0,s\<^sub>0,b\<^sub>0\<rangle> \<rightarrow> \<langle>e\<^sub>1,s\<^sub>1,b\<^sub>1\<rangle>; R e\<^sub>1 (hp s\<^sub>1) (lcl s\<^sub>1) (shp s\<^sub>1) b\<^sub>1 e' (hp s') (lcl s') (shp s') b' \<rbrakk>
            \<Longrightarrow> R e\<^sub>0 (hp s\<^sub>0) (lcl s\<^sub>0) (shp s\<^sub>0) b\<^sub>0 e' (hp s') (lcl s') (shp s') b'"
     from reds have "R e (hp s) (lcl s) (shp s) b e' (hp s') (lcl s') (shp s') b'"
     proof (induct rule:converse_rtrancl_induct3)
       case refl show ?case by(rule base)
     next
       case step
       thus ?case by(blast intro:red\<^sub>1)
     qed
     }
   with assms show ?thesis by fastforce
 qed
 (*>*)
 
 
 subsection\<open>Some easy lemmas\<close>
 
 lemma [iff]: "\<not> P \<turnstile> \<langle>[],s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
 (*<*)by(blast elim: reds.cases)(*>*)
 
 lemma [iff]: "\<not> P \<turnstile> \<langle>Val v,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
 (*<*)by(fastforce elim: red.cases)(*>*)
 
 lemma val_no_step: "val_of e = \<lfloor>v\<rfloor> \<Longrightarrow> \<not> P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
 (*<*)by(drule val_of_spec, simp)(*>*)
 
 lemma [iff]: "\<not> P \<turnstile> \<langle>Throw a,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
 (*<*)by(fastforce elim: red.cases)(*>*)
 
 
 lemma map_Vals_no_step [iff]: "\<not> P \<turnstile> \<langle>map Val vs,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
 (*<*)
-apply(induct vs arbitrary: es', simp)
-apply(rule notI)
-apply(erule reds.cases, auto)
-done
+proof(induct vs arbitrary: es')
+  case (Cons a vs)
+  { assume "P \<turnstile> \<langle>map Val (a # vs),s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
+    then have False by(rule reds.cases) (insert Cons, auto)
+  }
+  then show ?case by clarsimp
+qed simp
 (*>*)
 
 lemma vals_no_step: "map_vals_of es = \<lfloor>vs\<rfloor> \<Longrightarrow> \<not> P \<turnstile> \<langle>es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
 (*<*)by(drule map_vals_of_spec, simp)(*>*)
 
 lemma vals_throw_no_step [iff]: "\<not> P \<turnstile> \<langle>map Val vs @ Throw a # es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
 (*<*)
-apply(induct vs arbitrary: es', auto)
-apply(erule reds.cases, auto)
-apply(erule reds.cases, auto)
-done
+proof(induct vs arbitrary: es')
+  case Nil
+  { assume "P \<turnstile> \<langle>Throw a # es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
+    then have False by(rule reds.cases) (insert Cons, auto)
+  }
+  then show ?case by clarsimp
+next
+  case (Cons a' vs')
+  { assume "P \<turnstile> \<langle>map Val (a'#vs') @ Throw a # es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
+    then have False by(rule reds.cases) (insert Cons, auto)
+  }
+  then show ?case by clarsimp
+qed
 (*>*)
 
 lemma lass_val_of_red:
  "\<lbrakk> lass_val_of e = \<lfloor>a\<rfloor>; P \<turnstile> \<langle>e,(h, l, sh),b\<rangle> \<rightarrow> \<langle>e',(h', l', sh'),b'\<rangle> \<rbrakk>
   \<Longrightarrow> e' = unit \<and> h' = h \<and> l' = l(fst a\<mapsto>snd a) \<and> sh' = sh \<and> b = b'"
 (*<*)by(drule lass_val_of_spec, auto)(*>*)
 
 
 lemma final_no_step [iff]: "final e \<Longrightarrow> \<not> P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow> \<langle>e',s',b'\<rangle>"
 (*<*)by(erule finalE, simp+)(*>*)
 
 lemma finals_no_step [iff]: "finals es \<Longrightarrow> \<not> P \<turnstile> \<langle>es,s,b\<rangle> [\<rightarrow>] \<langle>es',s',b'\<rangle>"
 (*<*)by(erule finalsE, simp+)(*>*)
 
 lemma reds_final_same:
 "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle> \<Longrightarrow> final e \<Longrightarrow> e = e' \<and> s = s' \<and> b = b'"
 proof(induct rule:converse_rtrancl_induct3)
   case refl show ?case by simp
 next
   case (step e0 s0 b0 e1 s1 b1) show ?case
   proof(rule finalE[OF step.prems(1)])
     fix v assume "e0 = Val v" then show ?thesis using step by simp
   next
     fix a assume "e0 = Throw a" then show ?thesis using step by simp
   qed
 qed
 
 lemma reds_throw:
 "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle> \<Longrightarrow> (\<And>e\<^sub>t. throw_of e = \<lfloor>e\<^sub>t\<rfloor> \<Longrightarrow> \<exists>e\<^sub>t'. throw_of e' = \<lfloor>e\<^sub>t'\<rfloor>)"
 proof(induct rule:converse_rtrancl_induct3)
   case refl then show ?case by simp
 next
   case (step e0 s0 b0 e1 s1 b1)
   then show ?case by(auto elim: red.cases)
 qed
 
 lemma red_hext_incr: "P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',(h',l',sh'),b'\<rangle>  \<Longrightarrow> h \<unlhd> h'"
   and reds_hext_incr: "P \<turnstile> \<langle>es,(h,l,sh),b\<rangle> [\<rightarrow>] \<langle>es',(h',l',sh'),b'\<rangle>  \<Longrightarrow> h \<unlhd> h'"
 (*<*)
 proof(induct rule:red_reds_inducts)
   case RedNew thus ?case
     by(fastforce dest:new_Addr_SomeD simp:hext_def split:if_splits)
 next
   case RedFAss thus ?case by(simp add:hext_def split:if_splits)
 qed simp_all
 (*>*)
 
 
 lemma red_lcl_incr: "P \<turnstile> \<langle>e,(h\<^sub>0,l\<^sub>0,sh\<^sub>0),b\<rangle> \<rightarrow> \<langle>e',(h\<^sub>1,l\<^sub>1,sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1"
 and reds_lcl_incr: "P \<turnstile> \<langle>es,(h\<^sub>0,l\<^sub>0,sh\<^sub>0),b\<rangle> [\<rightarrow>] \<langle>es',(h\<^sub>1,l\<^sub>1,sh\<^sub>1),b'\<rangle> \<Longrightarrow> dom l\<^sub>0 \<subseteq> dom l\<^sub>1"
 (*<*)by(induct rule: red_reds_inducts)(auto simp del:fun_upd_apply)(*>*)
 
 lemma red_lcl_add: "P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',(h',l',sh'),b'\<rangle> \<Longrightarrow> (\<And>l\<^sub>0. P \<turnstile> \<langle>e,(h,l\<^sub>0++l,sh),b\<rangle> \<rightarrow> \<langle>e',(h',l\<^sub>0++l',sh'),b'\<rangle>)"
 and reds_lcl_add: "P \<turnstile> \<langle>es,(h,l,sh),b\<rangle> [\<rightarrow>] \<langle>es',(h',l',sh'),b'\<rangle> \<Longrightarrow> (\<And>l\<^sub>0. P \<turnstile> \<langle>es,(h,l\<^sub>0++l,sh),b\<rangle> [\<rightarrow>] \<langle>es',(h',l\<^sub>0++l',sh'),b'\<rangle>)"
 (*<*)
 proof (induct rule:red_reds_inducts)
   case RedCast thus ?case by(fastforce intro:red_reds.intros)
 next
   case RedCastFail thus ?case by(force intro:red_reds.intros)
 next
   case RedFAcc thus ?case by(fastforce intro:red_reds.intros)
 next
   case RedCall thus ?case by(fastforce intro:red_reds.intros)
 next
   case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T l\<^sub>0)
   have IH: "\<And>l\<^sub>0. P \<turnstile> \<langle>e,(h, l\<^sub>0 ++ l(V \<mapsto> v), sh),b\<rangle> \<rightarrow> \<langle>e',(h', l\<^sub>0 ++ l', sh'),b'\<rangle>"
     and l'V: "l' V = Some v'" by fact+
   from IH have IH': "P \<turnstile> \<langle>e,(h, (l\<^sub>0 ++ l)(V \<mapsto> v), sh),b\<rangle> \<rightarrow> \<langle>e',(h', l\<^sub>0 ++ l', sh'),b'\<rangle>"
     by simp
   have "(l\<^sub>0 ++ l')(V := (l\<^sub>0 ++ l) V) = l\<^sub>0 ++ l'(V := l V)"
     by(rule ext)(simp add:map_add_def)
   with red_reds.InitBlockRed[OF IH'] l'V show ?case by(simp del:fun_upd_apply)
 next
   case (BlockRedNone e h l V sh b e' h' l' sh' b' T l\<^sub>0)
   have IH: "\<And>l\<^sub>0. P \<turnstile> \<langle>e,(h, l\<^sub>0 ++ l(V := None), sh),b\<rangle> \<rightarrow> \<langle>e',(h', l\<^sub>0 ++ l', sh'),b'\<rangle>"
     and l'V: "l' V = None" and unass: "\<not> assigned V e" by fact+
   have "l\<^sub>0(V := None) ++ l(V := None) = (l\<^sub>0 ++ l)(V := None)"
     by(simp add:fun_eq_iff map_add_def)
   hence IH': "P \<turnstile> \<langle>e,(h, (l\<^sub>0++l)(V := None), sh),b\<rangle> \<rightarrow> \<langle>e',(h', l\<^sub>0(V := None) ++ l', sh'),b'\<rangle>"
     using IH[of "l\<^sub>0(V := None)"] by simp
   have "(l\<^sub>0(V := None) ++ l')(V := (l\<^sub>0 ++ l) V) = l\<^sub>0 ++ l'(V := l V)"
     by(simp add:fun_eq_iff map_add_def)
   with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
     by(simp add: map_add_def)
 next
   case (BlockRedSome e h l V sh b e' h' l' sh' b' v T l\<^sub>0)
   have IH: "\<And>l\<^sub>0. P \<turnstile> \<langle>e,(h, l\<^sub>0 ++ l(V := None), sh),b\<rangle> \<rightarrow> \<langle>e',(h', l\<^sub>0 ++ l', sh'),b'\<rangle>"
     and l'V: "l' V = Some v" and unass: "\<not> assigned V e" by fact+
   have "l\<^sub>0(V := None) ++ l(V := None) = (l\<^sub>0 ++ l)(V := None)"
     by(simp add:fun_eq_iff map_add_def)
   hence IH': "P \<turnstile> \<langle>e,(h, (l\<^sub>0++l)(V := None), sh),b\<rangle> \<rightarrow> \<langle>e',(h', l\<^sub>0(V := None) ++ l', sh'),b'\<rangle>"
     using IH[of "l\<^sub>0(V := None)"] by simp
   have "(l\<^sub>0(V := None) ++ l')(V := (l\<^sub>0 ++ l) V) = l\<^sub>0 ++ l'(V := l V)"
     by(simp add:fun_eq_iff map_add_def)
   with red_reds.BlockRedSome[OF IH' _ unass] l'V show ?case
     by(simp add:map_add_def)
 next
   case RedTryCatch thus ?case by(fastforce intro:red_reds.intros)
 next
   case RedTryFail thus ?case by(force intro!:red_reds.intros)
 qed (simp_all add:red_reds.intros)
 (*>*)
 
 
 lemma Red_lcl_add:
 assumes "P \<turnstile> \<langle>e,(h,l,sh), b\<rangle> \<rightarrow>* \<langle>e',(h',l',sh'), b'\<rangle>" shows "P \<turnstile> \<langle>e,(h,l\<^sub>0++l,sh),b\<rangle> \<rightarrow>* \<langle>e',(h',l\<^sub>0++l',sh'),b'\<rangle>"
 (*<*)
 using assms
 proof(induct rule:converse_rtrancl_induct_red)
   case 1 thus ?case by simp
 next
   case 2 thus ?case
     by (blast dest: red_lcl_add intro: converse_rtrancl_into_rtrancl)
 qed
 (*>*)
 
 lemma assumes wf: "wwf_J_prog P"
 shows red_proc_pres: "P \<turnstile> \<langle>e,(h,l,sh),b\<rangle> \<rightarrow> \<langle>e',(h',l',sh'),b'\<rangle>
   \<Longrightarrow> not_init C e \<Longrightarrow> sh C = \<lfloor>(sfs, Processing)\<rfloor> \<Longrightarrow> not_init C e' \<and> (\<exists>sfs'. sh' C = \<lfloor>(sfs', Processing)\<rfloor>)"
   and reds_proc_pres: "P \<turnstile> \<langle>es,(h,l,sh),b\<rangle> [\<rightarrow>] \<langle>es',(h',l',sh'),b'\<rangle>
   \<Longrightarrow> not_inits C es \<Longrightarrow> sh C = \<lfloor>(sfs, Processing)\<rfloor> \<Longrightarrow> not_inits C es' \<and> (\<exists>sfs'. sh' C = \<lfloor>(sfs', Processing)\<rfloor>)"
 (*<*)
 proof(induct rule:red_reds_inducts)
   case RedCall then show ?case
   using sees_wwf_nsub_RI[OF wf RedCall.hyps(2)] sub_RI_blocks_body nsub_RI_not_init by auto
 next
   case RedSCall then show ?case
   using sees_wwf_nsub_RI[OF wf RedSCall.hyps(1)] sub_RI_blocks_body nsub_RI_not_init by auto
 next
   case (RedInitDone sh C sfs C' Cs e h l b)
   then show ?case by(cases Cs, auto)
 next
   case (RedInitProcessing sh C sfs C' Cs e h l b)
   then show ?case by(cases Cs, auto)
 next
   case (RedRInit sh C sfs i sh' C' Cs v e h l b)
   then show ?case by(cases Cs, auto)
 next
   case (CallThrowParams es vs e es' v M h l sh b)
   then show ?case by(auto dest: not_inits_def')
 next
   case (SCallThrowParams es vs e es' C M h l sh b)
   then show ?case by(auto dest: not_inits_def')
 qed(auto)
 
 end
diff --git a/thys/JinjaDCI/J/WWellForm.thy b/thys/JinjaDCI/J/WWellForm.thy
--- a/thys/JinjaDCI/J/WWellForm.thy
+++ b/thys/JinjaDCI/J/WWellForm.thy
@@ -1,42 +1,40 @@
 (*  Title:      JinjaDCI/J/WWellForm.thy
 
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/WWellForm.thy by Tobias Nipkow
 *)
 
 section \<open> Weak well-formedness of Jinja programs \<close>
 
 theory WWellForm imports "../Common/WellForm" Expr begin
 
 definition wwf_J_mdecl :: "J_prog \<Rightarrow> cname \<Rightarrow> J_mb mdecl \<Rightarrow> bool"
 where
   "wwf_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> fv body \<subseteq> {this} \<union> set pns
  | Static \<Rightarrow> fv body \<subseteq> set pns)"
 
 lemma wwf_J_mdecl_NonStatic[simp]:
   "wwf_J_mdecl P C (M,NonStatic,Ts,T,pns,body) =
   (length Ts = length pns \<and> distinct pns \<and> \<not>sub_RI body \<and> this \<notin> set pns \<and> fv body \<subseteq> {this} \<union> set pns)"
 (*<*)by(simp add:wwf_J_mdecl_def)(*>*)
 
 lemma wwf_J_mdecl_Static[simp]:
   "wwf_J_mdecl P C (M,Static,Ts,T,pns,body) =
   (length Ts = length pns \<and> distinct pns \<and> \<not>sub_RI body \<and> fv body \<subseteq> set pns)"
 (*<*)by(simp add:wwf_J_mdecl_def)(*>*)
 
 abbreviation
   wwf_J_prog :: "J_prog \<Rightarrow> bool" where
   "wwf_J_prog \<equiv> wf_prog wwf_J_mdecl"
 
 
 lemma sees_wwf_nsub_RI:
  "\<lbrakk> wwf_J_prog P; P \<turnstile> C sees M,b : Ts\<rightarrow>T = (pns, body) in D \<rbrakk> \<Longrightarrow> \<not>sub_RI body"
-apply(drule sees_wf_mdecl, simp)
-apply(unfold wwf_J_mdecl_def wf_mdecl_def, simp)
-done
+(*<*)by(auto dest!: sees_wf_mdecl simp: wwf_J_mdecl_def wf_mdecl_def)(*>*)
 
 end
diff --git a/thys/JinjaDCI/J/WellType.thy b/thys/JinjaDCI/J/WellType.thy
--- a/thys/JinjaDCI/J/WellType.thy
+++ b/thys/JinjaDCI/J/WellType.thy
@@ -1,255 +1,219 @@
 (*  Title:      JinjaDCI/J/WellType.thy
 
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/WellType.thy by Tobias Nipkow
 *)
 
 section \<open> Well-typedness of Jinja expressions \<close>
 
 theory WellType
 imports "../Common/Objects" Expr
 begin
 
 type_synonym
   env  = "vname \<rightharpoonup> ty"
 
 inductive
   WT :: "[J_prog,env, expr     , ty     ] \<Rightarrow> bool"
          ("_,_ \<turnstile> _ :: _"   [51,51,51]50)
   and WTs :: "[J_prog,env, expr list, ty list] \<Rightarrow> bool"
          ("_,_ \<turnstile> _ [::] _" [51,51,51]50)
   for P :: J_prog
 where
   
   WTNew:
   "is_class P C  \<Longrightarrow>
   P,E \<turnstile> new C :: Class C"
 
 | WTCast:
   "\<lbrakk> P,E \<turnstile> e :: Class D;  is_class P C;  P \<turnstile> C \<preceq>\<^sup>* D \<or> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> Cast C e :: Class C"
 
 | WTVal:
   "typeof v = Some T \<Longrightarrow>
   P,E \<turnstile> Val v :: T"
 
 | WTVar:
   "E V = Some T \<Longrightarrow>
   P,E \<turnstile> Var V :: T"
 
 | WTBinOpEq:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: T\<^sub>1;  P,E \<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 \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<^sub>1 \<guillemotleft>Eq\<guillemotright> e\<^sub>2 :: Boolean"
 
 | WTBinOpAdd:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: Integer;  P,E \<turnstile> e\<^sub>2 :: Integer \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<^sub>1 \<guillemotleft>Add\<guillemotright> e\<^sub>2 :: Integer"
 
 | WTLAss:
   "\<lbrakk> E V = Some T;  P,E \<turnstile> e :: T';  P \<turnstile> T' \<le> T; V \<noteq> this \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> V:=e :: Void"
 
 | WTFAcc:
   "\<lbrakk> P,E \<turnstile> e :: Class C;  P \<turnstile> C sees F,NonStatic:T in D \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<bullet>F{D} :: T"
 
 | WTSFAcc:
   "\<lbrakk> P \<turnstile> C sees F,Static:T in D \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> C\<bullet>\<^sub>sF{D} :: T"
 
 | WTFAss:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: Class C;  P \<turnstile> C sees F,NonStatic:T in D;  P,E \<turnstile> e\<^sub>2 :: T';  P \<turnstile> T' \<le> T \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<^sub>1\<bullet>F{D}:=e\<^sub>2 :: Void"
 
 | WTSFAss:
   "\<lbrakk>  P \<turnstile> C sees F,Static:T in D;  P,E \<turnstile> e\<^sub>2 :: T';  P \<turnstile> T' \<le> T \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> C\<bullet>\<^sub>sF{D}:=e\<^sub>2 :: Void"
 
 | WTCall:
   "\<lbrakk> P,E \<turnstile> e :: Class C;  P \<turnstile> C sees M,NonStatic:Ts \<rightarrow> T = (pns,body) in D;
      P,E \<turnstile> es [::] Ts';  P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> e\<bullet>M(es) :: T"
 
 | WTSCall:
   "\<lbrakk> P \<turnstile> C sees M,Static:Ts \<rightarrow> T = (pns,body) in D;
      P,E \<turnstile> es [::] Ts';  P \<turnstile> Ts' [\<le>] Ts; M \<noteq> clinit \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> C\<bullet>\<^sub>sM(es) :: T"
 
 | WTBlock:
   "\<lbrakk> is_type P T;  P,E(V \<mapsto> T) \<turnstile> e :: T' \<rbrakk>
   \<Longrightarrow>  P,E \<turnstile> {V:T; e} :: T'"
 
 | WTSeq:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1::T\<^sub>1;  P,E \<turnstile> e\<^sub>2::T\<^sub>2 \<rbrakk>
   \<Longrightarrow>  P,E \<turnstile> e\<^sub>1;;e\<^sub>2 :: T\<^sub>2"
 
 | WTCond:
   "\<lbrakk> P,E \<turnstile> e :: Boolean;  P,E \<turnstile> e\<^sub>1::T\<^sub>1;  P,E \<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 \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :: T"
 
 | WTWhile:
   "\<lbrakk> P,E \<turnstile> e :: Boolean;  P,E \<turnstile> c::T \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> while (e) c :: Void"
 
 | WTThrow:
   "P,E \<turnstile> e :: Class C  \<Longrightarrow> 
   P,E \<turnstile> throw e :: Void"
 
 | WTTry:
   "\<lbrakk> P,E \<turnstile> e\<^sub>1 :: T;  P,E(V \<mapsto> Class C) \<turnstile> e\<^sub>2 :: T; is_class P C \<rbrakk>
   \<Longrightarrow> P,E \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 :: T"
 
 \<comment> \<open>well-typed expression lists\<close>
 
 | WTNil:
   "P,E \<turnstile> [] [::] []"
 
 | WTCons:
   "\<lbrakk> P,E \<turnstile> e :: T; P,E \<turnstile> es [::] Ts \<rbrakk>
   \<Longrightarrow>  P,E \<turnstile> e#es [::] T#Ts"
 
 (*<*)
 declare WT_WTs.intros[intro!] (* WTNil[iff] *)
 
 lemmas WT_WTs_induct = WT_WTs.induct [split_format (complete)]
   and WT_WTs_inducts = WT_WTs.inducts [split_format (complete)]
 (*>*)
 
 lemma init_nwt [simp]:"\<not>P,E \<turnstile> INIT C (Cs,b) \<leftarrow> e :: T"
  by(auto elim:WT.cases)
 lemma ri_nwt [simp]:"\<not>P,E \<turnstile> RI(C,e);Cs \<leftarrow> e' :: T"
  by(auto elim:WT.cases)
 
 lemma [iff]: "(P,E \<turnstile> [] [::] Ts) = (Ts = [])"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTs.cases)
-done
-(*>*)
+(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)
 
 lemma [iff]: "(P,E \<turnstile> e#es [::] T#Ts) = (P,E \<turnstile> e :: T \<and> P,E \<turnstile> es [::] Ts)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTs.cases)
-done
-(*>*)
+(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)
 
 lemma [iff]: "(P,E \<turnstile> (e#es) [::] Ts) =
   (\<exists>U Us. Ts = U#Us \<and> P,E \<turnstile> e :: U \<and> P,E \<turnstile> es [::] Us)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTs.cases)
-done
-(*>*)
+(*<*)by (rule iffI) (auto elim: WTs.cases)(*>*)
 
 lemma [iff]: "\<And>Ts. (P,E \<turnstile> es\<^sub>1 @ es\<^sub>2 [::] Ts) =
   (\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E \<turnstile> es\<^sub>1 [::] Ts\<^sub>1 \<and> P,E \<turnstile> es\<^sub>2[::]Ts\<^sub>2)"
 (*<*)
-apply(induct es\<^sub>1 type:list)
- apply simp
-apply clarsimp
-apply(erule thin_rl)
-apply (rule iffI)
- apply clarsimp
- apply(rule exI)+
- apply(rule conjI)
-  prefer 2 apply blast
- apply simp
-apply fastforce
-done
+proof(induct es\<^sub>1 type:list)
+  case (Cons a list)
+  let ?lhs = "(\<exists>U Us. Ts = U # Us \<and> P,E \<turnstile> a :: U \<and>
+        (\<exists>Ts\<^sub>1 Ts\<^sub>2. Us = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E \<turnstile> list [::] Ts\<^sub>1 \<and> P,E \<turnstile> es\<^sub>2 [::] Ts\<^sub>2))"
+  let ?rhs = "(\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and>
+        (\<exists>U Us. Ts\<^sub>1 = U # Us \<and> P,E \<turnstile> a :: U \<and> P,E \<turnstile> list [::] Us) \<and> P,E \<turnstile> es\<^sub>2 [::] Ts\<^sub>2)"
+  { assume ?lhs
+    then have ?rhs by (auto intro: Cons_eq_appendI)
+  }
+  moreover {
+    assume ?rhs
+    then have ?lhs by fastforce
+  }
+  ultimately have "?lhs = ?rhs" by(rule iffI)
+  then show ?case by (clarsimp simp: Cons)
+qed simp
 (*>*)
 
 lemma [iff]: "P,E \<turnstile> Val v :: T = (typeof v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 lemma [iff]: "P,E \<turnstile> Var V :: T = (E V = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 lemma [iff]: "P,E \<turnstile> e\<^sub>1;;e\<^sub>2 :: T\<^sub>2 = (\<exists>T\<^sub>1. P,E \<turnstile> e\<^sub>1::T\<^sub>1 \<and> P,E \<turnstile> e\<^sub>2::T\<^sub>2)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 lemma [iff]: "(P,E \<turnstile> {V:T; e} :: T') = (is_type P T \<and> P,E(V\<mapsto>T) \<turnstile> e :: T')"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WT.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WT.cases)(*>*)
 
 (*<*)
 inductive_cases WT_elim_cases[elim!]:
   "P,E \<turnstile> V :=e :: T"
   "P,E \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 :: T"
   "P,E \<turnstile> while (e) c :: T"
   "P,E \<turnstile> throw e :: T"
   "P,E \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 :: T"
   "P,E \<turnstile> Cast D e :: T"
   "P,E \<turnstile> a\<bullet>F{D} :: T"
   "P,E \<turnstile> C\<bullet>\<^sub>sF{D} :: T"
   "P,E \<turnstile> a\<bullet>F{D} := v :: T"
   "P,E \<turnstile> C\<bullet>\<^sub>sF{D} := v :: T"
   "P,E \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 :: T"
   "P,E \<turnstile> new C :: T"
   "P,E \<turnstile> e\<bullet>M(ps) :: T"
   "P,E \<turnstile> C\<bullet>\<^sub>sM(ps) :: T"
 (*>*)
 
 
 lemma wt_env_mono:
   "P,E \<turnstile> e :: T \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E' \<turnstile> e :: T)" and 
   "P,E \<turnstile> es [::] Ts \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E' \<turnstile> es [::] Ts)"
 (*<*)
-apply(induct rule: WT_WTs_inducts)
-apply(simp add: WTNew)
-apply(fastforce simp: WTCast)
-apply(fastforce simp: WTVal)
-apply(simp add: WTVar map_le_def dom_def)
-apply(fastforce simp: WTBinOpEq)
-apply(fastforce simp: WTBinOpAdd)
-apply(force simp:map_le_def)
-apply(fastforce simp: WTFAcc)
-apply(fastforce)
-apply(fastforce simp: WTFAss del:WT_WTs.intros WT_elim_cases)
-apply(fastforce)
-apply(fastforce simp: WTCall)
-apply(fastforce)
-apply(fastforce simp: map_le_def WTBlock)
-apply(fastforce simp: WTSeq)
-apply(fastforce simp: WTCond)
-apply(fastforce simp: WTWhile)
-apply(fastforce simp: WTThrow)
-apply(fastforce simp: WTTry map_le_def dom_def)
-apply(simp add: WTNil)
-apply(simp add: WTCons)
-done
+proof(induct rule: WT_WTs_inducts)
+  case WTVar then show ?case by(simp add: map_le_def dom_def)
+next
+  case WTLAss then show ?case by(force simp:map_le_def)
+qed fastforce+
 (*>*)
 
 
 lemma WT_fv: "P,E \<turnstile> e :: T \<Longrightarrow> fv e \<subseteq> dom E"
 and "P,E \<turnstile> es [::] Ts \<Longrightarrow> fvs es \<subseteq> dom E"
 (*<*)
-apply(induct rule:WT_WTs.inducts)
-apply(simp_all del: fun_upd_apply)
-apply fast+
-done
+proof(induct rule:WT_WTs.inducts)
+  case WTVar then show ?case by fastforce
+next
+  case WTLAss then show ?case by fastforce
+next
+  case WTBlock then show ?case by fastforce
+next
+  case WTTry then show ?case by fastforce
+qed simp_all
+(*>*)
 
 lemma WT_nsub_RI: "P,E \<turnstile> e :: T \<Longrightarrow> \<not>sub_RI e"
  and WTs_nsub_RIs: "P,E \<turnstile> es [::] Ts \<Longrightarrow> \<not>sub_RIs es"
-proof(induct rule: WT_WTs.inducts) qed(simp_all)
+(*<*)proof(induct rule: WT_WTs.inducts) qed(simp_all)
 
 end
 (*>*)
diff --git a/thys/JinjaDCI/J/WellTypeRT.thy b/thys/JinjaDCI/J/WellTypeRT.thy
--- a/thys/JinjaDCI/J/WellTypeRT.thy
+++ b/thys/JinjaDCI/J/WellTypeRT.thy
@@ -1,353 +1,293 @@
 (*  Title:      JinjaDCI/J/WellTypeRT.thy
 
     Author:     Tobias Nipkow, Susannah Mansky
     Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC
 
     Based on the Jinja theory J/WellTypeRT.thy by Tobias Nipkow
 *)
 
 section \<open> Runtime Well-typedness \<close>
 
 theory WellTypeRT
 imports WellType
 begin
 
 inductive
   WTrt :: "J_prog \<Rightarrow> heap \<Rightarrow> sheap \<Rightarrow> env \<Rightarrow> expr \<Rightarrow> ty \<Rightarrow> bool"
   and WTrts :: "J_prog \<Rightarrow> heap \<Rightarrow> sheap \<Rightarrow> env \<Rightarrow> expr list \<Rightarrow> 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"
 
 | WTrtNew:
   "is_class P C  \<Longrightarrow>
   P,E,h,sh \<turnstile> new C : Class C"
 
 | WTrtCast:
   "\<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"
 
 | WTrtVal:
   "typeof\<^bsub>h\<^esub> v = Some T \<Longrightarrow>
   P,E,h,sh \<turnstile> Val v : T"
 
 | WTrtVar:
   "E V = Some T  \<Longrightarrow>
   P,E,h,sh \<turnstile> Var V : T"
 
 | WTrtBinOpEq:
   "\<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"
 
 | WTrtBinOpAdd:
   "\<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"
 
 | WTrtLAss:
   "\<lbrakk> E V = Some T;  P,E,h,sh \<turnstile> e : T';  P \<turnstile> T' \<le> T \<rbrakk>
    \<Longrightarrow> P,E,h,sh \<turnstile> V:=e : Void"
 
 | WTrtFAcc:
   "\<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"
 
 | WTrtFAccNT:
   "P,E,h,sh \<turnstile> e : NT \<Longrightarrow>
   P,E,h,sh \<turnstile> e\<bullet>F{D} : T"
 
 | WTrtSFAcc:
   "\<lbrakk> P \<turnstile> C has F,Static:T in D \<rbrakk> \<Longrightarrow>
   P,E,h,sh \<turnstile> C\<bullet>\<^sub>sF{D} : T"
 
 | WTrtFAss:
   "\<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"
 
 | WTrtFAssNT:
   "\<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"
 
 | WTrtSFAss:
   "\<lbrakk> P,E,h,sh \<turnstile> e\<^sub>2 : T\<^sub>2; P \<turnstile> C has F,Static:T in D; P \<turnstile> T\<^sub>2 \<le> T \<rbrakk>
   \<Longrightarrow> P,E,h,sh \<turnstile> C\<bullet>\<^sub>sF{D}:=e\<^sub>2 : Void"
 
 | WTrtCall:
   "\<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"
 
 | WTrtCallNT:
   "\<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"
 
 | WTrtSCall:
   "\<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"
 
 | WTrtBlock:
   "P,E(V\<mapsto>T),h,sh \<turnstile> e : T'  \<Longrightarrow>
   P,E,h,sh \<turnstile> {V:T; e} : T'"
 
 | WTrtSeq:
   "\<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"
 
 | WTrtCond:
   "\<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"
 
 | WTrtWhile:
   "\<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"
 
 | WTrtThrow:
   "\<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"
 
 | WTrtTry:
   "\<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"
 
 | WTrtInit:
   "\<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"
 
 | WTrtRI:
   "\<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'"
 
 \<comment> \<open>well-typed expression lists\<close>
 
 | WTrtNil:
   "P,E,h,sh \<turnstile> [] [:] []"
 
 | WTrtCons:
   "\<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"
 
 (*<*)
 declare WTrt_WTrts.intros[intro!] WTrtNil[iff]
 declare
   WTrtFAcc[rule del] WTrtFAccNT[rule del] WTrtSFAcc[rule del]
   WTrtFAss[rule del] WTrtFAssNT[rule del] WTrtSFAss[rule del]
   WTrtCall[rule del] WTrtCallNT[rule del] WTrtSCall[rule del]
 
 lemmas WTrt_induct = WTrt_WTrts.induct [split_format (complete)]
   and WTrt_inducts = WTrt_WTrts.inducts [split_format (complete)]
 (*>*)
 
 
 subsection\<open>Easy consequences\<close>
 
 lemma [iff]: "(P,E,h,sh \<turnstile> [] [:] Ts) = (Ts = [])"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrts.cases)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)
 
 lemma [iff]: "(P,E,h,sh \<turnstile> e#es [:] T#Ts) = (P,E,h,sh \<turnstile> e : T \<and> P,E,h,sh \<turnstile> es [:] Ts)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrts.cases)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)
 
 lemma [iff]: "(P,E,h,sh \<turnstile> (e#es) [:] Ts) =
   (\<exists>U Us. Ts = U#Us \<and> P,E,h,sh \<turnstile> e : U \<and> P,E,h,sh \<turnstile> es [:] Us)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrts.cases)
-done
-(*>*)
+(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)
 
 lemma [simp]: "\<forall>Ts. (P,E,h,sh \<turnstile> es\<^sub>1 @ es\<^sub>2 [:] Ts) =
   (\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E,h,sh \<turnstile> es\<^sub>1 [:] Ts\<^sub>1 & P,E,h,sh \<turnstile> es\<^sub>2[:]Ts\<^sub>2)"
 (*<*)
-apply(induct_tac es\<^sub>1)
- apply simp
-apply clarsimp
-apply(erule thin_rl)
-apply (rule iffI)
- apply clarsimp
- apply(rule exI)+
- apply(rule conjI)
-  prefer 2 apply blast
- apply simp
-apply fastforce
-done
+proof(induct es\<^sub>1)
+  case (Cons a list)
+  let ?lhs = "\<lambda>Ts. (\<exists>U Us. Ts = U # Us \<and> P,E,h,sh \<turnstile> a : U \<and>
+        (\<exists>Ts\<^sub>1 Ts\<^sub>2. Us = Ts\<^sub>1 @ Ts\<^sub>2 \<and> P,E,h,sh \<turnstile> list [:] Ts\<^sub>1 \<and> P,E,h,sh \<turnstile> es\<^sub>2 [:] Ts\<^sub>2))"
+  let ?rhs = "\<lambda>Ts. (\<exists>Ts\<^sub>1 Ts\<^sub>2. Ts = Ts\<^sub>1 @ Ts\<^sub>2 \<and>
+        (\<exists>U Us. Ts\<^sub>1 = U # Us \<and> P,E,h,sh \<turnstile> a : U \<and> P,E,h,sh \<turnstile> list [:] Us) \<and> P,E,h,sh \<turnstile> es\<^sub>2 [:] Ts\<^sub>2)"
+  { fix Ts assume "?lhs Ts"
+    then have "?rhs Ts" by (auto intro: Cons_eq_appendI)
+  }
+  moreover {
+    fix Ts assume "?rhs Ts"
+    then have "?lhs Ts" by fastforce
+  }
+  ultimately have "\<And>Ts. ?lhs Ts = ?rhs Ts" by(rule iffI)
+  then show ?case by (clarsimp simp: Cons)
+qed simp
 (*>*)
 
 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)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
 
 lemma [iff]: "P,E,h,sh \<turnstile> Var v : T = (E v = Some T)"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
 
 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)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
 
 lemma [iff]: "P,E,h,sh \<turnstile> {V:T; e} : T'  =  (P,E(V\<mapsto>T),h,sh \<turnstile> e : T')"
-(*<*)
-apply(rule iffI)
-apply (auto elim: WTrt.cases)
-done
-(*>*)
+(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)
+
 (*<*)
 inductive_cases WTrt_elim_cases[elim!]:
   "P,E,h,sh \<turnstile> v :=e : T"
   "P,E,h,sh \<turnstile> if (e) e\<^sub>1 else e\<^sub>2 : T"
   "P,E,h,sh \<turnstile> while(e) c : T"
   "P,E,h,sh \<turnstile> throw e : T"
   "P,E,h,sh \<turnstile> try e\<^sub>1 catch(C V) e\<^sub>2 : T"
   "P,E,h,sh \<turnstile> Cast D e : T"
   "P,E,h,sh \<turnstile> e\<bullet>F{D} : T"
   "P,E,h,sh \<turnstile> C\<bullet>\<^sub>sF{D} : T"
   "P,E,h,sh \<turnstile> e\<bullet>F{D} := v : T"
   "P,E,h,sh \<turnstile> C\<bullet>\<^sub>sF{D} := v : T"
   "P,E,h,sh \<turnstile> e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2 : T"
   "P,E,h,sh \<turnstile> new C : T"
   "P,E,h,sh \<turnstile> e\<bullet>M{D}(es) : T"
   "P,E,h,sh \<turnstile> C\<bullet>\<^sub>sM{D}(es) : T"
   "P,E,h,sh \<turnstile> INIT C (Cs,b) \<leftarrow> e : T"
   "P,E,h,sh \<turnstile> RI(C,e);Cs \<leftarrow> e' : T"
 (*>*)
 
 subsection\<open>Some interesting lemmas\<close>
 
 lemma WTrts_Val[simp]:
  "\<And>Ts. (P,E,h,sh \<turnstile> map Val vs [:] Ts) = (map (typeof\<^bsub>h\<^esub>) vs = map Some Ts)"
 (*<*)
-apply(induct vs)
- apply simp
-apply(case_tac Ts)
- apply simp
-apply simp
-done
+proof(induct vs)
+  case (Cons a vs)
+  then show ?case by(case_tac Ts; simp)
+qed simp
 (*>*)
 
 
 lemma WTrts_same_length: "\<And>Ts. P,E,h,sh \<turnstile> es [:] Ts \<Longrightarrow> length es = length Ts"
 (*<*)by(induct es type:list)auto(*>*)
 
 
 lemma WTrt_env_mono:
   "P,E,h,sh \<turnstile> e : T \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E',h,sh \<turnstile> e : T)" and
   "P,E,h,sh \<turnstile> es [:] Ts \<Longrightarrow> (\<And>E'. E \<subseteq>\<^sub>m E' \<Longrightarrow> P,E',h,sh \<turnstile> es [:] Ts)"
 (*<*)
 proof(induct rule: WTrt_inducts)
-  case (WTrtVar E V T)
-  then show ?case by(simp add: WTrtVar map_le_def dom_def)
+  case WTrtVar then show ?case by(simp add: map_le_def dom_def)
 next
-  case (WTrtLAss E V T e T')
-  then show ?case by(force simp: map_le_def)
+  case WTrtLAss then show ?case by(force simp:map_le_def)
 qed(fastforce intro: WTrt_WTrts.intros)+
 (*>*)
 
 
 lemma WTrt_hext_mono: "P,E,h,sh \<turnstile> e : T \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,E,h',sh \<turnstile> e : T"
 and WTrts_hext_mono: "P,E,h,sh \<turnstile> es [:] Ts \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> P,E,h',sh \<turnstile> es [:] Ts"
 (*<*)
-apply(induct rule: WTrt_inducts)
-apply(simp add: WTrtNew)
-apply(fastforce simp: WTrtCast)
-apply(fastforce simp: WTrtVal dest:hext_typeof_mono)
-apply(simp add: WTrtVar)
-apply(fastforce simp add: WTrtBinOpEq)
-apply(fastforce simp add: WTrtBinOpAdd)
-apply(fastforce simp add: WTrtLAss)
-apply(fast intro: WTrtFAcc)
-apply(simp add: WTrtFAccNT)
-apply(fast intro: WTrtSFAcc)
-apply(fastforce simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
-apply(fastforce simp: WTrtFAssNT)
-apply(fastforce simp: WTrtSFAss del:WTrt_WTrts.intros WTrt_elim_cases)
-apply(fastforce simp: WTrtCall)
-apply(fastforce simp: WTrtCallNT)
-using WTrtSCall apply blast
-apply(fastforce)
-apply(fastforce simp add: WTrtSeq)
-apply(fastforce simp add: WTrtCond)
-apply(fastforce simp add: WTrtWhile)
-apply(fastforce simp add: WTrtThrow)
-apply(fastforce simp: WTrtTry)
-apply(simp add: WTrtInit)
-apply(simp add: WTrtRI)
-apply(simp add: WTrtNil)
-apply(simp add: WTrtCons)
-done
+proof(induct rule: WTrt_inducts)
+  case WTrtVal then show ?case by(simp add: hext_typeof_mono)
+qed(fastforce intro: WTrt_WTrts.intros)+
 (*>*)
 
 lemma WTrt_shext_mono: "P,E,h,sh \<turnstile> e : T \<Longrightarrow> sh \<unlhd>\<^sub>s sh' \<Longrightarrow> \<not>sub_RI e \<Longrightarrow> P,E,h,sh' \<turnstile> e : T"
 and WTrts_shext_mono: "P,E,h,sh \<turnstile> es [:] Ts \<Longrightarrow> sh \<unlhd>\<^sub>s sh' \<Longrightarrow> \<not>sub_RIs es \<Longrightarrow> P,E,h,sh' \<turnstile> es [:] Ts"
 (*<*)
 by(induct rule: WTrt_inducts)
   (auto simp add: WTrt_WTrts.intros)
 (*>*)
 
 lemma WTrt_hext_shext_mono: "P,E,h,sh \<turnstile> e : T
    \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> sh \<unlhd>\<^sub>s sh' \<Longrightarrow> \<not>sub_RI e \<Longrightarrow> P,E,h',sh' \<turnstile> e : T"
  by(auto intro: WTrt_hext_mono WTrt_shext_mono)
 
 lemma WTrts_hext_shext_mono: "P,E,h,sh \<turnstile> es [:] Ts
    \<Longrightarrow> h \<unlhd> h' \<Longrightarrow> sh \<unlhd>\<^sub>s sh' \<Longrightarrow> \<not>sub_RIs es \<Longrightarrow> P,E,h',sh' \<turnstile> es [:] Ts"
  by(auto intro: WTrts_hext_mono WTrts_shext_mono)
 
 
 lemma WT_implies_WTrt: "P,E \<turnstile> e :: T \<Longrightarrow> P,E,h,sh \<turnstile> e : T"
 and WTs_implies_WTrts: "P,E \<turnstile> es [::] Ts \<Longrightarrow> P,E,h,sh \<turnstile> es [:] Ts"
 (*<*)
-apply(induct rule: WT_WTs_inducts)
-apply fast
-apply (fast)
-apply(fastforce dest:typeof_lit_typeof)
-apply(simp)
-apply(fastforce)
-apply(fastforce)
-apply(fastforce)
-apply(meson WTrtFAcc has_visible_field)
-apply(meson WTrtSFAcc has_visible_field)
-apply(meson WTrtFAss has_visible_field)
-apply(meson WTrtSFAss has_visible_field)
-apply(fastforce simp: WTrtCall)
-apply(fastforce simp: WTrtSCall)
-apply(fastforce)
-apply(fastforce)
-apply(fastforce simp: WTrtCond)
-apply(fastforce)
-apply(fastforce)
-apply(fastforce)
-apply(simp)
-apply(simp)
-done
+proof(induct rule: WT_WTs_inducts)
+  case WTVal then show ?case by(fastforce dest: typeof_lit_typeof)
+next
+  case WTFAcc
+  then show ?case by(fastforce simp: WTrtFAcc has_visible_field)
+next
+  case WTSFAcc
+  then show ?case by(fastforce simp: WTrtSFAcc has_visible_field)
+next
+  case WTFAss
+  then show ?case by(fastforce simp: WTrtFAss dest: has_visible_field)
+next
+  case WTSFAss
+  then show ?case by(fastforce simp: WTrtSFAss dest: has_visible_field)
+qed(fastforce intro: WTrt_WTrts.intros)+
 (*>*)
 
 end