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