# HG changeset patch
# User wenzelm
# Date 1731709224 -3600
# Node ID 1263d1143baba9008e4a9f0f87aee3c24aba53a8
# Parent  c8283b7f079183a2c46d6f82dfad0f27a5093ca0
tuned proofs;

diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -286,9 +286,8 @@
     have "G,A\<turnstile>{Normal (?P  \<and>. Not \<circ> initd C)} .Init C. {?R}" 
     proof (cases n)
       case 0
-      with is_cls
       show ?thesis
-        by - (rule ax_impossible [THEN conseq1],fastforce dest: nyinitcls_emptyD)
+        by (rule ax_impossible [THEN conseq1]) (use is_cls 0 in \<open>fastforce dest: nyinitcls_emptyD\<close>)
     next
       case (Suc m)
       with mgf_hyp have mgf_hyp': "\<And> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}"
@@ -413,18 +412,15 @@
         obtain "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT)"
           and  "s1\<Colon>\<preceq>(G, L)"
           by (rule eval_type_soundE) simp
-        moreover
-        {
-          assume normal_s1: "normal s1"
-          have "\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
-          proof -
-            from eval_e wt_e da_e wf normal_s1
-            have "nrm C \<subseteq>  dom (locals (store s1))"
-              by (cases rule: da_good_approxE') iprover
-            with da_ps show ?thesis
-              by (rule da_weakenE) iprover
-          qed
-        }
+        moreover have "\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
+          if normal_s1: "normal s1"
+        proof -
+          from eval_e wt_e da_e wf normal_s1
+          have "nrm C \<subseteq>  dom (locals (store s1))"
+            by (cases rule: da_good_approxE') iprover
+          with da_ps show ?thesis
+            by (rule da_weakenE) iprover
+        qed
         ultimately show ?thesis
           using eq_accC_accC' by simp
       qed
@@ -538,9 +534,8 @@
   and      wt: "\<lparr>prg=G, cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T" 
   and      wf: "wf_prog G"
 shows "abrupt s1 \<noteq> Some (Jump j)"
-using eval no_jmp wt wf
-by - (rule eval_expression_no_jump 
-            [where ?Env="\<lparr>prg=G, cls=C,lcl=L\<rparr>",simplified],auto)
+  by (rule eval_expression_no_jump [where ?Env="\<lparr>prg=G, cls=C,lcl=L\<rparr>",simplified])
+    (use eval no_jmp wt wf in auto)
 
 
 text \<open>To derive the most general formula for the loop statement, we need to
@@ -938,17 +933,13 @@
   fix l show "abrupt s2 \<noteq> Some (Jump (Break l)) \<and>  
               abrupt s2 \<noteq> Some (Jump (Cont l))"
   proof -
-    fix accC from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
+    fix accC
+    from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
       by auto
-    from eval_init wf
     have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
-      by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
-    from eval_c _ wt_c wf
-    show ?thesis
-      apply (rule jumpNestingOk_eval [THEN conjE, elim_format])
-      using jmpOk s1_no_jmp
-      apply auto
-      done
+      by (rule eval_statement_no_jump [OF _ _ _ wt_init]) (use eval_init wf in auto)
+    from eval_c _ wt_c wf show ?thesis
+      by (rule jumpNestingOk_eval [THEN conjE, elim_format]) (use jmpOk s1_no_jmp in auto)
   qed
 qed
 
@@ -1021,12 +1012,12 @@
   assume hyp: "\<forall> m. Suc m \<le> n \<longrightarrow> (\<forall> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
   show "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
   proof -
-  { 
     fix v e c es
     have "G,A\<turnstile>{=:n} \<langle>v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}" and 
       "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and
       "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" and  
       "G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
+      for v e c es
     proof (induct rule: compat_var.induct compat_expr.induct compat_stmt.induct compat_expr_list.induct)
       case (LVar v)
       show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
@@ -1337,7 +1328,6 @@
         apply (fastforce intro: eval.Cons)
         done
     qed
-  }
   thus ?thesis
     by (cases rule: term_cases) auto
   qed
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/AxSound.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -106,55 +106,49 @@
   assumes recursive: "G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}"
   shows "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
 proof -
-  {
-    fix n
-    assume recursive: "\<And> n. \<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>n\<Colon>t
-                              \<Longrightarrow>  \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
-    have "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
-    proof (induct n)
-      case 0
-      show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>0\<Colon>t"
-      proof -
-        {
-          fix C sig
-          assume "(C,sig) \<in> ms" 
-          have "G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
-            by (rule Methd_triple_valid2_0)
-        }
-        thus ?thesis
-          by (simp add: mtriples_def split_def)
-      qed
-    next
-      case (Suc m)
-      note hyp = \<open>\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t\<close>
-      note prem = \<open>\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t\<close>
-      show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>Suc m\<Colon>t"
+  have "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
+    if rec: "\<And>n. \<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>n\<Colon>t
+                  \<Longrightarrow>  \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}. G\<Turnstile>n\<Colon>t"
+    for n
+  proof (induct n)
+    case 0
+    show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>0\<Colon>t"
+    proof -
+      have "G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
+        if "(C,sig) \<in> ms"
+        for C sig
+        by (rule Methd_triple_valid2_0)
+      thus ?thesis
+        by (simp add: mtriples_def split_def)
+    qed
+  next
+    case (Suc m)
+    note hyp = \<open>\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t\<close>
+    note prem = \<open>\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t\<close>
+    show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>Suc m\<Colon>t"
+    proof -
+      have "G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
+        if m: "(C,sig) \<in> ms"
+        for C sig
       proof -
-        {
-          fix C sig
-          assume m: "(C,sig) \<in> ms" 
-          have "G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
-          proof -
-            from prem have prem_m: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t"
-              by (rule triples_valid2_Suc)
-            hence "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
-              by (rule hyp)
-            with prem_m
-            have "\<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>m\<Colon>t"
-              by (simp add: ball_Un)
-            hence "\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
-              by (rule recursive)
-            with m have "G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}"
-              by (auto simp add: mtriples_def split_def)
-            thus ?thesis
-              by (rule Methd_triple_valid2_SucI)
-          qed
-        }
+        from prem have prem_m: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t"
+          by (rule triples_valid2_Suc)
+        hence "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
+          by (rule hyp)
+        with prem_m
+        have "\<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>m\<Colon>t"
+          by (simp add: ball_Un)
+        hence "\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
+          by (rule rec)
+        with m have "G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}"
+          by (auto simp add: mtriples_def split_def)
         thus ?thesis
-          by (simp add: mtriples_def split_def)
+          by (rule Methd_triple_valid2_SucI)
       qed
+      thus ?thesis
+        by (simp add: mtriples_def split_def)
     qed
-  }
+  qed
   with recursive show ?thesis
     by (unfold ax_valids2_def) blast
 qed
@@ -353,19 +347,18 @@
   note valid_t = \<open>G,A|\<Turnstile>\<Colon>{t}\<close>
   moreover
   note valid_ts = \<open>G,A|\<Turnstile>\<Colon>ts\<close>
-  {
-    fix n assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
-    have "G\<Turnstile>n\<Colon>t" and "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
-    proof -
-      from valid_A valid_t show "G\<Turnstile>n\<Colon>t"
-        by (simp add: ax_valids2_def)
-    next
-      from valid_A valid_ts show "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
-        by (unfold ax_valids2_def) blast
-    qed
-    hence "\<forall>t'\<in>insert t ts. G\<Turnstile>n\<Colon>t'"
+  have "\<forall>t'\<in>insert t ts. G\<Turnstile>n\<Colon>t'"
+    if valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
+    for n
+  proof -
+    have "G\<Turnstile>n\<Colon>t"
+      using valid_A valid_t by (simp add: ax_valids2_def)
+    moreover
+    have "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
+      using valid_A valid_ts by (unfold ax_valids2_def) blast
+    ultimately show "\<forall>t'\<in>insert t ts. G\<Turnstile>n\<Colon>t'"
       by simp
-  }
+  qed
   thus ?case
     by (unfold ax_valids2_def) blast
 next
@@ -701,17 +694,19 @@
         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>init_comp_ty T\<rangle>\<^sub>s\<guillemotright> I"
       proof (cases "\<exists>C. T = Class C")
         case True
-        thus ?thesis
-          by - (rule that, (auto intro: da_Init [simplified] 
-                                        assigned.select_convs
-                              simp add: init_comp_ty_def))
+        show ?thesis
+          by (rule that)
+            (use True in
+              \<open>auto intro: da_Init [simplified] assigned.select_convs
+                simp add: init_comp_ty_def\<close>)
          (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
       next
         case False
-        thus ?thesis
-          by - (rule that, (auto intro: da_Skip [simplified] 
-                                      assigned.select_convs
-                           simp add: init_comp_ty_def))
+        show ?thesis
+          by (rule that)
+            (use False in
+              \<open>auto intro: da_Skip [simplified] assigned.select_convs
+                simp add: init_comp_ty_def\<close>)
          (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
       qed
       with valid_init P valid_A conf_s0 eval_init wt_init 
@@ -1341,40 +1336,38 @@
                   init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs \<and>.
                   (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)
                ) v s3' Z"
-      {
-        assume abrupt_s3: "\<not> normal s3"
-        have "S \<lfloor>v\<rfloor>\<^sub>e s5 Z"
-        proof -
-          from abrupt_s3 check have eq_s3'_s3: "s3'=s3"
-            by (auto simp add: check_method_access_def Let_def)
-          with R s3 invDeclC invC l abrupt_s3
-          have R': "PROP ?R"
-            by auto
-          have conf_s3': "s3'\<Colon>\<preceq>(G, Map.empty)"
-           (* we need an arbirary environment (here empty) that s2' conforms to
+      have abrupt_s3_lemma: "S \<lfloor>v\<rfloor>\<^sub>e s5 Z"
+        if abrupt_s3: "\<not> normal s3"
+      proof -
+        from abrupt_s3 check have eq_s3'_s3: "s3'=s3"
+          by (auto simp add: check_method_access_def Let_def)
+        with R s3 invDeclC invC l abrupt_s3
+        have R': "PROP ?R"
+          by auto
+        have conf_s3': "s3'\<Colon>\<preceq>(G, Map.empty)"
+          (* we need an arbirary environment (here empty) that s2' conforms to
               to apply validE *)
-          proof -
-            from s2_no_return s3
-            have "abrupt s3 \<noteq> Some (Jump Ret)"
-              by (cases s2) (auto simp add: init_lvars_def2 split: if_split_asm)
-            moreover
-            obtain abr2 str2 where s2: "s2=(abr2,str2)"
-              by (cases s2)
-            from s3 s2 conf_s2 have "(abrupt s3,str2)\<Colon>\<preceq>(G, L)"
-              by (auto simp add: init_lvars_def2 split: if_split_asm)
-            ultimately show ?thesis
-              using s3 s2 eq_s3'_s3
-              apply (simp add: init_lvars_def2)
-              apply (rule conforms_set_locals [OF _ wlconf_empty])
-              by auto
-          qed
-          from valid_methd R' valid_A conf_s3' evaln_methd abrupt_s3 eq_s3'_s3
-          have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
-            by (cases rule: validE) simp+
-          with s5 l show ?thesis
-            by simp
+        proof -
+          from s2_no_return s3
+          have "abrupt s3 \<noteq> Some (Jump Ret)"
+            by (cases s2) (auto simp add: init_lvars_def2 split: if_split_asm)
+          moreover
+          obtain abr2 str2 where s2: "s2=(abr2,str2)"
+            by (cases s2)
+          from s3 s2 conf_s2 have "(abrupt s3,str2)\<Colon>\<preceq>(G, L)"
+            by (auto simp add: init_lvars_def2 split: if_split_asm)
+          ultimately show ?thesis
+            using s3 s2 eq_s3'_s3
+            apply (simp add: init_lvars_def2)
+            apply (rule conforms_set_locals [OF _ wlconf_empty])
+            by auto
         qed
-      } note abrupt_s3_lemma = this
+        from valid_methd R' valid_A conf_s3' evaln_methd abrupt_s3 eq_s3'_s3
+        have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
+          by (cases rule: validE) simp+
+        with s5 l show ?thesis
+          by simp
+      qed
 
       have "S \<lfloor>v\<rfloor>\<^sub>e s5 Z"
       proof (cases "normal s2")
@@ -2003,187 +1996,187 @@
            evaluation relation, with all
            the necessary preconditions to apply \<open>valid_e\<close> and 
            \<open>valid_c\<close> in the goal.\<close>
-      {
-        fix t s s' v 
-        assume "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
-        hence "\<And> Y' T E. 
-                \<lbrakk>t =  \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s; \<forall>t\<in>A. G\<Turnstile>n\<Colon>t; P Y' s Z; s\<Colon>\<preceq>(G, L);
-                 normal s \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
-                 normal s \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>E
-                \<rbrakk>\<Longrightarrow> (P'\<leftarrow>=False\<down>=\<diamondsuit>) v s' Z"
+      have generalized:
+          "\<And> Y' T E.
+              \<lbrakk>t =  \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s; \<forall>t\<in>A. G\<Turnstile>n\<Colon>t; P Y' s Z; s\<Colon>\<preceq>(G, L);
+               normal s \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
+               normal s \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>E
+              \<rbrakk>\<Longrightarrow> (P'\<leftarrow>=False\<down>=\<diamondsuit>) v s' Z"
           (is "PROP ?Hyp n t s v s'")
-        proof (induct)
-          case (Loop s0' e' b n' s1' c' s2' l' s3' Y' T E)
-          note while = \<open>(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<close>
-          hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
-          note valid_A = \<open>\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t\<close>
-          note P = \<open>P Y' (Norm s0') Z\<close>
-          note conf_s0' = \<open>Norm s0'\<Colon>\<preceq>(G, L)\<close>
-          have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
-            using Loop.prems eqs by simp
-          have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
-                    dom (locals (store ((Norm s0')::state)))\<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright>E"
-            using Loop.prems eqs by simp
-          have evaln_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<midarrow>n'\<rightarrow> s1'" 
-            using Loop.hyps eqs by simp
-          show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
-          proof -
-            from wt  obtain 
-              wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
-              wt_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
-              by cases (simp add: eqs)
-            from da obtain E S where
-              da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
+        if "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
+        for t s s' v
+        using that
+      proof (induct)
+        case (Loop s0' e' b n' s1' c' s2' l' s3' Y' T E)
+        note while = \<open>(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<close>
+        hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
+        note valid_A = \<open>\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t\<close>
+        note P = \<open>P Y' (Norm s0') Z\<close>
+        note conf_s0' = \<open>Norm s0'\<Colon>\<preceq>(G, L)\<close>
+        have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
+          using Loop.prems eqs by simp
+        have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
+                  dom (locals (store ((Norm s0')::state)))\<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright>E"
+          using Loop.prems eqs by simp
+        have evaln_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<midarrow>n'\<rightarrow> s1'" 
+          using Loop.hyps eqs by simp
+        show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
+        proof -
+          from wt  obtain 
+            wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
+            wt_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
+            by cases (simp add: eqs)
+          from da obtain E S where
+            da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                      \<turnstile> dom (locals (store ((Norm s0')::state))) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
-              da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
+            da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                      \<turnstile> (dom (locals (store ((Norm s0')::state))) 
                             \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> S"
-              by cases (simp add: eqs)
-            from evaln_e 
-            have eval_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<rightarrow> s1'"
-              by (rule evaln_eval)
-            from valid_e P valid_A conf_s0' evaln_e wt_e da_e
-            obtain P': "P' \<lfloor>b\<rfloor>\<^sub>e s1' Z" and conf_s1': "s1'\<Colon>\<preceq>(G,L)"
-              by (rule validE)
-            show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
-            proof (cases "normal s1'")
+            by cases (simp add: eqs)
+          from evaln_e 
+          have eval_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<rightarrow> s1'"
+            by (rule evaln_eval)
+          from valid_e P valid_A conf_s0' evaln_e wt_e da_e
+          obtain P': "P' \<lfloor>b\<rfloor>\<^sub>e s1' Z" and conf_s1': "s1'\<Colon>\<preceq>(G,L)"
+            by (rule validE)
+          show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
+          proof (cases "normal s1'")
+            case True
+            note normal_s1'=this
+            show ?thesis
+            proof (cases "the_Bool b")
               case True
-              note normal_s1'=this
+              with P' normal_s1' have P'': "(Normal (P'\<leftarrow>=True)) \<lfloor>b\<rfloor>\<^sub>e s1' Z"
+                by auto
+              from True Loop.hyps obtain
+                eval_c: "G\<turnstile>s1' \<midarrow>c\<midarrow>n'\<rightarrow> s2'" and 
+                eval_while:  
+                "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> s3'"
+                by (simp add: eqs)
+              from True Loop.hyps have
+                hyp: "PROP ?Hyp n' \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s 
+                          (abupd (absorb (Cont l')) s2') \<diamondsuit> s3'"
+                apply (simp only: True if_True eqs)
+                apply (elim conjE)
+                apply (tactic "smp_tac \<^context> 3 1")
+                apply fast
+                done
+              from eval_e
+              have s0'_s1': "dom (locals (store ((Norm s0')::state))) 
+                                  \<subseteq> dom (locals (store s1'))"
+                by (rule dom_locals_eval_mono_elim)
+              obtain S' where
+                da_c':
+                "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(dom (locals (store s1')))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> S'" 
+              proof -
+                note s0'_s1'
+                moreover
+                from eval_e normal_s1' wt_e 
+                have "assigns_if True e \<subseteq> dom (locals (store s1'))"
+                  by (rule assigns_if_good_approx' [elim_format]) 
+                    (simp add: True)
+                ultimately 
+                have "dom (locals (store ((Norm s0')::state)))
+                           \<union> assigns_if True e \<subseteq> dom (locals (store s1'))"
+                  by (rule Un_least)
+                with da_c show thesis
+                  by (rule da_weakenE) (rule that)
+              qed
+              with valid_c P'' valid_A conf_s1' eval_c wt_c
+              obtain "(abupd (absorb (Cont l)) .; P) \<diamondsuit> s2' Z" and 
+                conf_s2': "s2'\<Colon>\<preceq>(G,L)"
+                by (rule validE)
+              hence P_s2': "P \<diamondsuit> (abupd (absorb (Cont l)) s2') Z"
+                by simp
+              from conf_s2'
+              have conf_absorb: "abupd (absorb (Cont l)) s2' \<Colon>\<preceq>(G, L)"
+                by (cases s2') (auto intro: conforms_absorb)
+              moreover
+              obtain E' where 
+                da_while':
+                "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
+                     dom (locals(store (abupd (absorb (Cont l)) s2')))
+                      \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright> E'"
+              proof -
+                note s0'_s1'
+                also 
+                from eval_c 
+                have "G\<turnstile>s1' \<midarrow>c\<rightarrow> s2'"
+                  by (rule evaln_eval)
+                hence "dom (locals (store s1')) \<subseteq> dom (locals (store s2'))"
+                  by (rule dom_locals_eval_mono_elim)
+                also 
+                have "\<dots>\<subseteq>dom (locals (store (abupd (absorb (Cont l)) s2')))"
+                  by simp
+                finally
+                have "dom (locals (store ((Norm s0')::state))) \<subseteq> \<dots>" .
+                with da show thesis
+                  by (rule da_weakenE) (rule that)
+              qed
+              from valid_A P_s2' conf_absorb wt da_while'
+              show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z" 
+                using hyp by (simp add: eqs)
+            next
+              case False
+              with Loop.hyps obtain "s3'=s1'"
+                by simp
+              with P' False show ?thesis
+                by auto
+            qed 
+          next
+            case False
+            note abnormal_s1'=this
+            have "s3'=s1'"
+            proof -
+              from False obtain abr where abr: "abrupt s1' = Some abr"
+                by (cases s1') auto
+              from eval_e _ wt_e wf
+              have no_jmp: "\<And> j. abrupt s1' \<noteq> Some (Jump j)"
+                by (rule eval_expression_no_jump 
+                    [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
+                  simp
               show ?thesis
               proof (cases "the_Bool b")
-                case True
-                with P' normal_s1' have P'': "(Normal (P'\<leftarrow>=True)) \<lfloor>b\<rfloor>\<^sub>e s1' Z"
-                  by auto
-                from True Loop.hyps obtain
+                case True  
+                with Loop.hyps obtain
                   eval_c: "G\<turnstile>s1' \<midarrow>c\<midarrow>n'\<rightarrow> s2'" and 
                   eval_while:  
-                     "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> s3'"
+                  "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> s3'"
                   by (simp add: eqs)
-                from True Loop.hyps have
-                  hyp: "PROP ?Hyp n' \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s 
-                          (abupd (absorb (Cont l')) s2') \<diamondsuit> s3'"
-                  apply (simp only: True if_True eqs)
-                  apply (elim conjE)
-                  apply (tactic "smp_tac \<^context> 3 1")
-                  apply fast
-                  done
-                from eval_e
-                have s0'_s1': "dom (locals (store ((Norm s0')::state))) 
-                                  \<subseteq> dom (locals (store s1'))"
-                  by (rule dom_locals_eval_mono_elim)
-                obtain S' where
-                  da_c':
-                   "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(dom (locals (store s1')))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> S'" 
-                proof -
-                  note s0'_s1'
-                  moreover
-                  from eval_e normal_s1' wt_e 
-                  have "assigns_if True e \<subseteq> dom (locals (store s1'))"
-                    by (rule assigns_if_good_approx' [elim_format]) 
-                       (simp add: True)
-                  ultimately 
-                  have "dom (locals (store ((Norm s0')::state)))
-                           \<union> assigns_if True e \<subseteq> dom (locals (store s1'))"
-                    by (rule Un_least)
-                  with da_c show thesis
-                    by (rule da_weakenE) (rule that)
-                qed
-                with valid_c P'' valid_A conf_s1' eval_c wt_c
-                obtain "(abupd (absorb (Cont l)) .; P) \<diamondsuit> s2' Z" and 
-                  conf_s2': "s2'\<Colon>\<preceq>(G,L)"
-                  by (rule validE)
-                hence P_s2': "P \<diamondsuit> (abupd (absorb (Cont l)) s2') Z"
-                  by simp
-                from conf_s2'
-                have conf_absorb: "abupd (absorb (Cont l)) s2' \<Colon>\<preceq>(G, L)"
-                  by (cases s2') (auto intro: conforms_absorb)
-                moreover
-                obtain E' where 
-                  da_while':
-                   "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
-                     dom (locals(store (abupd (absorb (Cont l)) s2')))
-                      \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright> E'"
-                proof -
-                  note s0'_s1'
-                  also 
-                  from eval_c 
-                  have "G\<turnstile>s1' \<midarrow>c\<rightarrow> s2'"
-                    by (rule evaln_eval)
-                  hence "dom (locals (store s1')) \<subseteq> dom (locals (store s2'))"
-                    by (rule dom_locals_eval_mono_elim)
-                  also 
-                  have "\<dots>\<subseteq>dom (locals (store (abupd (absorb (Cont l)) s2')))"
-                    by simp
-                  finally
-                  have "dom (locals (store ((Norm s0')::state))) \<subseteq> \<dots>" .
-                  with da show thesis
-                    by (rule da_weakenE) (rule that)
-                qed
-                from valid_A P_s2' conf_absorb wt da_while'
-                show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z" 
-                  using hyp by (simp add: eqs)
+                from eval_c abr have "s2'=s1'" by auto
+                moreover from calculation no_jmp 
+                have "abupd (absorb (Cont l)) s2'=s2'"
+                  by (cases s1') (simp add: absorb_def)
+                ultimately show ?thesis
+                  using eval_while abr
+                  by auto
               next
                 case False
-                with Loop.hyps obtain "s3'=s1'"
-                  by simp
-                with P' False show ?thesis
-                  by auto
-              qed 
-            next
-              case False
-              note abnormal_s1'=this
-              have "s3'=s1'"
-              proof -
-                from False obtain abr where abr: "abrupt s1' = Some abr"
-                  by (cases s1') auto
-                from eval_e _ wt_e wf
-                have no_jmp: "\<And> j. abrupt s1' \<noteq> Some (Jump j)"
-                  by (rule eval_expression_no_jump 
-                       [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
-                     simp
-                show ?thesis
-                proof (cases "the_Bool b")
-                  case True  
-                  with Loop.hyps obtain
-                    eval_c: "G\<turnstile>s1' \<midarrow>c\<midarrow>n'\<rightarrow> s2'" and 
-                    eval_while:  
-                     "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> s3'"
-                    by (simp add: eqs)
-                  from eval_c abr have "s2'=s1'" by auto
-                  moreover from calculation no_jmp 
-                  have "abupd (absorb (Cont l)) s2'=s2'"
-                    by (cases s1') (simp add: absorb_def)
-                  ultimately show ?thesis
-                    using eval_while abr
-                    by auto
-                next
-                  case False
-                  with Loop.hyps show ?thesis by simp
-                qed
+                with Loop.hyps show ?thesis by simp
               qed
-              with P' False show ?thesis
-                by auto
             qed
-          qed
-        next
-          case (Abrupt abr s t' n' Y' T E)
-          note t' = \<open>t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<close>
-          note conf = \<open>(Some abr, s)\<Colon>\<preceq>(G, L)\<close>
-          note P = \<open>P Y' (Some abr, s) Z\<close>
-          note valid_A = \<open>\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t\<close>
-          show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (undefined3 t') (Some abr, s) Z"
-          proof -
-            have eval_e: 
-              "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (undefined3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
-              by auto
-            from valid_e P valid_A conf eval_e 
-            have "P' (undefined3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
-              by (cases rule: validE [where ?P="P"]) simp+
-            with t' show ?thesis
+            with P' False show ?thesis
               by auto
           qed
-        qed simp_all
-      } note generalized=this
+        qed
+      next
+        case (Abrupt abr s t' n' Y' T E)
+        note t' = \<open>t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<close>
+        note conf = \<open>(Some abr, s)\<Colon>\<preceq>(G, L)\<close>
+        note P = \<open>P Y' (Some abr, s) Z\<close>
+        note valid_A = \<open>\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t\<close>
+        show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (undefined3 t') (Some abr, s) Z"
+        proof -
+          have eval_e: 
+            "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (undefined3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
+            by auto
+          from valid_e P valid_A conf eval_e 
+          have "P' (undefined3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
+            by (cases rule: validE [where ?P="P"]) simp+
+          with t' show ?thesis
+            by auto
+        qed
+      qed simp_all
       from eval _ valid_A P conf_s0 wt da
       have "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3 Z"
         by (rule generalized)  simp_all
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/Decl.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -68,24 +68,20 @@
 instance
 proof
   fix x y z::acc_modi
-  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
+  show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
     by (auto simp add: le_acc_def less_acc_def split: acc_modi.split) 
   show "x \<le> x"                       \<comment> \<open>reflexivity\<close>
     by (auto simp add: le_acc_def)
-  {
-    assume "x \<le> y" "y \<le> z"           \<comment> \<open>transitivity\<close> 
-    then show "x \<le> z"
-      by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
-  next
-    assume "x \<le> y" "y \<le> x"           \<comment> \<open>antisymmetry\<close>
-    moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
+  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"  \<comment> \<open>transitivity\<close>
+    by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
+  show "x = y" if "x \<le> y" "y \<le> x"   \<comment> \<open>antisymmetry\<close>
+  proof -
+    have "\<forall>x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
       by (auto simp add: less_acc_def split: acc_modi.split)
-    ultimately show "x = y" by (unfold le_acc_def) iprover
-  next
-    fix x y:: acc_modi
-    show "x \<le> y \<or> y \<le> x"   
-      by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
-  }
+    with that show ?thesis by (unfold le_acc_def) iprover
+  qed
+  show "x \<le> y \<or> y \<le> x"
+    by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
 qed
   
 end
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -1019,9 +1019,8 @@
        (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
 next
   case (Inherited m C S)  
-  assume "G\<turnstile>C\<prec>\<^sub>C1S" and "is_class G S"
-  then show "is_class G C"
-    by - (rule subcls_is_class2,auto)
+  show "is_class G C" if "G\<turnstile>C\<prec>\<^sub>C1S" and "is_class G S"
+    by (rule subcls_is_class2) (use that in auto)
 qed
 
 lemma member_of_declC: 
@@ -2336,13 +2335,13 @@
   shows "D\<in>superclasses G C" using clsrel cls_C
 proof (induct arbitrary: c rule: converse_trancl_induct)
   case (base C)
-  with ws wf show ?case
-    by (auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def)
+  show ?case
+    by (use ws wf base in \<open>auto intro: no_subcls1_Object simp add: superclasses_rec subcls1_def\<close>)
 next
   case (step C S)
-  with ws wf show ?case
-    by - (rule superclasses_mono,
-          auto dest: no_subcls1_Object simp add: subcls1_def )
+  show ?case
+    by (rule superclasses_mono)
+      (use ws wf step in \<open>auto dest: no_subcls1_Object simp add: subcls1_def\<close>)
 qed
 
 end
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -974,7 +974,7 @@
       by (elim wt_elim_cases) simp
     with BinOp.hyps
     show ?case
-      by - (cases binop, auto simp add: assignsE_const_simp)
+      by (cases binop) (auto simp add: assignsE_const_simp)
   next
     case (Cond c e1 e2)
     note hyp_c = \<open>?Boolean c \<Longrightarrow> ?Incl c\<close>
@@ -1073,12 +1073,9 @@
     then 
     have "nrm C \<inter> brk C l \<subseteq> nrm C' \<inter> brk C' l" by auto
     moreover
-    {
-      fix l'
-      from hyp_brk
-      have "rmlab l (brk C) l'  \<subseteq> rmlab l (brk C') l'"
-        by  (cases "l=l'") simp_all
-    }
+    from hyp_brk
+    have "rmlab l (brk C) l'  \<subseteq> rmlab l (brk C') l'" for l'
+      by  (cases "l=l'") simp_all
     moreover note A A'
     ultimately show ?case
       by simp
@@ -1143,20 +1140,18 @@
     have "nrm A \<subseteq> nrm A'"
       by blast
     moreover
-    { fix l'
-      have  "brk A l' \<subseteq> brk A' l'"
-      proof (cases "constVal e")
-        case None
-        with A A' C' 
-        show ?thesis
-           by (cases "l=l'") auto
-      next
-        case (Some bv)
-        with A A' C'
-        show ?thesis
-          by (cases "the_Bool bv", cases "l=l'") auto
-      qed
-    }
+    have  "brk A l' \<subseteq> brk A' l'" for l'
+    proof (cases "constVal e")
+      case None
+      with A A' C' 
+      show ?thesis
+        by (cases "l=l'") auto
+    next
+      case (Some bv)
+      with A A' C'
+      show ?thesis
+        by (cases "the_Bool bv", cases "l=l'") auto
+    qed
     ultimately show ?case
       by auto
   next
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -119,45 +119,38 @@
       by (cases j) auto
   next
     case (Comp c1 c2 jmps' jmps)
-    from Comp.prems 
-    have "jumpNestingOkS jmps c1" by - (rule Comp.hyps,auto)
-    moreover from Comp.prems
-    have "jumpNestingOkS jmps c2" by - (rule Comp.hyps,auto)
-    ultimately show ?case
-      by simp
+    have "jumpNestingOkS jmps c1" by (rule Comp.hyps) (use Comp.prems in auto)
+    moreover
+    have "jumpNestingOkS jmps c2" by (rule Comp.hyps) (use Comp.prems in auto)
+    ultimately show ?case by simp
   next
     case (If' e c1 c2 jmps' jmps)
-    from If'.prems 
-    have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto)
-    moreover from If'.prems 
-    have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto)
-    ultimately show ?case
-      by simp
+    have "jumpNestingOkS jmps c1" by (rule If'.hyps) (use If'.prems in auto)
+    moreover
+    have "jumpNestingOkS jmps c2" by (rule If'.hyps) (use If'.prems in auto)
+    ultimately show ?case by simp
   next
     case (Loop l e c jmps' jmps)
-    from \<open>jumpNestingOkS jmps' (l\<bullet> While(e) c)\<close>
-    have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
+    from \<open>jumpNestingOkS jmps' (l\<bullet> While(e) c)\<close> have "jumpNestingOkS ({Cont l} \<union> jmps') c"
+      by simp
     moreover
-    from \<open>jmps' \<subseteq> jmps\<close>
-    have "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps" by auto
-    ultimately
-    have "jumpNestingOkS ({Cont l} \<union> jmps) c"
+    from \<open>jmps' \<subseteq> jmps\<close> have "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps"
+      by auto
+    ultimately have "jumpNestingOkS ({Cont l} \<union> jmps) c"
       by (rule Loop.hyps)
     thus ?case by simp
   next
     case (TryC c1 C vn c2 jmps' jmps)
-    from TryC.prems 
-    have "jumpNestingOkS jmps c1" by - (rule TryC.hyps,auto)
-    moreover from TryC.prems 
-    have "jumpNestingOkS jmps c2" by - (rule TryC.hyps,auto)
+    have "jumpNestingOkS jmps c1" by (rule TryC.hyps) (use TryC.prems in auto)
+    moreover 
+    have "jumpNestingOkS jmps c2" by (rule TryC.hyps) (use TryC.prems in auto)
     ultimately show ?case
       by simp
   next
     case (Fin c1 c2 jmps' jmps)
-    from Fin.prems 
-    have "jumpNestingOkS jmps c1" by - (rule Fin.hyps,auto)
-    moreover from Fin.prems 
-    have "jumpNestingOkS jmps c2" by - (rule Fin.hyps,auto)
+    have "jumpNestingOkS jmps c1" by (rule Fin.hyps) (use Fin.prems in auto)
+    moreover
+    have "jumpNestingOkS jmps c2" by (rule Fin.hyps) (use Fin.prems in auto)
     ultimately show ?case
       by simp
   qed (simp_all)
@@ -312,28 +305,24 @@
     note G = \<open>prg Env = G\<close>
     have wt_c: "Env\<turnstile>c\<Colon>\<surd>" 
       using Lab.prems by (elim wt_elim_cases)
-    { 
-      fix j
-      assume ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)"
-      have "j\<in>jmps"          
+    have "j\<in>jmps" if ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)" for j
+    proof -
+      from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
+        by (cases s1) (simp add: absorb_def)
+      note hyp_c = \<open>PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>\<close>
+      from ab_s1 have "j \<noteq> jmp" 
+        by (cases s1) (simp add: absorb_def)
+      moreover have "j \<in> {jmp} \<union> jmps"
       proof -
-        from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
-          by (cases s1) (simp add: absorb_def)
-        note hyp_c = \<open>PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>\<close>
-        from ab_s1 have "j \<noteq> jmp" 
-          by (cases s1) (simp add: absorb_def)
-        moreover have "j \<in> {jmp} \<union> jmps"
-        proof -
-          from jmpOK 
-          have "jumpNestingOk ({jmp} \<union> jmps) (In1r c)" by simp
-          with wt_c jmp_s1 G hyp_c
-          show ?thesis
-            by - (rule hyp_c [THEN conjunct1,rule_format],simp)
-        qed
-        ultimately show ?thesis
-          by simp
+        from jmpOK 
+        have "jumpNestingOk ({jmp} \<union> jmps) (In1r c)" by simp
+        with wt_c jmp_s1 G hyp_c
+        show ?thesis
+          by - (rule hyp_c [THEN conjunct1,rule_format],simp)
       qed
-    }
+      ultimately show ?thesis
+        by simp
+    qed
     thus ?case by simp
   next
     case (Comp s0 c1 s1 c2 s2 jmps T Env)
@@ -342,24 +331,21 @@
     from Comp.prems obtain
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
-    {
-      fix j
-      assume abr_s2: "abrupt s2 = Some (Jump j)"
-      have "j\<in>jmps"
+    have "j\<in>jmps" if abr_s2: "abrupt s2 = Some (Jump j)" for j
+    proof -
+      have jmp: "?Jmp jmps s1"
       proof -
-        have jmp: "?Jmp jmps s1"
-        proof -
-          note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>\<close>
-          with wt_c1 jmpOk G 
-          show ?thesis by simp
-        qed
-        moreover note hyp_c2 = \<open>PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)\<close>
-        have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
-        moreover note wt_c2 G abr_s2
-        ultimately show "j \<in> jmps"
-          by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
+        note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>\<close>
+        with wt_c1 jmpOk G 
+        show ?thesis by simp
       qed
-    } thus ?case by simp
+      moreover note hyp_c2 = \<open>PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)\<close>
+      have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
+      moreover note wt_c2 G abr_s2
+      ultimately show "j \<in> jmps"
+        by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
+    qed
+    thus ?case by simp
   next
     case (If s0 e b s1 c1 c2 s2 jmps T Env)
     note jmpOk = \<open>jumpNestingOk jmps (In1r (If(e) c1 Else c2))\<close>
@@ -368,23 +354,19 @@
               wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
       wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
       by (elim wt_elim_cases) simp
-    { 
-      fix j
-      assume jmp: "abrupt s2 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
-        with wt_e G have "?Jmp jmps s1" 
-          by simp
-        moreover note hyp_then_else =
-          \<open>PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>\<close>
-        have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
-          using jmpOk by (cases "the_Bool b") simp_all
-        moreover note wt_then_else G jmp
-        ultimately show "j\<in> jmps" 
-          by (rule hyp_then_else [THEN conjunct1,rule_format (no_asm)])
-      qed
-    }
+    have "j\<in>jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
+    proof -
+      note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
+      with wt_e G have "?Jmp jmps s1" 
+        by simp
+      moreover note hyp_then_else =
+        \<open>PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>\<close>
+      have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
+        using jmpOk by (cases "the_Bool b") simp_all
+      moreover note wt_then_else G jmp
+      ultimately show "j\<in> jmps" 
+        by (rule hyp_then_else [THEN conjunct1,rule_format (no_asm)])
+    qed
     thus ?case by simp
   next
     case (Loop s0 e b s1 c s2 l s3 jmps T Env)
@@ -395,74 +377,66 @@
               wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
               wt_c: "Env\<turnstile>c\<Colon>\<surd>"
       by (elim wt_elim_cases)
-    {
-      fix j
-      assume jmp: "abrupt s3 = Some (Jump j)" 
-      have "j\<in>jmps"
-      proof -
-        note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
-        with wt_e G have jmp_s1: "?Jmp jmps s1" 
-          by simp
-        show ?thesis
-        proof (cases "the_Bool b")
-          case False
-          from Loop.hyps
-          have "s3=s1"
-            by (simp (no_asm_use) only: if_False False) 
-          with jmp_s1 jmp have "j \<in> jmps" by simp
-          thus ?thesis by simp
-        next
-          case True
-          from Loop.hyps 
-            (* Because of the mixture of object and pure logic in the rule 
+    have "j\<in>jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
+    proof -
+      note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
+      with wt_e G have jmp_s1: "?Jmp jmps s1" 
+        by simp
+      show ?thesis
+      proof (cases "the_Bool b")
+        case False
+        from Loop.hyps
+        have "s3=s1"
+          by (simp (no_asm_use) only: if_False False) 
+        with jmp_s1 jmp have "j \<in> jmps" by simp
+        thus ?thesis by simp
+      next
+        case True
+        from Loop.hyps 
+          (* Because of the mixture of object and pure logic in the rule 
                eval.If the atomization-rulification of the induct method 
                leaves the hypothesis in object logic *)
-          have "?HypObj (In1r c) s1 s2 (\<diamondsuit>::vals)"
-            apply (simp (no_asm_use) only: True if_True )
-            apply (erule conjE)+
-            apply assumption
-            done
-          note hyp_c = this [rule_format (no_asm)]
-          moreover from jmpOk have "jumpNestingOk ({Cont l} \<union> jmps) (In1r c)"
-            by simp
-          moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
-          ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2" 
-            using wt_c G by iprover
-          have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
-          proof -
-            {
-              fix j'
-              assume abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')"
-              have "j' \<in> jmps"
-              proof (cases "j' = Cont l")
-                case True
-                with abs show ?thesis
-                  by (cases s2) (simp add: absorb_def)
-              next
-                case False 
-                with abs have "abrupt s2 = Some (Jump j')"
-                  by (cases s2) (simp add: absorb_def) 
-                with jmp_s2 False show ?thesis
-                  by simp
-              qed
-            }
-            thus ?thesis by simp
+        have "?HypObj (In1r c) s1 s2 (\<diamondsuit>::vals)"
+          apply (simp (no_asm_use) only: True if_True )
+          apply (erule conjE)+
+          apply assumption
+          done
+        note hyp_c = this [rule_format (no_asm)]
+        moreover from jmpOk have "jumpNestingOk ({Cont l} \<union> jmps) (In1r c)"
+          by simp
+        moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
+        ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2" 
+          using wt_c G by iprover
+        have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
+        proof -
+          have "j' \<in> jmps" if abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')" for j'
+          proof (cases "j' = Cont l")
+            case True
+            with abs show ?thesis
+              by (cases s2) (simp add: absorb_def)
+          next
+            case False 
+            with abs have "abrupt s2 = Some (Jump j')"
+              by (cases s2) (simp add: absorb_def) 
+            with jmp_s2 False show ?thesis
+              by simp
           qed
-          moreover
-          from Loop.hyps
-          have "?HypObj (In1r (l\<bullet> While(e) c)) 
+          thus ?thesis by simp
+        qed
+        moreover
+        from Loop.hyps
+        have "?HypObj (In1r (l\<bullet> While(e) c)) 
                         (abupd (absorb (Cont l)) s2) s3 (\<diamondsuit>::vals)"
-            apply (simp (no_asm_use) only: True if_True)
-            apply (erule conjE)+
-            apply assumption
-            done
-          note hyp_w = this [rule_format (no_asm)]
-          note jmpOk wt G jmp 
-          ultimately show "j\<in> jmps" 
-            by (rule hyp_w [THEN conjunct1,rule_format (no_asm)])
-        qed
+          apply (simp (no_asm_use) only: True if_True)
+          apply (erule conjE)+
+          apply assumption
+          done
+        note hyp_w = this [rule_format (no_asm)]
+        note jmpOk wt G jmp 
+        ultimately show "j\<in> jmps" 
+          by (rule hyp_w [THEN conjunct1,rule_format (no_asm)])
       qed
-    }
+    qed
     thus ?case by simp
   next
     case (Jmp s j jmps T Env) thus ?case by simp
@@ -473,20 +447,16 @@
     from Throw.prems obtain Te where 
       wt_e: "Env\<turnstile>e\<Colon>-Te" 
       by (elim wt_elim_cases)
-    {
-      fix j
-      assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        from \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
-        have "?Jmp jmps s1" using wt_e G by simp
-        moreover
-        from jmp 
-        have "abrupt s1 = Some (Jump j)"
-          by (cases s1) (simp add: throw_def abrupt_if_def)
-        ultimately show "j \<in> jmps" by simp
-      qed
-    }
+    have "j\<in>jmps" if jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)" for j
+    proof -
+      from \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
+      have "?Jmp jmps s1" using wt_e G by simp
+      moreover
+      from jmp 
+      have "abrupt s1 = Some (Jump j)"
+        by (cases s1) (simp add: throw_def abrupt_if_def)
+      ultimately show "j \<in> jmps" by simp
+    qed
     thus ?case by simp
   next
     case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
@@ -496,49 +466,45 @@
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and  
       wt_c2: "Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
-    {
-      fix j
-      assume jmp: "abrupt s3 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)\<close>
-        with jmpOk wt_c1 G
-        have jmp_s1: "?Jmp jmps s1" by simp
-        note s2 = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
-        show "j \<in> jmps"
-        proof (cases "G,s2\<turnstile>catch C")
-          case False
-          from Try.hyps have "s3=s2" 
-            by (simp (no_asm_use) only: False if_False)
-          with jmp have "abrupt s1 = Some (Jump j)"
-            using sxalloc_no_jump' [OF s2] by simp
-          with jmp_s1 
-          show ?thesis by simp
-        next
-          case True
-          with Try.hyps 
-          have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3 (\<diamondsuit>::vals)"
-            apply (simp (no_asm_use) only: True if_True simp_thms)
-            apply (erule conjE)+
-            apply assumption
-            done
-          note hyp_c2 = this [rule_format (no_asm)]
-          from jmp_s1 sxalloc_no_jump' [OF s2] 
-          have "?Jmp jmps s2"
-            by simp
-          hence "?Jmp jmps (new_xcpt_var vn s2)"
-            by (cases s2) simp
-          moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
-          moreover note wt_c2
-          moreover from G 
-          have "prg (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>) = G"
-            by simp
-          moreover note jmp
-          ultimately show ?thesis 
-            by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
-        qed
+    have "j\<in>jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
+    proof -
+      note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)\<close>
+      with jmpOk wt_c1 G
+      have jmp_s1: "?Jmp jmps s1" by simp
+      note s2 = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
+      show "j \<in> jmps"
+      proof (cases "G,s2\<turnstile>catch C")
+        case False
+        from Try.hyps have "s3=s2" 
+          by (simp (no_asm_use) only: False if_False)
+        with jmp have "abrupt s1 = Some (Jump j)"
+          using sxalloc_no_jump' [OF s2] by simp
+        with jmp_s1 
+        show ?thesis by simp
+      next
+        case True
+        with Try.hyps 
+        have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3 (\<diamondsuit>::vals)"
+          apply (simp (no_asm_use) only: True if_True simp_thms)
+          apply (erule conjE)+
+          apply assumption
+          done
+        note hyp_c2 = this [rule_format (no_asm)]
+        from jmp_s1 sxalloc_no_jump' [OF s2] 
+        have "?Jmp jmps s2"
+          by simp
+        hence "?Jmp jmps (new_xcpt_var vn s2)"
+          by (cases s2) simp
+        moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
+        moreover note wt_c2
+        moreover from G 
+        have "prg (Env\<lparr>lcl := (lcl Env)(VName vn\<mapsto>Class C)\<rparr>) = G"
+          by simp
+        moreover note jmp
+        ultimately show ?thesis 
+          by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
       qed
-    }
+    qed
     thus ?case by simp
   next
     case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
@@ -547,26 +513,22 @@
     from Fin.prems obtain 
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
-    {
-      fix j
-      assume jmp: "abrupt s3 = Some (Jump j)" 
-      have "j \<in> jmps"
-      proof (cases "x1=Some (Jump j)")
-        case True
-        note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>\<close>
-        with True jmpOk wt_c1 G show ?thesis 
-          by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
-      next
-        case False
-        note hyp_c2 = \<open>PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>\<close>
-        note \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+    have "j \<in> jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
+    proof (cases "x1=Some (Jump j)")
+      case True
+      note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>\<close>
+      with True jmpOk wt_c1 G show ?thesis 
+        by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
+    next
+      case False
+      note hyp_c2 = \<open>PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>\<close>
+      note \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>
-        with False jmp have "abrupt s2 = Some (Jump j)"
-          by (cases s2) (simp add: abrupt_if_def)
-        with jmpOk wt_c2 G show ?thesis 
-          by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)
-      qed
-    }
+      with False jmp have "abrupt s2 = Some (Jump j)"
+        by (cases s2) (simp add: abrupt_if_def)
+      with jmpOk wt_c2 G show ?thesis 
+        by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)
+    qed
     thus ?case by simp
   next
     case (Init C c s0 s3 s1 s2 jmps T Env)
@@ -575,227 +537,195 @@
     note \<open>the (class G C) = c\<close>
     with Init.prems have c: "class G C = Some c"
       by (elim wt_elim_cases) auto
-    {
-      fix j
-      assume jmp: "abrupt s3 = (Some (Jump j))" 
-      have "j\<in>jmps"
-      proof (cases "inited C (globs s0)") 
-        case True
-        with Init.hyps have "s3=Norm s0"
-          by simp
-        with jmp
-        have "False" by simp thus ?thesis ..
-      next
-        case False
-        from wf c G
-        have wf_cdecl: "wf_cdecl G (C,c)"
-          by (simp add: wf_prog_cdecl)
-        from Init.hyps
-        have "?HypObj (In1r (if C = Object then Skip else Init (super c))) 
+    have "j\<in>jmps" if jmp: "abrupt s3 = (Some (Jump j))" for j
+    proof (cases "inited C (globs s0)") 
+      case True
+      with Init.hyps have "s3=Norm s0"
+        by simp
+      with jmp have "False"
+        by simp
+      thus ?thesis ..
+    next
+      case False
+      from wf c G
+      have wf_cdecl: "wf_cdecl G (C,c)"
+        by (simp add: wf_prog_cdecl)
+      from Init.hyps
+      have "?HypObj (In1r (if C = Object then Skip else Init (super c))) 
                             (Norm ((init_class_obj G C) s0)) s1 (\<diamondsuit>::vals)"
-          apply (simp (no_asm_use) only: False if_False simp_thms)
-          apply (erule conjE)+
-          apply assumption
-          done
-        note hyp_s1 = this [rule_format (no_asm)]
-        from wf_cdecl G have
-          wt_super: "Env\<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
-          by (cases "C=Object")
-             (auto dest: wf_cdecl_supD is_acc_classD) 
-        from hyp_s1 [OF _ _ wt_super G]
-        have "?Jmp jmps s1" 
-          by simp
-        hence jmp_s1: "?Jmp jmps ((set_lvars Map.empty) s1)" by (cases s1) simp
-        from False Init.hyps
-        have "?HypObj (In1r (init c)) ((set_lvars Map.empty) s1) s2 (\<diamondsuit>::vals)" 
-          apply (simp (no_asm_use) only: False if_False simp_thms)
-          apply (erule conjE)+
-          apply assumption
-          done
-        note hyp_init_c = this [rule_format (no_asm)] 
-        from wf_cdecl 
-        have wt_init_c: "\<lparr>prg = G, cls = C, lcl = Map.empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
-          by (rule wf_cdecl_wt_init)
-        from wf_cdecl have "jumpNestingOkS {} (init c)" 
-          by (cases rule: wf_cdeclE)
-        hence "jumpNestingOkS jmps (init c)"
-          by (rule jumpNestingOkS_mono) simp
-        moreover 
-        have "abrupt s2 = Some (Jump j)"
-        proof -
-          from False Init.hyps 
-          have "s3 = (set_lvars (locals (store s1))) s2"  by simp
-          with jmp show ?thesis by (cases s2) simp
-        qed
-        ultimately show ?thesis
-          using hyp_init_c [OF jmp_s1 _ wt_init_c]
-          by simp
+        apply (simp (no_asm_use) only: False if_False simp_thms)
+        apply (erule conjE)+
+        apply assumption
+        done
+      note hyp_s1 = this [rule_format (no_asm)]
+      from wf_cdecl G have
+        wt_super: "Env\<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
+        by (cases "C=Object")
+          (auto dest: wf_cdecl_supD is_acc_classD) 
+      from hyp_s1 [OF _ _ wt_super G]
+      have "?Jmp jmps s1" 
+        by simp
+      hence jmp_s1: "?Jmp jmps ((set_lvars Map.empty) s1)" by (cases s1) simp
+      from False Init.hyps
+      have "?HypObj (In1r (init c)) ((set_lvars Map.empty) s1) s2 (\<diamondsuit>::vals)" 
+        apply (simp (no_asm_use) only: False if_False simp_thms)
+        apply (erule conjE)+
+        apply assumption
+        done
+      note hyp_init_c = this [rule_format (no_asm)] 
+      from wf_cdecl 
+      have wt_init_c: "\<lparr>prg = G, cls = C, lcl = Map.empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
+        by (rule wf_cdecl_wt_init)
+      from wf_cdecl have "jumpNestingOkS {} (init c)" 
+        by (cases rule: wf_cdeclE)
+      hence "jumpNestingOkS jmps (init c)"
+        by (rule jumpNestingOkS_mono) simp
+      moreover 
+      have "abrupt s2 = Some (Jump j)"
+      proof -
+        from False Init.hyps 
+        have "s3 = (set_lvars (locals (store s1))) s2"  by simp
+        with jmp show ?thesis by (cases s2) simp
       qed
-    }
+      ultimately show ?thesis
+        using hyp_init_c [OF jmp_s1 _ wt_init_c]
+        by simp
+    qed
     thus ?case by simp
   next
     case (NewC s0 C s1 a s2 jmps T Env)
-    {
-      fix j
-      assume jmp: "abrupt s2 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof - 
-        note \<open>prg Env = G\<close>
-        moreover note hyp_init = \<open>PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>\<close>
-        moreover from wf NewC.prems 
-        have "Env\<turnstile>(Init C)\<Colon>\<surd>"
-          by (elim wt_elim_cases) (drule is_acc_classD,simp)
-        moreover 
-        have "abrupt s1 = Some (Jump j)"
-        proof -
-          from \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> and jmp show ?thesis
-            by (rule halloc_no_jump')
-        qed
-        ultimately show "j \<in> jmps" 
-          by - (rule hyp_init [THEN conjunct1,rule_format (no_asm)],auto)
+    have "j\<in>jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
+    proof - 
+      note \<open>prg Env = G\<close>
+      moreover note hyp_init = \<open>PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>\<close>
+      moreover from wf NewC.prems 
+      have "Env\<turnstile>(Init C)\<Colon>\<surd>"
+        by (elim wt_elim_cases) (drule is_acc_classD,simp)
+      moreover 
+      have "abrupt s1 = Some (Jump j)"
+      proof -
+        from \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> and jmp show ?thesis
+          by (rule halloc_no_jump')
       qed
-    }
+      ultimately show "j \<in> jmps" 
+        by - (rule hyp_init [THEN conjunct1,rule_format (no_asm)],auto)
+    qed
     thus ?case by simp
   next
     case (NewA s0 elT s1 e i s2 a s3 jmps T Env)
-    {
-      fix j
-      assume jmp: "abrupt s3 = Some (Jump j)"
-      have "j\<in>jmps"
+    have "j\<in>jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
+    proof -
+      note G = \<open>prg Env = G\<close>
+      from NewA.prems 
+      obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
+        wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
+        by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
+      note \<open>PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>\<close>
+      with wt_init G 
+      have "?Jmp jmps s1" 
+        by (simp add: init_comp_ty_def)
+      moreover
+      note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 i)\<close>
+      have "abrupt s2 = Some (Jump j)"
       proof -
-        note G = \<open>prg Env = G\<close>
-        from NewA.prems 
-        obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
-               wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
-          by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
-        note \<open>PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>\<close>
-        with wt_init G 
-        have "?Jmp jmps s1" 
-          by (simp add: init_comp_ty_def)
-        moreover
-        note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 i)\<close>
-        have "abrupt s2 = Some (Jump j)"
-        proof -
-          note \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3\<close>
-          moreover note jmp
-          ultimately 
-          have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
-            by (rule halloc_no_jump')
-          thus ?thesis by (cases s2) auto
-        qed
-        ultimately show "j\<in>jmps" using wt_size G 
-          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)
+        note \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3\<close>
+        moreover note jmp
+        ultimately 
+        have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
+          by (rule halloc_no_jump')
+        thus ?thesis by (cases s2) auto
       qed
-    }
+      ultimately show "j\<in>jmps" using wt_size G 
+        by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)
+    qed
     thus ?case by simp
   next
     case (Cast s0 e v s1 s2 cT jmps T Env)
-    {
-      fix j
-      assume jmp: "abrupt s2 = Some (Jump j)"
-      have "j\<in>jmps"
+    have "j\<in>jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
+    proof -
+      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
+      note \<open>prg Env = G\<close>
+      moreover from Cast.prems
+      obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
+      moreover 
+      have "abrupt s1 = Some (Jump j)"
       proof -
-        note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
-        note \<open>prg Env = G\<close>
-        moreover from Cast.prems
-        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
-        moreover 
-        have "abrupt s1 = Some (Jump j)"
-        proof -
-          note \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>
-          moreover note jmp
-          ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
-        qed
-        ultimately show ?thesis 
-          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
+        note \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>
+        moreover note jmp
+        ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
       qed
-    }
+      ultimately show ?thesis 
+        by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
+    qed
     thus ?case by simp
   next
     case (Inst s0 e v s1 b eT jmps T Env)
-    {
-      fix j
-      assume jmp: "abrupt s1 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
-        note \<open>prg Env = G\<close>
-        moreover from Inst.prems
-        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
-        moreover note jmp
-        ultimately show "j\<in>jmps" 
-          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
-      qed
-    }
+    have "j\<in>jmps" if jmp: "abrupt s1 = Some (Jump j)" for j
+    proof -
+      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
+      note \<open>prg Env = G\<close>
+      moreover from Inst.prems
+      obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
+      moreover note jmp
+      ultimately show "j\<in>jmps" 
+        by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
+    qed
     thus ?case by simp
   next
     case Lit thus ?case by simp
   next
     case (UnOp s0 e v s1 unop jmps T Env)
-    {
-      fix j
-      assume jmp: "abrupt s1 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
-        note \<open>prg Env = G\<close>
-        moreover from UnOp.prems
-        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
-        moreover note jmp
-        ultimately show  "j\<in>jmps" 
-          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all) 
-      qed
-    }
+    have "j\<in>jmps" if jmp: "abrupt s1 = Some (Jump j)" for j
+    proof -
+      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
+      note \<open>prg Env = G\<close>
+      moreover from UnOp.prems obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
+      moreover note jmp
+      ultimately show "j\<in>jmps" 
+        by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
+    qed
     thus ?case by simp
   next
     case (BinOp s0 e1 v1 s1 binop e2 v2 s2 jmps T Env)
-    {
-      fix j
-      assume jmp: "abrupt s2 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        note G = \<open>prg Env = G\<close>
-        from BinOp.prems
-        obtain e1T e2T where 
-          wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
-          wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
-          by (elim wt_elim_cases)
-        note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)\<close>
-        with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
-        note hyp_e2 =
-          \<open>PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
+    have "j\<in>jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
+    proof -
+      note G = \<open>prg Env = G\<close>
+      from BinOp.prems
+      obtain e1T e2T where 
+        wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
+        wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
+        by (elim wt_elim_cases)
+      note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)\<close>
+      with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
+      note hyp_e2 =
+        \<open>PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
                      s1 s2 (In1 v2)\<close>
-        show "j\<in>jmps"
-        proof (cases "need_second_arg binop v1")
-          case True with jmp_s1 wt_e2 jmp G
-          show ?thesis 
-            by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
-        next
-          case False with jmp_s1 jmp G
-          show ?thesis 
-            by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],auto)
-        qed
+      show "j\<in>jmps"
+      proof (cases "need_second_arg binop v1")
+        case True with jmp_s1 wt_e2 jmp G
+        show ?thesis 
+          by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
+      next
+        case False with jmp_s1 jmp G
+        show ?thesis 
+          by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],auto)
       qed
-    }
+    qed
     thus ?case by simp
   next
     case Super thus ?case by simp
   next
     case (Acc s0 va v f s1 jmps T Env)
-    {
-      fix j
-      assume jmp: "abrupt s1 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        note hyp_va = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))\<close>
-        note \<open>prg Env = G\<close>
-        moreover from Acc.prems
-        obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
-        moreover note jmp
-        ultimately show "j\<in>jmps" 
-          by - (rule hyp_va [THEN conjunct1,rule_format (no_asm)], simp_all)
-      qed
-    }
+    have "j\<in>jmps" if jmp: "abrupt s1 = Some (Jump j)" for j
+    proof -
+      note hyp_va = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))\<close>
+      note \<open>prg Env = G\<close>
+      moreover from Acc.prems
+      obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
+      moreover note jmp
+      ultimately show "j\<in>jmps" 
+        by - (rule hyp_va [THEN conjunct1,rule_format (no_asm)], simp_all)
+    qed
     thus ?case by simp
   next
     case (Ass s0 va w f s1 e v s2 jmps T Env)
@@ -807,34 +737,30 @@
       by (elim wt_elim_cases)
     note hyp_v = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))\<close>
     note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 v)\<close>
-    {
-      fix j
-      assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        have "abrupt s2 = Some (Jump j)"
-        proof (cases "normal s2")
-          case True
-          from \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> and True have nrm_s1: "normal s1" 
-            by (rule eval_no_abrupt_lemma [rule_format]) 
-          with nrm_s1 wt_va G True
-          have "abrupt (f v s2) \<noteq> Some (Jump j)"
-            using hyp_v [THEN conjunct2,rule_format (no_asm)]
-            by simp
-          from this jmp
-          show ?thesis
-            by (rule assign_abrupt_propagation)
-        next
-          case False with jmp 
-          show ?thesis by (cases s2) (simp add: assign_def Let_def)
-        qed
-        moreover from wt_va G
-        have "?Jmp jmps s1"
-          by - (rule hyp_v [THEN conjunct1],simp_all)
-        ultimately show ?thesis using G 
-          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)
+    have "j\<in>jmps" if jmp: "abrupt (assign f v s2) = Some (Jump j)" for j
+    proof -
+      have "abrupt s2 = Some (Jump j)"
+      proof (cases "normal s2")
+        case True
+        from \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> and True have nrm_s1: "normal s1" 
+          by (rule eval_no_abrupt_lemma [rule_format]) 
+        with nrm_s1 wt_va G True
+        have "abrupt (f v s2) \<noteq> Some (Jump j)"
+          using hyp_v [THEN conjunct2,rule_format (no_asm)]
+          by simp
+        from this jmp
+        show ?thesis
+          by (rule assign_abrupt_propagation)
+      next
+        case False with jmp 
+        show ?thesis by (cases s2) (simp add: assign_def Let_def)
       qed
-    }
+      moreover from wt_va G
+      have "?Jmp jmps s1"
+        by - (rule hyp_v [THEN conjunct1],simp_all)
+      ultimately show ?thesis using G 
+        by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)
+    qed
     thus ?case by simp
   next
     case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)
@@ -847,28 +773,24 @@
        and  wt_e1: "Env\<turnstile>e1\<Colon>-e1T"
        and  wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
       by (elim wt_elim_cases)
-    {
-      fix j
-      assume jmp: "abrupt s2 = Some (Jump j)"
-      have "j\<in>jmps" 
-      proof -
-        from wt_e0 G 
-        have jmp_s1: "?Jmp jmps s1"
-          by - (rule hyp_e0 [THEN conjunct1],simp_all)
+    have "j\<in>jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
+    proof -
+      from wt_e0 G 
+      have jmp_s1: "?Jmp jmps s1"
+        by - (rule hyp_e0 [THEN conjunct1],simp_all)
+      show ?thesis
+      proof (cases "the_Bool b")
+        case True
+        with jmp_s1 wt_e1 G jmp
         show ?thesis
-        proof (cases "the_Bool b")
-          case True
-          with jmp_s1 wt_e1 G jmp
-          show ?thesis
-            by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
-        next
-          case False
-          with jmp_s1 wt_e2 G jmp
-          show ?thesis
-            by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
-        qed
+          by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
+      next
+        case False
+        with jmp_s1 wt_e2 G jmp
+        show ?thesis
+          by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
       qed
-    }
+    qed
     thus ?case by simp
   next
     case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
@@ -878,40 +800,35 @@
     obtain eT argsT 
       where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
       by (elim wt_elim_cases)
-    {
-      fix j
-      assume jmp: "abrupt ((set_lvars (locals (store s2))) s4) 
-                     = Some (Jump j)"
-      have "j\<in>jmps"
+    have "j\<in>jmps" if jmp: "abrupt ((set_lvars (locals (store s2))) s4) = Some (Jump j)" for j
+    proof -
+      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
+      from wt_e G 
+      have jmp_s1: "?Jmp jmps s1"
+        by - (rule hyp_e [THEN conjunct1],simp_all)
+      note hyp_args = \<open>PROP ?Hyp (In3 args) s1 s2 (In3 vs)\<close>
+      have "abrupt s2 = Some (Jump j)"
       proof -
-        note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
-        from wt_e G 
-        have jmp_s1: "?Jmp jmps s1"
-          by - (rule hyp_e [THEN conjunct1],simp_all)
-        note hyp_args = \<open>PROP ?Hyp (In3 args) s1 s2 (In3 vs)\<close>
-        have "abrupt s2 = Some (Jump j)"
-        proof -
-          note \<open>G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4\<close>
-          moreover
-          from jmp have "abrupt s4 = Some (Jump j)"
-            by (cases s4) simp
-          ultimately have "abrupt s3' = Some (Jump j)"
-            by - (rule ccontr,drule (1) Methd_no_jump,simp)
-          moreover note \<open>s3' = check_method_access G accC statT mode 
+        note \<open>G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4\<close>
+        moreover
+        from jmp have "abrupt s4 = Some (Jump j)"
+          by (cases s4) simp
+        ultimately have "abrupt s3' = Some (Jump j)"
+          by - (rule ccontr,drule (1) Methd_no_jump,simp)
+        moreover note \<open>s3' = check_method_access G accC statT mode 
                               \<lparr>name = mn, parTs = pTs\<rparr> a s3\<close>
-          ultimately have "abrupt s3 = Some (Jump j)"
-            by (cases s3) 
-               (simp add: check_method_access_def abrupt_if_def Let_def)
-          moreover 
-          note \<open>s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2\<close>
-          ultimately show ?thesis
-            by (cases s2) (auto simp add: init_lvars_def2)
-        qed
-        with jmp_s1 wt_args G
-        show ?thesis
-          by - (rule hyp_args [THEN conjunct1,rule_format (no_asm)], simp_all)
+        ultimately have "abrupt s3 = Some (Jump j)"
+          by (cases s3) 
+            (simp add: check_method_access_def abrupt_if_def Let_def)
+        moreover 
+        note \<open>s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2\<close>
+        ultimately show ?thesis
+          by (cases s2) (auto simp add: init_lvars_def2)
       qed
-    }
+      with jmp_s1 wt_args G
+      show ?thesis
+        by - (rule hyp_args [THEN conjunct1,rule_format (no_asm)], simp_all)
+    qed
     thus ?case by simp
   next
     case (Methd s0 D sig v s1 jmps T Env)
@@ -952,45 +869,36 @@
         by simp
     qed
     note fvar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>
-    {
-      fix j
-      assume jmp: "abrupt s3 = Some (Jump j)"
-      have "j\<in>jmps"
+    have "j\<in>jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
+    proof -
+      note hyp_init = \<open>PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>\<close>
+      have "?Jmp jmps s1"
+        by (rule hyp_init [THEN conjunct1]) (use G wt_init in auto)
+      moreover
+      note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 a)\<close>
+      have "abrupt s2 = Some (Jump j)"
       proof -
-        note hyp_init = \<open>PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>\<close>
-        from G wt_init 
-        have "?Jmp jmps s1"
-          by - (rule hyp_init [THEN conjunct1],auto)
-        moreover
-        note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 a)\<close>
-        have "abrupt s2 = Some (Jump j)"
-        proof -
-          note \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
-          with jmp have "abrupt s2' = Some (Jump j)"
-            by (cases s2') 
-               (simp add: check_field_access_def abrupt_if_def Let_def)
-         with fvar show "abrupt s2 =  Some (Jump j)"
-            by (cases s2) (simp add: fvar_def2 abrupt_if_def)
-        qed
-        ultimately show ?thesis
-          using G wt_e
-          by - (rule hyp_e [THEN conjunct1, rule_format (no_asm)],simp_all)
+        note \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
+        with jmp have "abrupt s2' = Some (Jump j)"
+          by (cases s2') 
+            (simp add: check_field_access_def abrupt_if_def Let_def)
+        with fvar show "abrupt s2 =  Some (Jump j)"
+          by (cases s2) (simp add: fvar_def2 abrupt_if_def)
       qed
-    }
+      ultimately show ?thesis
+        using G wt_e
+        by - (rule hyp_e [THEN conjunct1, rule_format (no_asm)],simp_all)
+    qed
     moreover
     from fvar obtain upd w
       where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and
               v: "v=(w,upd)"
       by (cases "fvar statDeclC stat fn a s2")
         (simp, use surjective_pairing in blast)
-    {
-      fix j val fix s::state
-      assume "normal s3"
-      assume no_jmp: "abrupt s \<noteq> Some (Jump j)"
-      with upd
-      have "abrupt (upd val s) \<noteq> Some (Jump j)"
-        by (rule fvar_upd_no_jump)
-    }
+    have "abrupt (upd val s) \<noteq> Some (Jump j)"
+      if "abrupt s \<noteq> Some (Jump j)"
+      for j val and s::state
+      using upd that by (rule fvar_upd_no_jump)
     ultimately show ?case using v by simp
   next
     case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
@@ -1000,68 +908,56 @@
       wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
       by  (elim wt_elim_cases) simp
     note avar = \<open>(v, s2') = avar G i a s2\<close>
-    {
-      fix j
-      assume jmp: "abrupt s2' = Some (Jump j)"
-      have "j\<in>jmps"
+    have "j\<in>jmps" if jmp: "abrupt s2' = Some (Jump j)" for j
+    proof -
+      note hyp_e1 = \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)\<close>
+      from G wt_e1
+      have "?Jmp jmps s1"
+        by - (rule hyp_e1 [THEN conjunct1], auto)
+      moreover
+      note hyp_e2 = \<open>PROP ?Hyp (In1l e2) s1 s2 (In1 i)\<close>
+      have "abrupt s2 = Some (Jump j)"
       proof -
-        note hyp_e1 = \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)\<close>
-        from G wt_e1
-        have "?Jmp jmps s1"
-          by - (rule hyp_e1 [THEN conjunct1], auto)
-        moreover
-        note hyp_e2 = \<open>PROP ?Hyp (In1l e2) s1 s2 (In1 i)\<close>
-        have "abrupt s2 = Some (Jump j)"
-        proof -
-          from avar have "s2' = snd (avar G i a s2)"
-            by (cases "avar G i a s2") simp
-          with jmp show ?thesis by - (rule avar_state_no_jump,simp) 
-        qed  
-        ultimately show ?thesis
-          using wt_e2 G
-          by - (rule hyp_e2 [THEN conjunct1, rule_format (no_asm)],simp_all)
-      qed
-    }
+        from avar have "s2' = snd (avar G i a s2)"
+          by (cases "avar G i a s2") simp
+        with jmp show ?thesis by - (rule avar_state_no_jump,simp) 
+      qed  
+      ultimately show ?thesis
+        using wt_e2 G
+        by - (rule hyp_e2 [THEN conjunct1, rule_format (no_asm)],simp_all)
+    qed
     moreover
     from avar obtain upd w
       where upd: "upd = snd (fst (avar G i a s2))" and
               v: "v=(w,upd)"
       by (cases "avar G i a s2")
         (simp, use surjective_pairing in blast)
-    {
-      fix j val fix s::state
-      assume "normal s2'"
-      assume no_jmp: "abrupt s \<noteq> Some (Jump j)"
-      with upd
-      have "abrupt (upd val s) \<noteq> Some (Jump j)"
-        by (rule avar_upd_no_jump)
-    }
+    have "abrupt (upd val s) \<noteq> Some (Jump j)" if "abrupt s \<noteq> Some (Jump j)"
+      for j val and s::state
+      using upd that by (rule avar_upd_no_jump)
     ultimately show ?case using v by simp
   next
-    case Nil thus ?case by simp
+    case Nil
+    thus ?case by simp
   next
     case (Cons s0 e v s1 es vs s2 jmps T Env)
     note G = \<open>prg Env = G\<close>
     from Cons.prems obtain eT esT
       where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_e2: "Env\<turnstile>es\<Colon>\<doteq>esT"
       by  (elim wt_elim_cases) simp
-    {
-      fix j
-      assume jmp: "abrupt s2 = Some (Jump j)"
-      have "j\<in>jmps"
-      proof -
-        note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
-        from G wt_e
-        have "?Jmp jmps s1"
-          by - (rule hyp_e [THEN conjunct1],simp_all)
-        moreover
-        note hyp_es = \<open>PROP ?Hyp (In3 es) s1 s2 (In3 vs)\<close>
-        ultimately show ?thesis
-          using wt_e2 G jmp
-          by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
-                (assumption|simp (no_asm_simp))+)
-      qed
-    }
+    have "j\<in>jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
+    proof -
+      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
+      from G wt_e
+      have "?Jmp jmps s1"
+        by - (rule hyp_e [THEN conjunct1],simp_all)
+      moreover
+      note hyp_es = \<open>PROP ?Hyp (In3 es) s1 s2 (In3 vs)\<close>
+      ultimately show ?thesis
+        using wt_e2 G jmp
+        by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
+            (assumption|simp (no_asm_simp))+)
+    qed
     thus ?case by simp
   qed
   note generalized = this
@@ -2243,379 +2139,376 @@
 proof -
   \<comment> \<open>To properly perform induction on the evaluation relation we have to
         generalize the lemma to terms not only expressions.\<close>
-  { fix t val
-   assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"  
-   assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
-   assume expr:  "\<exists> expr. t=In1l expr"
-   have "assigns_if (the_Bool (the_In1 val)) (the_In1l t) 
-                \<subseteq> dom (locals (store s1))"
-   using eval' normal bool' expr
-   proof (induct)
-     case Abrupt thus ?case by simp
-   next
-     case (NewC s0 C s1 a s2)
-     from \<open>Env\<turnstile>NewC C\<Colon>-PrimT Boolean\<close>
-     have False 
-       by cases simp
-     thus ?case ..
-   next
-     case (NewA s0 T s1 e i s2 a s3)
-     from \<open>Env\<turnstile>New T[e]\<Colon>-PrimT Boolean\<close>
-     have False 
-       by cases simp
-     thus ?case ..
-   next
-     case (Cast s0 e b s1 s2 T)
-     note s2 = \<open>s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1\<close>
-     have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))" 
-     proof -
-       from s2 and \<open>normal s2\<close>
-       have "normal s1"
-         by (cases s1) simp
-       moreover
-       from \<open>Env\<turnstile>Cast T e\<Colon>-PrimT Boolean\<close>
-       have "Env\<turnstile>e\<Colon>- PrimT Boolean" 
-         by cases (auto dest: cast_Boolean2)
-       ultimately show ?thesis 
-         by (rule Cast.hyps [elim_format]) auto
-     qed
-     also from s2 
-     have "\<dots> \<subseteq> dom (locals (store s2))"
-       by simp
-     finally show ?case by simp
-   next
-     case (Inst s0 e v s1 b T)
-     from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close> and \<open>normal s1\<close>
-     have "assignsE e \<subseteq> dom (locals (store s1))"
-       by (rule assignsE_good_approx)
-     thus ?case
-       by simp
-   next
-     case (Lit s v)
-     from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>
-     have "typeof empty_dt v = Some (PrimT Boolean)"
-       by cases simp
-     then obtain b where "v=Bool b"
-       by (cases v) (simp_all add: empty_dt_def)
-     thus ?case
-       by simp
-   next
-     case (UnOp s0 e v s1 unop)
-     note bool = \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>
-     hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" 
-       by cases (cases unop,simp_all)
-     show ?case
-     proof (cases "constVal (UnOp unop e)")
-       case None
-       note \<open>normal s1\<close>
-       moreover note bool_e
-       ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
-         by (rule UnOp.hyps [elim_format]) auto
-       moreover
-       from bool have "unop = UNot"
-         by cases (cases unop, simp_all)
-       moreover note None
-       ultimately 
-       have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) 
+  have generalized: "assigns_if (the_Bool (the_In1 val)) (the_In1l t) \<subseteq> dom (locals (store s1))"
+    if eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"  
+      and bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
+      and expr:  "\<exists> expr. t=In1l expr"
+    for t val
+    using eval' normal bool' expr
+  proof (induct)
+    case Abrupt thus ?case by simp
+  next
+    case (NewC s0 C s1 a s2)
+    from \<open>Env\<turnstile>NewC C\<Colon>-PrimT Boolean\<close>
+    have False 
+      by cases simp
+    thus ?case ..
+  next
+    case (NewA s0 T s1 e i s2 a s3)
+    from \<open>Env\<turnstile>New T[e]\<Colon>-PrimT Boolean\<close>
+    have False 
+      by cases simp
+    thus ?case ..
+  next
+    case (Cast s0 e b s1 s2 T)
+    note s2 = \<open>s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1\<close>
+    have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))" 
+    proof -
+      from s2 and \<open>normal s2\<close>
+      have "normal s1"
+        by (cases s1) simp
+      moreover
+      from \<open>Env\<turnstile>Cast T e\<Colon>-PrimT Boolean\<close>
+      have "Env\<turnstile>e\<Colon>- PrimT Boolean" 
+        by cases (auto dest: cast_Boolean2)
+      ultimately show ?thesis 
+        by (rule Cast.hyps [elim_format]) auto
+    qed
+    also from s2 
+    have "\<dots> \<subseteq> dom (locals (store s2))"
+      by simp
+    finally show ?case by simp
+  next
+    case (Inst s0 e v s1 b T)
+    from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close> and \<open>normal s1\<close>
+    have "assignsE e \<subseteq> dom (locals (store s1))"
+      by (rule assignsE_good_approx)
+    thus ?case
+      by simp
+  next
+    case (Lit s v)
+    from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>
+    have "typeof empty_dt v = Some (PrimT Boolean)"
+      by cases simp
+    then obtain b where "v=Bool b"
+      by (cases v) (simp_all add: empty_dt_def)
+    thus ?case
+      by simp
+  next
+    case (UnOp s0 e v s1 unop)
+    note bool = \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>
+    hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" 
+      by cases (cases unop,simp_all)
+    show ?case
+    proof (cases "constVal (UnOp unop e)")
+      case None
+      note \<open>normal s1\<close>
+      moreover note bool_e
+      ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
+        by (rule UnOp.hyps [elim_format]) auto
+      moreover
+      from bool have "unop = UNot"
+        by cases (cases unop, simp_all)
+      moreover note None
+      ultimately 
+      have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) 
               \<subseteq> dom (locals (store s1))"
-         by simp
-       thus ?thesis by simp
-     next
-       case (Some c)
-       moreover
-       from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>
-       have "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1" 
-         by (rule eval.UnOp)
-       with Some
-       have "eval_unop unop v=c"
-         by (rule constVal_eval_elim) simp
-       moreover
-       from Some bool
-       obtain b where "c=Bool b"
-         by (rule constVal_Boolean [elim_format])
-            (cases c, simp_all add: empty_dt_def)
-       ultimately
-       have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) = {}"
-         by simp
-       thus ?thesis by simp
-     qed
-   next
-     case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
-     note bool = \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>
-     show ?case
-     proof (cases "constVal (BinOp binop e1 e2)") 
-       case (Some c)
-       moreover
-       from BinOp.hyps
-       have
-         "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
-         by - (rule eval.BinOp) 
-       with Some
-       have "eval_binop binop v1 v2=c"
-         by (rule constVal_eval_elim) simp
-       moreover
-       from Some bool
-       obtain b where "c = Bool b"
-         by (rule constVal_Boolean [elim_format])
-            (cases c, simp_all add: empty_dt_def)
-       ultimately
-       have "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2) 
+        by simp
+      thus ?thesis by simp
+    next
+      case (Some c)
+      moreover
+      from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>
+      have "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1" 
+        by (rule eval.UnOp)
+      with Some
+      have "eval_unop unop v=c"
+        by (rule constVal_eval_elim) simp
+      moreover
+      from Some bool
+      obtain b where "c=Bool b"
+        by (rule constVal_Boolean [elim_format])
+          (cases c, simp_all add: empty_dt_def)
+      ultimately
+      have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) = {}"
+        by simp
+      thus ?thesis by simp
+    qed
+  next
+    case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
+    note bool = \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>
+    show ?case
+    proof (cases "constVal (BinOp binop e1 e2)") 
+      case (Some c)
+      moreover
+      from BinOp.hyps
+      have
+        "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
+        by - (rule eval.BinOp) 
+      with Some
+      have "eval_binop binop v1 v2=c"
+        by (rule constVal_eval_elim) simp
+      moreover
+      from Some bool
+      obtain b where "c = Bool b"
+        by (rule constVal_Boolean [elim_format])
+          (cases c, simp_all add: empty_dt_def)
+      ultimately
+      have "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2) 
              = {}"
-         by simp 
-       thus ?thesis by simp
-     next
-       case None
-       show ?thesis
-       proof (cases "binop=CondAnd \<or> binop=CondOr")
-         case True
-         from bool obtain bool_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
-                          bool_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
-           using True by cases auto
-         have "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s1))"
-         proof -
-           from BinOp have "normal s1"
-             by - (erule eval_no_abrupt_lemma [rule_format])
-           from this bool_e1
-           show ?thesis
-             by (rule BinOp.hyps [elim_format]) auto
-         qed
-         also
-         from BinOp.hyps
-         have "\<dots> \<subseteq> dom (locals (store s2))"
-           by - (erule dom_locals_eval_mono_elim,simp)
-         finally
-         have e1_s2: "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s2))".
-         from True show ?thesis
-         proof
-           assume condAnd: "binop = CondAnd"
-           show ?thesis
-           proof (cases "the_Bool (eval_binop binop v1 v2)")
-             case True
-             with condAnd 
-             have need_second: "need_second_arg binop v1"
-               by (simp add: need_second_arg_def)
-             from \<open>normal s2\<close>
-             have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
-               by (rule BinOp.hyps [elim_format]) 
-                  (simp add: need_second bool_e2)+
-             with e1_s2
-             have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
+        by simp 
+      thus ?thesis by simp
+    next
+      case None
+      show ?thesis
+      proof (cases "binop=CondAnd \<or> binop=CondOr")
+        case True
+        from bool obtain bool_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
+          bool_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
+          using True by cases auto
+        have "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s1))"
+        proof -
+          from BinOp have "normal s1"
+            by - (erule eval_no_abrupt_lemma [rule_format])
+          from this bool_e1
+          show ?thesis
+            by (rule BinOp.hyps [elim_format]) auto
+        qed
+        also
+        from BinOp.hyps
+        have "\<dots> \<subseteq> dom (locals (store s2))"
+          by - (erule dom_locals_eval_mono_elim,simp)
+        finally
+        have e1_s2: "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s2))".
+        from True show ?thesis
+        proof
+          assume condAnd: "binop = CondAnd"
+          show ?thesis
+          proof (cases "the_Bool (eval_binop binop v1 v2)")
+            case True
+            with condAnd 
+            have need_second: "need_second_arg binop v1"
+              by (simp add: need_second_arg_def)
+            from \<open>normal s2\<close>
+            have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+              by (rule BinOp.hyps [elim_format]) 
+                (simp add: need_second bool_e2)+
+            with e1_s2
+            have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
                     \<subseteq> dom (locals (store s2))"
-               by (rule Un_least)
-             with True condAnd None show ?thesis
-               by simp
-           next
-             case False
-             note binop_False = this
-             show ?thesis
-             proof (cases "need_second_arg binop v1")
-               case True
-               with binop_False condAnd
-               obtain "the_Bool v1=True" and "the_Bool v2 = False"
-                 by (simp add: need_second_arg_def)
-               moreover
-               from \<open>normal s2\<close>
-               have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
-                 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
-               with e1_s2
-               have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
+              by (rule Un_least)
+            with True condAnd None show ?thesis
+              by simp
+          next
+            case False
+            note binop_False = this
+            show ?thesis
+            proof (cases "need_second_arg binop v1")
+              case True
+              with binop_False condAnd
+              obtain "the_Bool v1=True" and "the_Bool v2 = False"
+                by (simp add: need_second_arg_def)
+              moreover
+              from \<open>normal s2\<close>
+              have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+                by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
+              with e1_s2
+              have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
                       \<subseteq> dom (locals (store s2))"
-                 by (rule Un_least)
-               moreover note binop_False condAnd None
-               ultimately show ?thesis
-                 by auto
-             next
-               case False
-               with binop_False condAnd
-               have "the_Bool v1=False"
-                 by (simp add: need_second_arg_def)
-               with e1_s2 
-               show ?thesis
-                 using binop_False condAnd None by auto
-             qed
-           qed
-         next
-           assume condOr: "binop = CondOr"
-           show ?thesis
-           proof (cases "the_Bool (eval_binop binop v1 v2)")
-             case False
-             with condOr 
-             have need_second: "need_second_arg binop v1"
-               by (simp add: need_second_arg_def)
-             from \<open>normal s2\<close>
-             have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
-               by (rule BinOp.hyps [elim_format]) 
-                  (simp add: need_second bool_e2)+
-             with e1_s2
-             have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
+                by (rule Un_least)
+              moreover note binop_False condAnd None
+              ultimately show ?thesis
+                by auto
+            next
+              case False
+              with binop_False condAnd
+              have "the_Bool v1=False"
+                by (simp add: need_second_arg_def)
+              with e1_s2 
+              show ?thesis
+                using binop_False condAnd None by auto
+            qed
+          qed
+        next
+          assume condOr: "binop = CondOr"
+          show ?thesis
+          proof (cases "the_Bool (eval_binop binop v1 v2)")
+            case False
+            with condOr 
+            have need_second: "need_second_arg binop v1"
+              by (simp add: need_second_arg_def)
+            from \<open>normal s2\<close>
+            have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+              by (rule BinOp.hyps [elim_format]) 
+                (simp add: need_second bool_e2)+
+            with e1_s2
+            have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
                     \<subseteq> dom (locals (store s2))"
-               by (rule Un_least)
-             with False condOr None show ?thesis
-               by simp
-           next
-             case True
-             note binop_True = this
-             show ?thesis
-             proof (cases "need_second_arg binop v1")
-               case True
-               with binop_True condOr
-               obtain "the_Bool v1=False" and "the_Bool v2 = True"
-                 by (simp add: need_second_arg_def)
-               moreover
-               from \<open>normal s2\<close>
-               have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
-                 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
-               with e1_s2
-               have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
+              by (rule Un_least)
+            with False condOr None show ?thesis
+              by simp
+          next
+            case True
+            note binop_True = this
+            show ?thesis
+            proof (cases "need_second_arg binop v1")
+              case True
+              with binop_True condOr
+              obtain "the_Bool v1=False" and "the_Bool v2 = True"
+                by (simp add: need_second_arg_def)
+              moreover
+              from \<open>normal s2\<close>
+              have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+                by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
+              with e1_s2
+              have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
                       \<subseteq> dom (locals (store s2))"
-                 by (rule Un_least)
-               moreover note binop_True condOr None
-               ultimately show ?thesis
-                 by auto
-             next
-               case False
-               with binop_True condOr
-               have "the_Bool v1=True"
-                 by (simp add: need_second_arg_def)
-               with e1_s2 
-               show ?thesis
-                 using binop_True condOr None by auto
-             qed
-           qed
-         qed  
-       next
-         case False
-         note \<open>\<not> (binop = CondAnd \<or> binop = CondOr)\<close>
-         from BinOp.hyps
-         have
-           "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
-           by - (rule eval.BinOp)  
-         moreover note \<open>normal s2\<close>
-         ultimately
-         have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
-           by (rule assignsE_good_approx)
-         with False None
-         show ?thesis 
-           by simp
-       qed
-     qed
-   next     
-     case Super 
-     note \<open>Env\<turnstile>Super\<Colon>-PrimT Boolean\<close>
-     hence False 
-       by cases simp
-     thus ?case ..
-   next
-     case (Acc s0 va v f s1)
-     from \<open>prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1\<close> and \<open>normal s1\<close>
-     have "assignsV va \<subseteq> dom (locals (store s1))"
-       by (rule assignsV_good_approx)
-     thus ?case by simp
-   next
-     case (Ass s0 va w f s1 e v s2)
-     hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"
-       by - (rule eval.Ass)
-     moreover note \<open>normal (assign f v s2)\<close>
-     ultimately 
-     have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"
-       by (rule assignsE_good_approx)
-     thus ?case by simp
-   next
-     case (Cond s0 e0 b s1 e1 e2 v s2)
-     from \<open>Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean\<close>
-     obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
-            wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
-       by cases (auto dest: widen_Boolean2)
-     note eval_e0 = \<open>prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1\<close>
-     have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
-     proof -
-       note eval_e0 
-       moreover
-       from Cond.hyps and \<open>normal s2\<close> have "normal s1"
-         by - (erule eval_no_abrupt_lemma [rule_format],simp)
-       ultimately
-       have "assignsE e0 \<subseteq> dom (locals (store s1))"
-         by (rule assignsE_good_approx)
-       also
-       from Cond
-       have "\<dots> \<subseteq> dom (locals (store s2))"
-         by - (erule dom_locals_eval_mono [elim_format],simp)
-       finally show ?thesis .
-     qed
-     show ?case
-     proof (cases "constVal e0")
-       case None
-       have "assigns_if (the_Bool v) e1 \<inter>  assigns_if (the_Bool v) e2 
+                by (rule Un_least)
+              moreover note binop_True condOr None
+              ultimately show ?thesis
+                by auto
+            next
+              case False
+              with binop_True condOr
+              have "the_Bool v1=True"
+                by (simp add: need_second_arg_def)
+              with e1_s2 
+              show ?thesis
+                using binop_True condOr None by auto
+            qed
+          qed
+        qed  
+      next
+        case False
+        note \<open>\<not> (binop = CondAnd \<or> binop = CondOr)\<close>
+        from BinOp.hyps
+        have
+          "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
+          by - (rule eval.BinOp)  
+        moreover note \<open>normal s2\<close>
+        ultimately
+        have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
+          by (rule assignsE_good_approx)
+        with False None
+        show ?thesis 
+          by simp
+      qed
+    qed
+  next     
+    case Super 
+    note \<open>Env\<turnstile>Super\<Colon>-PrimT Boolean\<close>
+    hence False 
+      by cases simp
+    thus ?case ..
+  next
+    case (Acc s0 va v f s1)
+    from \<open>prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1\<close> and \<open>normal s1\<close>
+    have "assignsV va \<subseteq> dom (locals (store s1))"
+      by (rule assignsV_good_approx)
+    thus ?case by simp
+  next
+    case (Ass s0 va w f s1 e v s2)
+    hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"
+      by - (rule eval.Ass)
+    moreover note \<open>normal (assign f v s2)\<close>
+    ultimately 
+    have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"
+      by (rule assignsE_good_approx)
+    thus ?case by simp
+  next
+    case (Cond s0 e0 b s1 e1 e2 v s2)
+    from \<open>Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean\<close>
+    obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
+      wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
+      by cases (auto dest: widen_Boolean2)
+    note eval_e0 = \<open>prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1\<close>
+    have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
+    proof -
+      note eval_e0 
+      moreover
+      from Cond.hyps and \<open>normal s2\<close> have "normal s1"
+        by - (erule eval_no_abrupt_lemma [rule_format],simp)
+      ultimately
+      have "assignsE e0 \<subseteq> dom (locals (store s1))"
+        by (rule assignsE_good_approx)
+      also
+      from Cond
+      have "\<dots> \<subseteq> dom (locals (store s2))"
+        by - (erule dom_locals_eval_mono [elim_format],simp)
+      finally show ?thesis .
+    qed
+    show ?case
+    proof (cases "constVal e0")
+      case None
+      have "assigns_if (the_Bool v) e1 \<inter>  assigns_if (the_Bool v) e2 
               \<subseteq> dom (locals (store s2))"
-       proof (cases "the_Bool b")
-         case True
-         from \<open>normal s2\<close>
-         have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
-           by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)
-         thus ?thesis
-           by blast
-       next
-         case False
-         from \<open>normal s2\<close>
-         have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
-           by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)
-         thus ?thesis
-           by blast
-       qed
-       with e0_s2
-       have "assignsE e0 \<union> 
+      proof (cases "the_Bool b")
+        case True
+        from \<open>normal s2\<close>
+        have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
+          by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)
+        thus ?thesis
+          by blast
+      next
+        case False
+        from \<open>normal s2\<close>
+        have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
+          by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)
+        thus ?thesis
+          by blast
+      qed
+      with e0_s2
+      have "assignsE e0 \<union> 
              (assigns_if (the_Bool v) e1 \<inter>  assigns_if (the_Bool v) e2)
                \<subseteq> dom (locals (store s2))"
-         by (rule Un_least)
-       with None show ?thesis
-         by simp
-     next
-       case (Some c)
-       from this eval_e0 have eq_b_c: "b=c" 
-         by (rule constVal_eval_elim) 
-       show ?thesis
-       proof (cases "the_Bool c")
-         case True
-         from \<open>normal s2\<close>
-         have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
-           by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)
-         with e0_s2
-         have "assignsE e0 \<union> assigns_if (the_Bool v) e1  \<subseteq> \<dots>"
-           by (rule Un_least)
-         with Some True show ?thesis
-           by simp
-       next
-         case False
-         from \<open>normal s2\<close>
-         have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
-           by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)
-         with e0_s2
-         have "assignsE e0 \<union> assigns_if (the_Bool v) e2  \<subseteq> \<dots>"
-           by (rule Un_least)
-         with Some False show ?thesis
-           by simp
-       qed
-     qed
-   next
-     case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
-     hence
-     "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v\<rightarrow> 
+        by (rule Un_least)
+      with None show ?thesis
+        by simp
+    next
+      case (Some c)
+      from this eval_e0 have eq_b_c: "b=c" 
+        by (rule constVal_eval_elim) 
+      show ?thesis
+      proof (cases "the_Bool c")
+        case True
+        from \<open>normal s2\<close>
+        have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
+          by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)
+        with e0_s2
+        have "assignsE e0 \<union> assigns_if (the_Bool v) e1  \<subseteq> \<dots>"
+          by (rule Un_least)
+        with Some True show ?thesis
+          by simp
+      next
+        case False
+        from \<open>normal s2\<close>
+        have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
+          by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)
+        with e0_s2
+        have "assignsE e0 \<union> assigns_if (the_Bool v) e2  \<subseteq> \<dots>"
+          by (rule Un_least)
+        with Some False show ?thesis
+          by simp
+      qed
+    qed
+  next
+    case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
+    hence
+      "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v\<rightarrow> 
                        (set_lvars (locals (store s2)) s4)"
-       by - (rule eval.Call)
-     hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args)) 
+      by - (rule eval.Call)
+    hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args)) 
               \<subseteq>  dom (locals (store ((set_lvars (locals (store s2))) s4)))"
-       using \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>
-       by (rule assignsE_good_approx)
-     thus ?case by simp
-   next
-     case Methd show ?case by simp
-   next
-     case Body show ?case by simp
-   qed simp+ \<comment> \<open>all the statements and variables\<close>
- }
- note generalized = this
- from eval bool show ?thesis
-   by (rule generalized [elim_format]) simp+
+      using \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>
+      by (rule assignsE_good_approx)
+    thus ?case by simp
+  next
+    case Methd show ?case by simp
+  next
+    case Body show ?case by simp
+  qed simp_all \<comment> \<open>all the statements and variables\<close>
+  from eval bool show ?thesis
+    by (rule generalized [elim_format]) simp+
 qed
 
 lemma assigns_if_good_approx': 
@@ -2731,19 +2624,16 @@
     moreover 
     have "?BreakAssigned (Norm s0) (abupd (absorb j) s1) A"
     proof -
-      {
-        fix l'
-        assume break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))"
-        with j 
-        have "l\<noteq>l'"
+      have "(brk A l' \<subseteq> dom (locals (store (abupd (absorb j) s1))))"
+        if break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))" for l'
+      proof -
+        from j that have "l\<noteq>l'"
           by (cases s1) (auto dest!: absorb_Some_JumpD)
         hence "(rmlab l (brk C)) l'= (brk C) l'"
-          by (simp)
-        with break brk_c A
-        have 
-          "(brk A l' \<subseteq> dom (locals (store (abupd (absorb j) s1))))"
+          by simp
+        with break brk_c A show ?thesis
           by (cases s1) auto
-      }
+      qed
       then show ?thesis
         by simp
     qed
@@ -3399,74 +3289,68 @@
       qed
     qed
     moreover
-    {
-      fix l assume brk_s3: "abrupt s3 = Some (Jump (Break l))"
-      have "brk A l \<subseteq> dom (locals (store s3))"
-      proof (cases "normal s2")
-        case True
-        with brk_s3 s3 
-        have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
+    have "brk A l \<subseteq> dom (locals (store s3))" if brk_s3: "abrupt s3 = Some (Jump (Break l))" for l
+    proof (cases "normal s2")
+      case True
+      with brk_s3 s3 
+      have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
+        by simp
+      have "brk C1 l \<subseteq> dom (locals (store s3))"
+      proof -
+        from True brk_s3 s3 have "x1=Some (Jump (Break l))"
+          by (cases s2) (simp add: abrupt_if_def)
+        with brkAss_C1 s1_s2 s2_s3
+        show ?thesis
           by simp
-        have "brk C1 l \<subseteq> dom (locals (store s3))"
-        proof -
-          from True brk_s3 s3 have "x1=Some (Jump (Break l))"
-            by (cases s2) (simp add: abrupt_if_def)
-          with brkAss_C1 s1_s2 s2_s3
-          show ?thesis
-            by simp
-        qed
-        moreover from True nrmAss_C2 s2_s3
-        have "nrm C2 \<subseteq> dom (locals (store s3))"
-          by - (rule subset_trans, simp_all)
-        ultimately 
-        have "((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) l \<subseteq> \<dots>"
-          by blast
-        with brk_A show ?thesis
-          by simp blast
+      qed
+      moreover from True nrmAss_C2 s2_s3
+      have "nrm C2 \<subseteq> dom (locals (store s3))"
+        by - (rule subset_trans, simp_all)
+      ultimately 
+      have "((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) l \<subseteq> \<dots>"
+        by blast
+      with brk_A show ?thesis
+        by simp blast
+    next
+      case False
+      note not_normal_s2 = this
+      have "s3=s2"
+      proof (cases "normal (x1,s1)")
+        case True with not_normal_s2 s3 show ?thesis
+          by (cases s2) (simp add: abrupt_if_def)
       next
-        case False
-        note not_normal_s2 = this
-        have "s3=s2"
-        proof (cases "normal (x1,s1)")
-          case True with not_normal_s2 s3 show ?thesis
-            by (cases s2) (simp add: abrupt_if_def)
-        next
-          case False with not_normal_s2 s3 brk_s3 show ?thesis
-            by (cases s2) (simp add: abrupt_if_def)
-        qed
-        with brkAss_C2 brk_s3
-        have "brk C2 l \<subseteq> dom (locals (store s3))"
-          by simp
-        with brk_A show ?thesis
-          by simp blast
+        case False with not_normal_s2 s3 brk_s3 show ?thesis
+          by (cases s2) (simp add: abrupt_if_def)
       qed
-    }
+      with brkAss_C2 brk_s3
+      have "brk C2 l \<subseteq> dom (locals (store s3))"
+        by simp
+      with brk_A show ?thesis
+        by simp blast
+    qed
     hence "?BreakAssigned (Norm s0) s3 A"
       by simp
     moreover
-    {
-      assume abr_s3: "abrupt s3 = Some (Jump Ret)"
-      have "Result \<in> dom (locals (store s3))"
-      proof (cases "x1 = Some (Jump Ret)")
-        case True
-        note ret_x1 = this
-        with resAss_s1 have res_s1: "Result \<in> dom (locals s1)"
-          by simp
-        moreover have "dom (locals (store ((Norm s1)::state))) 
+    have "Result \<in> dom (locals (store s3))" if abr_s3: "abrupt s3 = Some (Jump Ret)"
+    proof (cases "x1 = Some (Jump Ret)")
+      case True
+      note ret_x1 = this
+      with resAss_s1 have res_s1: "Result \<in> dom (locals s1)"
+        by simp
+      moreover have "dom (locals (store ((Norm s1)::state))) 
                          \<subseteq> dom (locals (store s2))"
-          by (rule dom_locals_eval_mono_elim) (rule Fin.hyps)
-        ultimately have "Result \<in> dom (locals (store s2))"
-          by - (rule subsetD,auto)
-        with res_s1 s3 show ?thesis
-          by simp
-      next
-        case False
-        with s3 abr_s3 obtain  "abrupt s2 = Some (Jump Ret)" and "s3=s2"
-          by (cases s2) (simp add: abrupt_if_def)
-        with resAss_s2 show ?thesis
-          by simp
-      qed
-    }
+        by (rule dom_locals_eval_mono_elim) (rule Fin.hyps)
+      ultimately have "Result \<in> dom (locals (store s2))"
+        by - (rule subsetD,auto)
+      with res_s1 s3 show ?thesis
+        by simp
+    next
+      case False
+      with s3 abr_s3 obtain  "abrupt s2 = Some (Jump Ret)" and "s3=s2"
+        by (cases s2) (simp add: abrupt_if_def)
+      with resAss_s2 show ?thesis
+        by simp
+    qed
     hence "?ResAssigned (Norm s0) s3"
       by simp
     ultimately show ?case by (intro conjI)
@@ -3547,21 +3431,19 @@
     with A have "?NormalAssigned s2 A"
       by simp
     moreover
-    {
-      fix j have "abrupt s2 \<noteq> Some (Jump j)"
-      proof -
-        have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
-          unfolding G by (rule eval.NewC NewC.hyps)+
-        from NewC.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with NewC.prems have "Env\<turnstile>NewC C\<Colon>-T'" 
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_no_jump) (simp_all add: G wf)
-      qed
-    }
+    have "abrupt s2 \<noteq> Some (Jump j)" for j
+    proof -
+      have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
+        unfolding G by (rule eval.NewC NewC.hyps)+
+      from NewC.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with NewC.prems have "Env\<turnstile>NewC C\<Colon>-T'" 
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_no_jump) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
       by simp_all      
     ultimately show ?case by (intro conjI)
@@ -3612,21 +3494,19 @@
       qed
     qed
     moreover
-    {
-      fix j have "abrupt s3 \<noteq> Some (Jump j)"
-      proof -
-        have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"
-          unfolding G by (rule eval.NewA NewA.hyps)+
-        from NewA.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with NewA.prems have "Env\<turnstile>New elT[e]\<Colon>-T'" 
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_no_jump) (simp_all add: G wf)
-      qed
-    }
+    have "abrupt s3 \<noteq> Some (Jump j)" for j
+    proof -
+      have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"
+        unfolding G by (rule eval.NewA NewA.hyps)+
+      from NewA.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with NewA.prems have "Env\<turnstile>New elT[e]\<Colon>-T'" 
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_no_jump) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"
       by simp_all
     ultimately show ?case by (intro conjI)
@@ -3657,21 +3537,19 @@
         by blast
     qed
     moreover
-    {
-      fix j have "abrupt s2 \<noteq> Some (Jump j)"
-      proof -
-        have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"
-          unfolding G by (rule eval.Cast Cast.hyps)+
-        from Cast.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with Cast.prems have "Env\<turnstile>Cast cT e\<Colon>-T'" 
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_no_jump) (simp_all add: G wf)
-      qed
-    }
+    have "abrupt s2 \<noteq> Some (Jump j)" for j
+    proof -
+      have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"
+        unfolding G by (rule eval.Cast Cast.hyps)+
+      from Cast.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with Cast.prems have "Env\<turnstile>Cast cT e\<Colon>-T'" 
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_no_jump) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
       by simp_all
     ultimately show ?case by (intro conjI)
@@ -3852,17 +3730,15 @@
       qed
     qed
     moreover
-    {
-      fix j have "abrupt s2 \<noteq> Some (Jump j)"
-      proof -
-        from BinOp.prems T 
-        have "Env\<turnstile>In1l (BinOp binop e1 e2)\<Colon>Inl (PrimT (binop_type binop))"
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_no_jump) (simp_all add: G wf) 
-      qed
-    }
+    have "abrupt s2 \<noteq> Some (Jump j)" for j
+    proof -
+      from BinOp.prems T 
+      have "Env\<turnstile>In1l (BinOp binop e1 e2)\<Colon>Inl (PrimT (binop_type binop))"
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_no_jump) (simp_all add: G wf) 
+    qed
     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
       by simp_all
     ultimately show ?case by (intro conjI) 
@@ -3998,21 +3874,19 @@
         finally show ?thesis .
       qed
     qed
-    moreover 
-    {
-      fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"
-      proof -
-        have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"
-          by (simp only: G) (rule eval.Ass Ass.hyps)+
-        from Ass.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with Ass.prems have "Env\<turnstile>var:=e\<Colon>-T'" by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_no_jump) (simp_all add: G wf)
-      qed
-    }
+    moreover
+    have "abrupt (assign upd v s2) \<noteq> Some (Jump j)" for j
+    proof -
+      have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"
+        by (simp only: G) (rule eval.Ass Ass.hyps)+
+      from Ass.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with Ass.prems have "Env\<turnstile>var:=e\<Colon>-T'" by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_no_jump) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) (assign upd v s2) A"
       and "?ResAssigned (Norm s0) (assign upd v s2)"       
       by simp_all
