# HG changeset patch
# User wenzelm
# Date 1731784946 -3600
# Node ID d8f77c1c97034e1a8d73ebdeb035cc3ecb14ef54
# Parent  dc35aa7d5311781e52b72c4362101febf8b5363b
tuned proofs;

diff -r dc35aa7d5311 -r d8f77c1c9703 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Sat Nov 16 19:54:30 2024 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Sat Nov 16 20:22:26 2024 +0100
@@ -337,7 +337,7 @@
           apply (rule MGFnD' [THEN conseq12, THEN allI])
           apply (clarsimp simp add: split_paired_all)
           apply (rule eval.Init [OF c])
-          apply (insert c)
+          using c
           apply auto
           done
       qed
@@ -579,7 +579,7 @@
       note abrupt_s' = this
       from eval_e _ wt wf
       have no_cont: "abrupt s' \<noteq> Some (Jump (Cont l))"
-        by (rule eval_expression_no_jump') (insert normal_t,simp)
+        by (rule eval_expression_no_jump') (use normal_t in simp)
       have
         "if the_Bool v 
              then (G\<turnstile>s' \<midarrow>c\<rightarrow> s' \<and> 
diff -r dc35aa7d5311 -r d8f77c1c9703 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Sat Nov 16 19:54:30 2024 +0100
+++ b/src/HOL/Bali/AxSound.thy	Sat Nov 16 20:22:26 2024 +0100
@@ -917,7 +917,7 @@
         case True
         from eval_e1 wt_e1 da_e1 conf_s0 wf
         have conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" 
-          by (rule evaln_type_sound [elim_format]) (insert True,simp)
+          by (rule evaln_type_sound [elim_format]) (use True in simp)
         from eval_e1 
         have "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
           by (rule evaln_eval)
@@ -985,7 +985,7 @@
         by cases simp
       from da obtain V where 
         da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
-        by (cases "\<exists> n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
+        by (cases "\<exists> n. var=LVar n") (use da.LVar in \<open>auto elim!: da_elim_cases\<close>)
       from eval obtain upd where
         eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(v, upd)\<midarrow>n\<rightarrow> s1"
         using normal_s0 by (fastforce elim: evaln_elim_cases)
@@ -1266,7 +1266,7 @@
       have s1_no_return: "abrupt s1 \<noteq> Some (Jump Ret)"
         by (rule eval_expression_no_jump 
                  [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
-           (insert normal_s0,auto)
+           (use normal_s0 in auto)
 
       from valid_e P valid_A conf_s0 evaln_e wt_e da_e
       obtain "Q \<lfloor>a\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
@@ -1397,13 +1397,13 @@
           by (rule evaln_eval)
         from evaln_e wt_e da_e conf_s0 wf
         have conf_a: "G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
-          by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp)
+          by (rule evaln_type_sound [elim_format]) (use normal_s1 in simp)
         with normal_s1 normal_s2 eval_args 
         have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
           by (auto dest: eval_gext)
         from evaln_args wt_args da_args' conf_s1 wf
         have conf_args: "list_all2 (conf G (store s2)) vs pTs"
-          by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp)
+          by (rule evaln_type_sound [elim_format]) (use normal_s2 in simp)
         from statM 
         obtain
           statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
@@ -1645,10 +1645,9 @@
         by (rule validE)
       have "s3=s2"
       proof -
-        from eval_init [THEN evaln_eval] wf
         have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
-          by - (rule eval_statement_no_jump [OF _ _ _ wt_init],
-                insert normal_s0,auto)
+          by (rule eval_statement_no_jump [OF _ _ _ wt_init])
+            (use eval_init [THEN evaln_eval] wf normal_s0 in auto)
         from eval_c [THEN evaln_eval] _ wt_c wf
         have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
           by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
@@ -2310,7 +2309,7 @@
         from sxalloc wf
         have "s2=s1"
           by (rule sxalloc_type_sound [elim_format])
-             (insert False, auto split: option.splits abrupt.splits )
+             (use False in \<open>auto split: option.splits abrupt.splits\<close>)
         with False 
         have no_catch: "\<not>  G,s2\<turnstile>catch C"
           by (simp add: catch_def)
@@ -2437,7 +2436,7 @@
         by auto
       from eval_c1 wt_c1 da_c1 conf_s0 wf
       have  "error_free (abr1,s1)"
-        by (rule evaln_type_sound  [elim_format]) (insert normal_s0,simp)
+        by (rule evaln_type_sound  [elim_format]) (use normal_s0 in simp)
       with s3 have s3': "s3 = abupd (abrupt_if (abr1 \<noteq> None) abr1) s2"
         by (simp add: error_free_def)
       from conf_s1 
@@ -2544,8 +2543,8 @@
           using that by (auto intro: assigned.select_convs)
       next
         case False 
-        with da_Init show ?thesis
-          by - (rule that, auto intro: assigned.select_convs)
+        show ?thesis
+          by (rule that) (use da_Init False in \<open>auto intro: assigned.select_convs\<close>)
       qed
       from normal_s0 conf_s0 wf cls_C not_inited
       have conf_init_cls: "(Norm ((init_class_obj G C) (store s0)))\<Colon>\<preceq>(G, L)"
diff -r dc35aa7d5311 -r d8f77c1c9703 src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Sat Nov 16 19:54:30 2024 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Sat Nov 16 20:22:26 2024 +0100
@@ -1201,11 +1201,11 @@
       by blast
     note hyp_c2 = \<open>PROP ?Hyp Env B \<langle>c2\<rangle> C2\<close>
     from da_c2' B' 
-     obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
-       by - (drule hyp_c2,auto)
-     with A A' C1'
-     show ?case
-       by auto
+    obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
+      by - (drule hyp_c2,auto)
+    with A A' C1'
+    show ?case
+      by auto
    next
      case Init thus ?case by (elim da_elim_cases) auto
    next
diff -r dc35aa7d5311 -r d8f77c1c9703 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Nov 16 19:54:30 2024 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Nov 16 20:22:26 2024 +0100
@@ -3805,7 +3805,7 @@
         from Ass.prems obtain E where
           da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
           nrm_A: "nrm A = nrm E \<union> {vn}"
-          by (elim da_elim_cases) (insert vn,auto)
+          by (elim da_elim_cases) (use vn in auto)
         obtain E' where
           da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" and
           E_E': "nrm E \<subseteq> nrm E'"
@@ -3849,7 +3849,7 @@
         from Ass.prems obtain V where
           da_var: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>var\<rangle>\<guillemotright> V" and
           da_e:   "Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
-          by (elim da_elim_cases) (insert False,simp+)
+          by (elim da_elim_cases) (use False in simp_all)
         from hyp_var wt_var da_var G normal_s1
         have "nrm V \<subseteq> dom (locals (store s1))"
           by simp
diff -r dc35aa7d5311 -r d8f77c1c9703 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Sat Nov 16 19:54:30 2024 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Sat Nov 16 20:22:26 2024 +0100
@@ -560,7 +560,7 @@
         eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
              eq_mheads:"sm=mhead (mthd dm) "
       by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
-    then have static: "is_static dm = is_static sm" by - (auto)
+    then have static: "is_static dm = is_static sm" by auto
     with declC invC dynlookup_static dm
     have declC': "declC = (declclass dm)"  
       by (auto simp add: invocation_declclass_def)
@@ -1421,9 +1421,8 @@
   next
     case (Cons y tl)
     note ys = \<open>ys=y#tl\<close>
-    with tab_vn tab'_vn 
     have "(tab(x\<mapsto>y)) vn = Some el"
-      by - (rule Cons.hyps,auto)
+      by (rule Cons.hyps) (use tab_vn tab'_vn ys in auto)
     moreover from tab'_vn ys
     have "(tab'(x\<mapsto>y, xs[\<mapsto>]tl)) vn = None" 
       by simp
@@ -1503,8 +1502,8 @@
     case Nil with len show ?thesis by simp
   next
     case (Cons y tl)
-    with len have "dom (tab(x\<mapsto>y, xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
-      by - (rule Hyp,simp)
+    have "dom (tab(x\<mapsto>y, xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
+      by (rule Hyp) (use len Cons in simp)
     moreover 
     have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
       by (rule dom_map_upd)
@@ -1637,7 +1636,7 @@
         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)
+            (use wt_e1 in \<open>simp_all add: e1T v1\<close>)
         with s0_s1 show ?thesis by (rule Un_least)
       qed
       ultimately show ?thesis
@@ -1663,7 +1662,7 @@
         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)
+            (use wt_e1 in \<open>simp_all add: e1T v1\<close>)
         with s0_s1 show ?thesis by (rule Un_least)
       qed
       ultimately show ?thesis
@@ -2102,7 +2101,7 @@
       from sx_alloc wf
       have eq_s2_s1: "s2=s1"
         by (rule sxalloc_type_sound [elim_format])
-           (insert False, auto split: option.splits abrupt.splits )
+           (use False in \<open>auto split: option.splits abrupt.splits\<close>)
       with False 
       have "\<not>  G,s2\<turnstile>catch catchC"
         by (simp add: catch_def)
@@ -2258,8 +2257,7 @@
     note cls = \<open>the (class G C) = c\<close>
     note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
     note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T\<close>
-    with cls
-    have cls_C: "class G C = Some c"
+    with cls have cls_C: "class G C = Some c"
       by - (erule wt_elim_cases, auto)
     show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
           (error_free (Norm s0) = error_free s3)"
@@ -2305,8 +2303,8 @@
           using that by (auto intro: assigned.select_convs)
       next
         case False 
-        with da_Init show ?thesis
-          by - (rule that, auto intro: assigned.select_convs)
+        show ?thesis
+          by (rule that) (use da_Init False in \<open>auto intro: assigned.select_convs\<close>)
       qed
       ultimately 
       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
@@ -2418,17 +2416,17 @@
          \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (init_comp_ty elT)\<guillemotright> I"
       proof (cases "\<exists>C. elT = 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
       ultimately show thesis
@@ -2683,7 +2681,7 @@
     from Acc.prems obtain V where
       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)
+      by (cases "\<exists> n. v=LVar n") (use da.LVar in \<open>auto elim!: da_elim_cases\<close>)
     have lvar_in_locals: "locals (store s1) n \<noteq> None"
       if lvar: "v=LVar n" for n
     proof -
@@ -3384,9 +3382,8 @@
       from iscls_D
       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)
+        by (rule eval_statement_no_jump [OF _ _ _ wt_init]) (use eval_init wf in auto)
       from eval_c _ wt_c wf
       have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
         by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)