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+