@@ -4122,20 +3996,18 @@
       qed
     qed
     moreover
-    {
-      fix j have "abrupt s2 \<noteq> Some (Jump j)"
-      proof -
-        have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
-          unfolding G by (rule eval.Cond Cond.hyps)+
-        from Cond.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with Cond.prems have "Env\<turnstile>e0 ? e1 : e2\<Colon>-T'" by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_no_jump) (simp_all add: G wf)
-      qed
-    } 
+    have "abrupt s2 \<noteq> Some (Jump j)" for j
+    proof -
+      have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
+        unfolding G by (rule eval.Cond Cond.hyps)+
+      from Cond.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with Cond.prems have "Env\<turnstile>e0 ? e1 : e2\<Colon>-T'" by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_no_jump) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
       by simp_all
     ultimately show ?case by (intro conjI)
@@ -4192,22 +4064,20 @@
       qed
     qed
     moreover
-    {
-      fix j have "abrupt (restore_lvars s2 s4) \<noteq> Some (Jump j)"
-      proof -
-        have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v
+    have "abrupt (restore_lvars s2 s4) \<noteq> Some (Jump j)" for j
+    proof -
+      have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v
                             \<rightarrow> (restore_lvars s2 s4)"
-          unfolding G by (rule eval.Call Call)+
-        from Call.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with Call.prems have "Env\<turnstile>({accC,statT,mode}e\<cdot>mn( {pTs}args))\<Colon>-T'" 
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_no_jump) (simp_all add: G wf)
-      qed
-    } 
+        unfolding G by (rule eval.Call Call)+
+      from Call.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with Call.prems have "Env\<turnstile>({accC,statT,mode}e\<cdot>mn( {pTs}args))\<Colon>-T'" 
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_no_jump) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) (restore_lvars s2 s4) A"
       and "?ResAssigned (Norm s0) (restore_lvars s2 s4)"
       by simp_all
