--- 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>
--- 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)"
--- 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
--- 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
--- 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)