@@ -4312,23 +4182,21 @@
       qed
     qed
     moreover
-    {
-      fix j have "abrupt s3 \<noteq> Some (Jump j)"
-      proof -
-        obtain w upd where v: "(w,upd)=v"
-          by (cases v) auto
-        have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"
-          by (simp only: G v) (rule eval.FVar FVar.hyps)+
-        from FVar.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with FVar.prems have "Env\<turnstile>({accC,statDeclC,stat}e..fn)\<Colon>=T'" 
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
-      qed
-    } 
+    have "abrupt s3 \<noteq> Some (Jump j)" for j
+    proof -
+      obtain w upd where v: "(w,upd)=v"
+        by (cases v) auto
+      have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"
+        by (simp only: G v) (rule eval.FVar FVar.hyps)+
+      from FVar.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with FVar.prems have "Env\<turnstile>({accC,statDeclC,stat}e..fn)\<Colon>=T'" 
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"
       by simp_all
     ultimately show ?case by (intro conjI)
@@ -4378,23 +4246,21 @@
       qed
     qed
     moreover
-    {
-      fix j have "abrupt s2' \<noteq> Some (Jump j)"
-      proof -
-        obtain w upd where v: "(w,upd)=v"
-          by (cases v) auto
-        have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"
-          unfolding G v by (rule eval.AVar AVar.hyps)+
-        from AVar.prems 
-        obtain T' where  "T=Inl T'"
-          by (elim wt_elim_cases) simp
-        with AVar.prems have "Env\<turnstile>(e1.[e2])\<Colon>=T'" 
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
-      qed
-    } 
+    have "abrupt s2' \<noteq> Some (Jump j)" for j
+    proof -
+      obtain w upd where v: "(w,upd)=v"
+        by (cases v) auto
+      have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"
+        unfolding G v by (rule eval.AVar AVar.hyps)+
+      from AVar.prems 
+      obtain T' where  "T=Inl T'"
+        by (elim wt_elim_cases) simp
+      with AVar.prems have "Env\<turnstile>(e1.[e2])\<Colon>=T'" 
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) s2' A" and "?ResAssigned (Norm s0) s2'"
       by simp_all
     ultimately show ?case by (intro conjI)
@@ -4438,21 +4304,19 @@
       qed
     qed
     moreover
-    {
-      fix j have "abrupt s2 \<noteq> Some (Jump j)"
-      proof -
-        have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"
-          unfolding G by (rule eval.Cons Cons.hyps)+
-        from Cons.prems 
-        obtain T' where  "T=Inr T'"
-          by (elim wt_elim_cases) simp
-        with Cons.prems have "Env\<turnstile>(e # es)\<Colon>\<doteq>T'" 
-          by simp
-        from eval _ this
-        show ?thesis
-          by (rule eval_expression_list_no_jump) (simp_all add: G wf)
-      qed
-    } 
+    have "abrupt s2 \<noteq> Some (Jump j)" for j
+    proof -
+      have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"
+        unfolding G by (rule eval.Cons Cons.hyps)+
+      from Cons.prems 
+      obtain T' where  "T=Inr T'"
+        by (elim wt_elim_cases) simp
+      with Cons.prems have "Env\<turnstile>(e # es)\<Colon>\<doteq>T'" 
+        by simp
+      from eval _ this
+      show ?thesis
+        by (rule eval_expression_list_no_jump) (simp_all add: G wf)
+    qed
     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
       by simp_all
     ultimately show ?case by (intro conjI)
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/Eval.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -888,12 +888,12 @@
 
 lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In1l (Callee l e)"
-    then have "False" by induct auto
-  }  
+  have False
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In1l (Callee l e)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce
 qed
@@ -901,36 +901,36 @@
 
 lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In1l (InsInitE c e)"
-    then have "False" by induct auto
-  }
+  have "False"
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In1l (InsInitE c e)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce
 qed
 
 lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In2 (InsInitV c w)"
-    then have "False" by induct auto
-  }  
+  have "False"
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In2 (InsInitV c w)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce
 qed
 
 lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In1r (FinA a c)"
-    then have "False" by induct auto
-  }  
+  have "False"
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In1r (FinA a c)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce 
 qed
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/Evaln.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -297,48 +297,48 @@
 
 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In1l (Callee l e)"
-    then have "False" by induct auto
-  }
+  have "False"
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In1l (Callee l e)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce 
 qed
 
 lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In1l (InsInitE c e)"
-    then have "False" by induct auto
-  }
+  have "False"
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In1l (InsInitE c e)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce
 qed
 
 lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In2 (InsInitV c w)"
-    then have "False" by induct auto
-  }  
+  have "False"
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In2 (InsInitV c w)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce
 qed
 
 lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
 proof -
-  { fix s t v s'
-    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
-         normal: "normal s" and
-         callee: "t=In1r (FinA a c)"
-    then have "False" by induct auto
-  } 
+  have "False"
+    if eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')"
+    and normal: "normal s"
+    and callee: "t=In1r (FinA a c)"
+    for s t v s'
+    using that by induct auto
   then show ?thesis
     by (cases s') fastforce
 qed
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -230,17 +230,14 @@
     proof
       assume eq_C_D: "C=D"
       show "False"
-      proof -
+      proof (rule notE)
         from subcls1_C_Z eq_C_D 
-        have "G\<turnstile>D \<prec>\<^sub>C Z"
+        show "G\<turnstile>D \<prec>\<^sub>C Z"
           by (auto)
         also
         from subcls_Z_D ws   
-        have "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
+        show "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
           by (rule subcls_acyclic)
-        ultimately 
-        show ?thesis 
-          by - (rule notE)
       qed
     qed
   qed
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -1614,87 +1614,73 @@
     from eval_e1 have 
       s0_s1:"dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
       by (rule dom_locals_eval_mono_elim)
-    {
-      assume condAnd: "binop=CondAnd"
-      have ?thesis
-      proof -
-        from da obtain E2' where
-          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
+    consider (condAnd) "binop=CondAnd" | (condOr) "binop=CondOr" | (notAndOr) "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
+      by (cases binop) auto
+    then show ?thesis
+    proof cases
+      case condAnd
+      from da obtain E2' where
+        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
              \<turnstile> dom (locals (store s0)) \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
-          by cases (simp add: condAnd)+
-        moreover
-        have "dom (locals (store s0)) 
+        by cases (simp add: condAnd)+
+      moreover
+      have "dom (locals (store s0)) 
           \<union> assigns_if True e1 \<subseteq> dom (locals (store s1))"
-        proof -
-          from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
-            by simp
-          with normal_s1 conf_v1 obtain b where "v1=Bool b"
-            by (auto dest: conf_Boolean)
-          with True condAnd
-          have v1: "v1=Bool True"
-            by simp
-          from eval_e1 normal_s1 
-          have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
-            by (rule assigns_if_good_approx' [elim_format])
-               (insert wt_e1, simp_all add: e1T v1)
-          with s0_s1 show ?thesis by (rule Un_least)
-        qed
-        ultimately
-        show ?thesis
-          using that by (cases rule: da_weakenE) (simp add: True)
+      proof -
+        from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
+          by simp
+        with normal_s1 conf_v1 obtain b where "v1=Bool b"
+          by (auto dest: conf_Boolean)
+        with True condAnd
+        have v1: "v1=Bool True"
+          by simp
+        from eval_e1 normal_s1 
+        have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
+          by (rule assigns_if_good_approx' [elim_format])
+            (insert wt_e1, simp_all add: e1T v1)
+        with s0_s1 show ?thesis by (rule Un_least)
       qed
-    }
-    moreover
-    { 
-      assume condOr: "binop=CondOr"
-      have ?thesis
+      ultimately show ?thesis
+        using that by (cases rule: da_weakenE) (simp add: True)
+    next
+      case condOr
         (* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
-      proof -
-        from da obtain E2' where
-          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
+      from da obtain E2' where
+        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
               \<turnstile> dom (locals (store s0)) \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
-          by cases (simp add: condOr)+
-        moreover
-        have "dom (locals (store s0)) 
+        by cases (simp add: condOr)+
+      moreover
+      have "dom (locals (store s0)) 
                      \<union> assigns_if False e1 \<subseteq> dom (locals (store s1))"
-        proof -
-          from condOr wt_binop have e1T: "e1T=PrimT Boolean"
-            by simp
-          with normal_s1 conf_v1 obtain b where "v1=Bool b"
-            by (auto dest: conf_Boolean)
-          with True condOr
-          have v1: "v1=Bool False"
-            by simp
-          from eval_e1 normal_s1 
-          have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
-            by (rule assigns_if_good_approx' [elim_format])
-               (insert wt_e1, simp_all add: e1T v1)
-          with s0_s1 show ?thesis by (rule Un_least)
-        qed
-        ultimately
-        show ?thesis
-          using that by (rule da_weakenE) (simp add: True)
+      proof -
+        from condOr wt_binop have e1T: "e1T=PrimT Boolean"
+          by simp
+        with normal_s1 conf_v1 obtain b where "v1=Bool b"
+          by (auto dest: conf_Boolean)
+        with True condOr
+        have v1: "v1=Bool False"
+          by simp
+        from eval_e1 normal_s1 
+        have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
+          by (rule assigns_if_good_approx' [elim_format])
+            (insert wt_e1, simp_all add: e1T v1)
+        with s0_s1 show ?thesis by (rule Un_least)
       qed
-    }
-    moreover
-    {
-      assume notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
-      have ?thesis
-      proof -
-        from da notAndOr obtain E1' where
-          da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
+      ultimately show ?thesis
+        using that by (rule da_weakenE) (simp add: True)
+    next
+      case notAndOr
+      from da notAndOr obtain E1' where
+        da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1'"
-          and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
-          by cases simp+
-        from eval_e1 wt_e1 da_e1 wf normal_s1 
-        have "nrm E1' \<subseteq> dom (locals (store s1))"
-          by (cases rule: da_good_approxE') iprover
-        with da_e2 show ?thesis
-          using that by (rule da_weakenE) (simp add: True)
-      qed
-    }
-    ultimately show ?thesis
-      by (cases binop) auto
+        and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
+        by cases simp+
+      from eval_e1 wt_e1 da_e1 wf normal_s1 
+      have "nrm E1' \<subseteq> dom (locals (store s1))"
+        by (cases rule: da_good_approxE') iprover
+      with da_e2 show ?thesis
+        using that by (rule da_weakenE) (simp add: True)
+    qed
   qed
   thus ?thesis ..
 qed
@@ -2503,20 +2489,18 @@
     from error_free_s1 s2
     have error_free_s2: "error_free s2"
       by simp
-    {
-      assume norm_s2: "normal s2"
-      have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
-      proof -
-        from s2 norm_s2 have "normal s1"
-          by (cases s1) simp
-        with v_ok 
-        have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
-          by simp
-        with eT wf s2 T norm_s2
-        show ?thesis
-          by (cases s1) (auto dest: fits_conf)
-      qed
-    }
+    have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
+      if norm_s2: "normal s2"
+    proof -
+      from s2 norm_s2 have "normal s1"
+        by (cases s1) simp
+      with v_ok 
+      have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
+        by simp
+      with eT wf s2 T norm_s2
+      show ?thesis
+        by (cases s1) (auto dest: fits_conf)
+    qed
     with conf_s2 error_free_s2
     show "s2\<Colon>\<preceq>(G, L) \<and> 
            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T)  \<and>
@@ -2700,24 +2684,22 @@
       da_v: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 v\<guillemotright> V"
       by (cases "\<exists> n. v=LVar n") (insert da.LVar, auto elim!: da_elim_cases)
-    {
-      fix n assume lvar: "v=LVar n"
-      have "locals (store s1) n \<noteq> None"
+    have lvar_in_locals: "locals (store s1) n \<noteq> None"
+      if lvar: "v=LVar n" for n
+    proof -
+      from Acc.prems lvar have 
+        "n \<in> dom (locals s0)"
+        by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
+      also
+      have "dom (locals s0) \<subseteq> dom (locals (store s1))"
       proof -
-        from Acc.prems lvar have 
-          "n \<in> dom (locals s0)"
-          by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
-        also
-        have "dom (locals s0) \<subseteq> dom (locals (store s1))"
-        proof -
-          from \<open>G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1\<close>
-          show ?thesis
-            by (rule dom_locals_eval_mono_elim) simp
-        qed
-        finally show ?thesis
-          by blast
+        from \<open>G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1\<close>
+        show ?thesis
+          by (rule dom_locals_eval_mono_elim) simp
       qed
-    } note lvar_in_locals = this 
+      finally show ?thesis
+        by blast
+    qed
     from conf_s0 wt_v da_v
     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)"
       and  conf_var: "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In2 v\<succ>In2 (w, upd)\<Colon>\<preceq>Inl vT)"
@@ -3018,28 +3000,26 @@
            conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
            error_free_s1: "error_free s1" 
       by (rule hyp_e [elim_format]) simp
-    { 
-      assume abnormal_s2: "\<not> normal s2"
-      have "set_lvars (locals (store s2)) s4 = s2"
-      proof -
-        from abnormal_s2 init_lvars 
-        obtain keep_abrupt: "abrupt s3 = abrupt s2" and
-             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
+    have propagate_abnormal_s2: "set_lvars (locals (store s2)) s4 = s2"
+      if abnormal_s2: "\<not> normal s2"
+    proof -
+      from abnormal_s2 init_lvars 
+      obtain keep_abrupt: "abrupt s3 = abrupt s2" and
+        "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
                                             mode a vs s2)" 
-          by (auto simp add: init_lvars_def2)
-        moreover
-        from keep_abrupt abnormal_s2 check
-        have eq_s3'_s3: "s3'=s3" 
-          by (auto simp add: check_method_access_def Let_def)
-        moreover
-        from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
-        have "s4=s3'"
-          by auto
-        ultimately show
-          "set_lvars (locals (store s2)) s4 = s2"
-          by (cases s2,cases s3) (simp add: init_lvars_def2)
-      qed
-    } note propagate_abnormal_s2 = this
+        by (auto simp add: init_lvars_def2)
+      moreover
+      from keep_abrupt abnormal_s2 check
+      have eq_s3'_s3: "s3'=s3" 
+        by (auto simp add: check_method_access_def Let_def)
+      moreover
+      from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
+      have "s4=s3'"
+        by auto
+      ultimately show
+        "set_lvars (locals (store s2)) s4 = s2"
+        by (cases s2,cases s3) (simp add: init_lvars_def2)
+    qed
     show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
            (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
              G,L,store ((set_lvars (locals (store s2))) s4)
@@ -3419,26 +3399,24 @@
         by force
     qed
     moreover
-    {
-      assume normal_upd_s2:  "normal (abupd (absorb Ret) s2)"
-      have "Result \<in> dom (locals (store s2))"
-      proof -
-        from normal_upd_s2
-        have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
-          by (cases s2) (simp add: absorb_def)
-        thus ?thesis
-        proof 
-          assume "normal s2"
-          with eval_c wt_c da_C' wf res nrm_C'
-          show ?thesis
-            by (cases rule: da_good_approxE') blast
-        next
-          assume "abrupt s2 = Some (Jump Ret)"
-          with conf_s2 show ?thesis
-            by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
-        qed 
-      qed
-    }
+    have "Result \<in> dom (locals (store s2))"
+      if normal_upd_s2:  "normal (abupd (absorb Ret) s2)"
+    proof -
+      from normal_upd_s2
+      have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
+        by (cases s2) (simp add: absorb_def)
+      thus ?thesis
+      proof 
+        assume "normal s2"
+        with eval_c wt_c da_C' wf res nrm_C'
+        show ?thesis
+          by (cases rule: da_good_approxE') blast
+      next
+        assume "abrupt s2 = Some (Jump Ret)"
+        with conf_s2 show ?thesis
+          by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
+      qed 
+    qed
     moreover note T resultT
     ultimately
     show "abupd (absorb Ret) s3\<Colon>\<preceq>(G, L) \<and>
@@ -3939,29 +3917,27 @@
     from wt_c1 da_c1
     have P_c1: "P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1"
       by (rule Comp.hyps)
-    {
-      fix Q
-      assume normal_s1: "normal s1"
-      assume elim: "\<And> C2'. 
+    have thesis
+      if normal_s1: "normal s1"
+      and elim: "\<And> C2'.
                     \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright>C2';
-                       P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q"
-      have Q
+                       P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> thesis"
+      for thesis
+    proof -
+      obtain C2' where 
+        da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
       proof -
-        obtain C2' where 
-          da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
-        proof -
-          from eval_c1 wt_c1 da_c1 wf normal_s1
-          have "nrm C1 \<subseteq> dom (locals (store s1))"
-            by (cases rule: da_good_approxE') iprover
-          with da_c2 show thesis
-            by (rule da_weakenE) (rule that)
-        qed
-        with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
-          by (rule Comp.hyps)
-        with da show ?thesis
-          using elim by iprover
+        from eval_c1 wt_c1 da_c1 wf normal_s1
+        have "nrm C1 \<subseteq> dom (locals (store s1))"
+          by (cases rule: da_good_approxE') iprover
+        with da_c2 show thesis
+          by (rule da_weakenE) (rule that)
       qed
-    }
+      with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
+        by (rule Comp.hyps)
+      with da show ?thesis
+        using elim by iprover
+    qed
     with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
     show ?case
       by (rule comp) iprover+
@@ -3985,39 +3961,37 @@
     from wt_e da_e
     have P_e: "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1"
       by (rule If.hyps)
-    {
-      fix Q
-      assume normal_s1: "normal s1"
-      assume elim: "\<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
-                                   \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
-                              P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
-                              \<rbrakk> \<Longrightarrow> Q"
-      have Q
-      proof -
-        obtain C' where
-          da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
+    have thesis
+      if normal_s1: "normal s1"
+      and elim: "\<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
+                             \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
+                        P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
+                        \<rbrakk> \<Longrightarrow> thesis"
+    for thesis
+    proof -
+      obtain C' where
+        da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
                 (dom (locals (store s1)))\<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<guillemotright> C'"
-        proof -
-          from eval_e have 
-            "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
-            by (rule dom_locals_eval_mono_elim)
-          moreover
-          from eval_e normal_s1 wt_e 
-          have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
-            by (rule assigns_if_good_approx')
-          ultimately 
-          have "dom (locals (store ((Norm s0)::state))) 
+      proof -
+        from eval_e have 
+          "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
+          by (rule dom_locals_eval_mono_elim)
+        moreover
+        from eval_e normal_s1 wt_e 
+        have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
+          by (rule assigns_if_good_approx')
+        ultimately 
+        have "dom (locals (store ((Norm s0)::state))) 
             \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
-            by (rule Un_least)
-          with da_then_else show thesis
-            by (rule da_weakenE) (rule that)
-        qed
-        with wt_then_else
-        have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
-          by (rule If.hyps)
-        with da show ?thesis using elim by iprover
+          by (rule Un_least)
+        with da_then_else show thesis
+          by (rule da_weakenE) (rule that)
       qed
-    }
+      with wt_then_else
+      have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
+        by (rule If.hyps)
+      with da show ?thesis using elim by iprover
+    qed
     with eval_e eval_then_else wt_e wt_then_else da_e P_e
     show ?case
       by (rule "if") iprover+
diff -r c8283b7f0791 -r 1263d1143bab src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Fri Nov 15 21:43:22 2024 +0100
+++ b/src/HOL/Bali/WellForm.thy	Fri Nov 15 23:20:24 2024 +0100
@@ -927,15 +927,16 @@
     from wf cls_C neq_C_Obj
     have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 
       by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
-    {
-      fix old
-      assume    member_super: "G\<turnstile>Method old member_of (super c)"
-      assume     inheritable: "G \<turnstile>Method old inheritable_in pid C"
-      assume instance_method: "\<not> is_static old"
+    have hyp_member_super: "?P C old"
+      if member_super: "G\<turnstile>Method old member_of (super c)"
+      and inheritable: "G \<turnstile>Method old inheritable_in pid C"
+      and instance_method: "\<not> is_static old"
+    for old
+    proof -
       from member_super
       have old_declared: "G\<turnstile>Method old declared_in (declclass old)"
        by (cases old) (auto dest: member_of_declC)
-      have "?P C old"
+      show ?thesis
       proof (cases "G\<turnstile>mid (msig old) undeclared_in C")
         case True
         with inheritable super accessible_super member_super
@@ -982,7 +983,7 @@
             by (contradiction)
         qed
       qed
-    } note hyp_member_super = this
+    qed
     from subclsC cls_C 
     have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old"
       by (rule subcls_superD)
@@ -1411,9 +1412,8 @@
         \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
   proof (induct C rule: ws_class_induct')
     case Object
-    assume "methd G Object sig = Some m" 
-    with wf show ?thesis
-      by - (rule method_declared_inI, auto) 
+    show ?thesis if "methd G Object sig = Some m"
+      by (rule method_declared_inI) (use wf that in auto)
   next
     case Subcls
     fix C c
@@ -2012,15 +2012,13 @@
   shows "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
 proof -
   from wf have ws: "ws_prog G" by simp
-  {
-    fix I i new
-    assume ifI: "iface G I = Some i"
-    assume new: "table_of (imethods i) sig = Some new" 
-    from ifI new not_private wf old  
-    have "?P (I,new)"
+  have hyp_newmethod: "?P (I,new)"
+    if ifI: "iface G I = Some i"
+    and new: "table_of (imethods i) sig = Some new"
+    for I i new
+    using ifI new not_private wf old  
       by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD
             simp del: methd_Object)
-  } note hyp_newmethod = this  
   from is_if_I ws new 
   show ?thesis
   proof (induct rule: ws_interface_induct)
@@ -2540,7 +2538,7 @@
   from subclseq iscls_statC 
   have iscls_dynC: "is_class G dynC"
     by (rule subcls_is_class2)
-  from  iscls_dynC iscls_statC wf m
+  from iscls_dynC iscls_statC wf m
   have "G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and>
         methd G (declclass m) sig = Some m" 
     by - (drule dynmethd_declC, auto)