--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Wed Jun 13 00:01:41 2007 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
header {* Correctness of Definite Assignment *}
theory DefiniteAssignmentCorrect imports WellForm Eval begin
@@ -107,8 +109,8 @@
and True
proof (induct rule: var_expr_stmt.inducts)
case (Lab j c jmps' jmps)
- have jmpOk: "jumpNestingOkS jmps' (j\<bullet> c)" .
- have jmps: "jmps' \<subseteq> jmps" .
+ note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
+ note jmps = `jmps' \<subseteq> jmps`
with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp
moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto
ultimately
@@ -138,10 +140,11 @@
by simp
next
case (Loop l e c jmps' jmps)
- have "jumpNestingOkS jmps' (l\<bullet> While(e) c)" .
- hence "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
- moreover have "jmps' \<subseteq> jmps" .
- hence "{Cont l} \<union> jmps' \<subseteq> {Cont l} \<union> jmps" by auto
+ from `jumpNestingOkS jmps' (l\<bullet> While(e) c)`
+ have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
+ moreover
+ from `jmps' \<subseteq> jmps`
+ have "{Cont l} \<union> jmps' \<subseteq> {Cont l} \<union> jmps" by auto
ultimately
have "jumpNestingOkS ({Cont l} \<union> jmps) c"
by (rule Loop.hyps)
@@ -310,8 +313,8 @@
case Expr thus ?case by (elim wt_elim_cases) simp
next
case (Lab s0 c s1 jmp jmps T Env)
- have jmpOK: "jumpNestingOk jmps (In1r (jmp\<bullet> c))" .
- have G: "prg Env = G" .
+ note jmpOK = `jumpNestingOk jmps (In1r (jmp\<bullet> c))`
+ note G = `prg Env = G`
have wt_c: "Env\<turnstile>c\<Colon>\<surd>"
using Lab.prems by (elim wt_elim_cases)
{
@@ -321,7 +324,7 @@
proof -
from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
by (cases s1) (simp add: absorb_def)
- have hyp_c: "PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>" .
+ note hyp_c = `PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>`
from ab_s1 have "j \<noteq> jmp"
by (cases s1) (simp add: absorb_def)
moreover have "j \<in> {jmp} \<union> jmps"
@@ -339,9 +342,9 @@
thus ?case by simp
next
case (Comp s0 c1 s1 c2 s2 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (c1;; c2))" .
- have G: "prg Env = G" .
- from Comp.prems obtain
+ note jmpOk = `jumpNestingOk jmps (In1r (c1;; c2))`
+ note G = `prg Env = G`
+ from Comp.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
{
@@ -351,11 +354,11 @@
proof -
have jmp: "?Jmp jmps s1"
proof -
- have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>" .
+ note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>`
with wt_c1 jmpOk G
show ?thesis by simp
qed
- moreover have hyp_c2: "PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)" .
+ moreover note hyp_c2 = `PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)`
have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
moreover note wt_c2 G abr_s2
ultimately show "j \<in> jmps"
@@ -364,8 +367,8 @@
} thus ?case by simp
next
case (If s0 e b s1 c1 c2 s2 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (If(e) c1 Else c2))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (If(e) c1 Else c2))`
+ note G = `prg Env = G`
from If.prems obtain
wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and
wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
@@ -375,11 +378,11 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
with wt_e G have "?Jmp jmps s1"
by simp
- moreover have hyp_then_else:
- "PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>" .
+ moreover note hyp_then_else =
+ `PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>`
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
@@ -390,9 +393,9 @@
thus ?case by simp
next
case (Loop s0 e b s1 c s2 l s3 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (l\<bullet> While(e) c))" .
- have G: "prg Env = G" .
- have wt: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
+ note jmpOk = `jumpNestingOk jmps (In1r (l\<bullet> While(e) c))`
+ note G = `prg Env = G`
+ note wt = `Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
then obtain
wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and
wt_c: "Env\<turnstile>c\<Colon>\<surd>"
@@ -402,7 +405,7 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
with wt_e G have jmp_s1: "?Jmp jmps s1"
by simp
show ?thesis
@@ -470,8 +473,8 @@
case (Jmp s j jmps T Env) thus ?case by simp
next
case (Throw s0 e a s1 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (Throw e))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (Throw e))`
+ note G = `prg Env = G`
from Throw.prems obtain Te where
wt_e: "Env\<turnstile>e\<Colon>-Te"
by (elim wt_elim_cases)
@@ -480,8 +483,8 @@
assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .
- hence "?Jmp jmps s1" using wt_e G by simp
+ from `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
+ have "?Jmp jmps s1" using wt_e G by simp
moreover
from jmp
have "abrupt s1 = Some (Jump j)"
@@ -492,8 +495,8 @@
thus ?case by simp
next
case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
- have jmpOk: "jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))`
+ note G = `prg Env = G`
from Try.prems obtain
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>"
@@ -503,10 +506,10 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)`
with jmpOk wt_c1 G
have jmp_s1: "?Jmp jmps s1" by simp
- have s2: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
+ note s2 = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
show "j \<in> jmps"
proof (cases "G,s2\<turnstile>catch C")
case False
@@ -544,8 +547,8 @@
thus ?case by simp
next
case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
- have jmpOk: " jumpNestingOk jmps (In1r (c1 Finally c2))" .
- have G: "prg Env = G" .
+ note jmpOk = `jumpNestingOk jmps (In1r (c1 Finally c2))`
+ note G = `prg Env = G`
from Fin.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
@@ -555,16 +558,16 @@
have "j \<in> jmps"
proof (cases "x1=Some (Jump j)")
case True
- have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>" .
+ note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>`
with True jmpOk wt_c1 G show ?thesis
by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
next
case False
- have hyp_c2: "PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>" .
- have "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+ note hyp_c2 = `PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>`
+ note `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
with False jmp have "abrupt s2 = Some (Jump j)"
- by (cases s2, simp add: abrupt_if_def)
+ 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
@@ -572,9 +575,9 @@
thus ?case by simp
next
case (Init C c s0 s3 s1 s2 jmps T Env)
- have "jumpNestingOk jmps (In1r (Init C))".
- have G: "prg Env = G" .
- have "the (class G C) = c" .
+ note `jumpNestingOk jmps (In1r (Init C))`
+ note G = `prg Env = G`
+ note `the (class G C) = c`
with Init.prems have c: "class G C = Some c"
by (elim wt_elim_cases) auto
{
@@ -642,16 +645,15 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have "prg Env = G" .
- moreover have hyp_init: "PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>" .
+ note `prg Env = G`
+ moreover note hyp_init = `PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>`
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 -
- have "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
- from this jmp show ?thesis
+ from `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2` and jmp show ?thesis
by (rule halloc_no_jump')
qed
ultimately show "j \<in> jmps"
@@ -666,20 +668,20 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have G: "prg Env = G" .
+ note G = `prg Env = G`
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')
- have "PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>" .
+ note `PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>`
with wt_init G
have "?Jmp jmps s1"
by (simp add: init_comp_ty_def)
moreover
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 i)" .
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 i)`
have "abrupt s2 = Some (Jump j)"
proof -
- have "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
+ note `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
moreover note jmp
ultimately
have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
@@ -698,14 +700,14 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
- have "prg Env = G" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+ note `prg Env = G`
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 -
- have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .
+ note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
moreover note jmp
ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
qed
@@ -721,8 +723,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
- have "prg Env = G" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+ note `prg Env = G`
moreover from Inst.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover note jmp
@@ -740,8 +742,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
- have "prg Env = G" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+ note `prg Env = G`
moreover from UnOp.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover note jmp
@@ -757,17 +759,17 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have G: "prg Env = G" .
+ note G = `prg Env = G`
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)
- have "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)" .
+ note `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)`
with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
- have hyp_e2:
- "PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
- s1 s2 (In1 v2)" .
+ note hyp_e2 =
+ `PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
+ s1 s2 (In1 v2)`
show "j\<in>jmps"
proof (cases "need_second_arg binop v1")
case True with jmp_s1 wt_e2 jmp G
@@ -790,8 +792,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_va: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))" .
- have "prg Env = G" .
+ note hyp_va = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))`
+ note `prg Env = G`
moreover from Acc.prems
obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
moreover note jmp
@@ -802,14 +804,14 @@
thus ?case by simp
next
case (Ass s0 va w f s1 e v s2 jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Ass.prems
obtain vT eT where
wt_va: "Env\<turnstile>va\<Colon>=vT" and
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have hyp_v: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))" .
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 v)" .
+ note hyp_v = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))`
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 v)`
{
fix j
assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
@@ -818,8 +820,7 @@
have "abrupt s2 = Some (Jump j)"
proof (cases "normal s2")
case True
- have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
- from this True have nrm_s1: "normal s1"
+ from `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2` 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)"
@@ -836,16 +837,15 @@
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)
+ 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)
- have G: "prg Env = G" .
- have hyp_e0: "PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)" .
- have hyp_e1_e2: "PROP ?Hyp (In1l (if the_Bool b then e1 else e2))
- s1 s2 (In1 v)" .
+ note G = `prg Env = G`
+ note hyp_e0 = `PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)`
+ note hyp_e1_e2 = `PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)`
from Cond.prems
obtain e1T e2T
where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"
@@ -878,7 +878,7 @@
next
case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Call.prems
obtain eT argsT
where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
@@ -889,26 +889,26 @@
= Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
from wt_e G
have jmp_s1: "?Jmp jmps s1"
by - (rule hyp_e [THEN conjunct1],simp_all)
- have hyp_args: "PROP ?Hyp (In3 args) s1 s2 (In3 vs)" .
+ note hyp_args = `PROP ?Hyp (In3 args) s1 s2 (In3 vs)`
have "abrupt s2 = Some (Jump j)"
proof -
- have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4" .
+ note `G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4`
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 have "s3' = check_method_access G accC statT mode
- \<lparr>name = mn, parTs = pTs\<rparr> a s3" .
+ moreover note `s3' = check_method_access G accC statT mode
+ \<lparr>name = mn, parTs = pTs\<rparr> a s3`
ultimately have "abrupt s3 = Some (Jump j)"
by (cases s3)
(simp add: check_method_access_def abrupt_if_def Let_def)
moreover
- have "s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2" .
+ note `s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2`
ultimately show ?thesis
by (cases s2) (auto simp add: init_lvars_def2)
qed
@@ -920,6 +920,7 @@
thus ?case by simp
next
case (Methd s0 D sig v s1 jmps T Env)
+ from `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
by (rule eval.Methd)
hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
@@ -929,7 +930,7 @@
case (Body s0 D s1 c s2 s3 jmps T Env)
have "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
\<rightarrow> abupd (absorb Ret) s3"
- by (rule eval.Body)
+ by (rule eval.Body) (rule Body)+
hence "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
by (rule Body_no_jump) simp
thus ?case by simp
@@ -938,7 +939,7 @@
thus ?case by (simp add: lvar_def Let_def)
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from wf FVar.prems
obtain statC f where
wt_e: "Env\<turnstile>e\<Colon>-Class statC" and
@@ -955,21 +956,21 @@
thus ?thesis
by simp
qed
- have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
+ note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
{
fix j
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_init: "PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>" .
+ note hyp_init = `PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>`
from G wt_init
have "?Jmp jmps s1"
by - (rule hyp_init [THEN conjunct1],auto)
moreover
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 a)" .
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 a)`
have "abrupt s2 = Some (Jump j)"
proof -
- have "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+ note `s3 = check_field_access G accC statDeclC fn stat a s2'`
with jmp have "abrupt s2' = Some (Jump j)"
by (cases s2')
(simp add: check_field_access_def abrupt_if_def Let_def)
@@ -997,23 +998,23 @@
ultimately show ?case using v by simp
next
case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from AVar.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) simp
- have avar: "(v, s2') = avar G i a s2" .
+ note avar = `(v, s2') = avar G i a s2`
{
fix j
assume jmp: "abrupt s2' = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e1: "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)" .
+ note hyp_e1 = `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)`
from G wt_e1
have "?Jmp jmps s1"
- by - (rule hyp_e1 [THEN conjunct1],auto)
+ by - (rule hyp_e1 [THEN conjunct1], auto)
moreover
- have hyp_e2: "PROP ?Hyp (In1l e2) s1 s2 (In1 i)" .
+ note hyp_e2 = `PROP ?Hyp (In1l e2) s1 s2 (In1 i)`
have "abrupt s2 = Some (Jump j)"
proof -
from avar have "s2' = snd (avar G i a s2)"
@@ -1043,7 +1044,7 @@
case Nil thus ?case by simp
next
case (Cons s0 e v s1 es vs s2 jmps T Env)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
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
@@ -1052,12 +1053,12 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
+ note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
from G wt_e
have "?Jmp jmps s1"
by - (rule hyp_e [THEN conjunct1],simp_all)
moreover
- have hyp_es: "PROP ?Hyp (In3 es) s1 s2 (In3 vs)" .
+ note hyp_es = `PROP ?Hyp (In3 es) s1 s2 (In3 vs)`
ultimately show ?thesis
using wt_e2 G jmp
by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
@@ -1199,7 +1200,7 @@
by auto
moreover
obtain x1 s1 where "f n s = (x1,s1)"
- by (cases "f n s", simp)
+ by (cases "f n s")
ultimately
show ?thesis
using f_ok
@@ -1338,8 +1339,8 @@
then
have s0_s1: "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))" by simp
- have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
- hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
+ from `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
+ have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
by (rule dom_locals_sxalloc_mono)
thus ?case
proof (cases "G,s2\<turnstile>catch C")
@@ -1406,7 +1407,7 @@
qed
next
case (NewC s0 C s1 a s2)
- have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
+ note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
from NewC.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1416,7 +1417,7 @@
finally show ?case by simp
next
case (NewA s0 T s1 e i s2 a s3)
- have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+ note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
from NewA.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1474,8 +1475,7 @@
finally show ?thesis by simp
next
case False
- have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
- with False
+ with `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
have "s2=s1"
by auto
with s0_s1 False
@@ -1497,7 +1497,7 @@
finally show ?case by simp
next
case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
- have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .
+ note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
from Call.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1526,11 +1526,11 @@
also
have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
proof -
- have "s3 =
+ from `s3 =
(if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
abrupt s2 = Some (Jump (Cont l))
- then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)".
- thus ?thesis
+ then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
+ show ?thesis
by simp
qed
finally show ?case by simp
@@ -1551,7 +1551,7 @@
by (simp add: dom_locals_fvar_vvar_mono)
hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s3 \<longrightarrow> ?V_ok)"
by - (intro strip, simp)
- have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+ note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
from FVar.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1690,7 +1690,7 @@
case NewC show ?case by simp
next
case (NewA s0 T s1 e i s2 a s3)
- have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+ note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
proof -
from NewA
@@ -1733,8 +1733,8 @@
also
have "\<dots> \<subseteq> dom (locals (store s2))"
proof -
- have "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
- else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
+ note `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+ else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
thus ?thesis
by (rule dom_locals_eval_mono_elim)
qed
@@ -1757,7 +1757,7 @@
case Acc thus ?case by simp
next
case (Ass s0 va w f s1 e v s2)
- have nrm_ass_s2: "normal (assign f v s2)" .
+ note nrm_ass_s2 = `normal (assign f v s2)`
hence nrm_s2: "normal s2"
by (cases s2, simp add: assign_def Let_def)
with Ass.hyps
@@ -1848,16 +1848,16 @@
case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
have nrm_s2: "normal s2"
proof -
- have "normal ((set_lvars (locals (snd s2))) s4)" .
- hence normal_s4: "normal s4" by simp
+ from `normal ((set_lvars (locals (snd s2))) s4)`
+ have normal_s4: "normal s4" by simp
hence "normal s3'" using Call.hyps
by - (erule eval_no_abrupt_lemma [rule_format])
- moreover have
- "s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3".
+ moreover note
+ `s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3`
ultimately have "normal s3"
by (cases s3) (simp add: check_method_access_def Let_def)
moreover
- have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .
+ note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
ultimately show "normal s2"
by (cases s2) (simp add: init_lvars_def2)
qed
@@ -1888,11 +1888,11 @@
case LVar thus ?case by simp
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
- have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
- have avar: "(v, s2') = fvar statDeclC stat fn a s2" .
+ note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
+ note avar = `(v, s2') = fvar statDeclC stat fn a s2`
have nrm_s2: "normal s2"
proof -
- have "normal s3" .
+ note `normal s3`
with s3 have "normal s2'"
by (cases s2') (simp add: check_field_access_def Let_def)
with avar show "normal s2"
@@ -1917,11 +1917,10 @@
by simp
next
case (AVar s0 e1 a s1 e2 i s2 v s2')
- have avar: "(v, s2') = avar G i a s2" .
+ note avar = `(v, s2') = avar G i a s2`
have nrm_s2: "normal s2"
proof -
- have "normal s2'" .
- with avar
+ from avar and `normal s2'`
show ?thesis by (cases s2) (simp add: avar_def2)
qed
with AVar.hyps
@@ -2024,19 +2023,19 @@
case Inst hence False by simp thus ?case ..
next
case (Lit val c v s0 s)
- have "constVal (Lit val) = Some c" .
+ note `constVal (Lit val) = Some c`
moreover
- have "G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s" .
- then obtain "v=val" and "normal s"
+ from `G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s`
+ obtain "v=val" and "normal s"
by cases simp
ultimately show "v=c \<and> normal s" by simp
next
case (UnOp unop e c v s0 s)
- have const: "constVal (UnOp unop e) = Some c" .
+ note const = `constVal (UnOp unop e) = Some c`
then obtain ce where ce: "constVal e = Some ce" by simp
- have "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s" .
- then obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
- v: "v = eval_unop unop ve"
+ from `G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s`
+ obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
+ v: "v = eval_unop unop ve"
by cases simp
from ce ve
obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
@@ -2048,13 +2047,13 @@
show ?case ..
next
case (BinOp binop e1 e2 c v s0 s)
- have const: "constVal (BinOp binop e1 e2) = Some c" .
+ note const = `constVal (BinOp binop e1 e2) = Some c`
then obtain c1 c2 where c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2" and
c: "c = eval_binop binop c1 c2"
by simp
- have "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s" .
- then obtain v1 s1 v2
+ from `G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s`
+ obtain v1 s1 v2
where v1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
v2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
else In1r Skip)\<succ>\<rightarrow> (In1 v2, s)" and
@@ -2095,14 +2094,14 @@
case Ass hence False by simp thus ?case ..
next
case (Cond b e1 e2 c v s0 s)
- have c: "constVal (b ? e1 : e2) = Some c" .
+ note c = `constVal (b ? e1 : e2) = Some c`
then obtain cb c1 c2 where
cb: "constVal b = Some cb" and
c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2"
by (auto split: bool.splits)
- have "G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s" .
- then obtain vb s1
+ from `G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s`
+ obtain vb s1
where vb: "G\<turnstile>Norm s0 \<midarrow>b-\<succ>vb\<rightarrow> s1" and
eval_v: "G\<turnstile>s1 \<midarrow>(if the_Bool vb then e1 else e2)-\<succ>v\<rightarrow> s"
by cases simp
@@ -2172,25 +2171,28 @@
case Inst hence False by simp thus ?case ..
next
case (Lit v c)
- have "constVal (Lit v) = Some c" .
- hence "c=v" by simp
- moreover have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
- hence "typeof empty_dt v = Some (PrimT Boolean)"
+ from `constVal (Lit v) = Some c`
+ have "c=v" by simp
+ moreover
+ from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+ have "typeof empty_dt v = Some (PrimT Boolean)"
by cases simp
ultimately show ?case by simp
next
case (UnOp unop e c)
- have "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
- hence "Boolean = unop_type unop" by cases simp
- moreover have "constVal (UnOp unop e) = Some c" .
- then obtain ce where "c = eval_unop unop ce" by auto
+ from `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
+ have "Boolean = unop_type unop" by cases simp
+ moreover
+ from `constVal (UnOp unop e) = Some c`
+ obtain ce where "c = eval_unop unop ce" by auto
ultimately show ?case by (simp add: eval_unop_type)
next
case (BinOp binop e1 e2 c)
- have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
- hence "Boolean = binop_type binop" by cases simp
- moreover have "constVal (BinOp binop e1 e2) = Some c" .
- then obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
+ from `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
+ have "Boolean = binop_type binop" by cases simp
+ moreover
+ from `constVal (BinOp binop e1 e2) = Some c`
+ obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
ultimately show ?case by (simp add: eval_binop_type)
next
case Super hence False by simp thus ?case ..
@@ -2200,13 +2202,13 @@
case Ass hence False by simp thus ?case ..
next
case (Cond b e1 e2 c)
- have c: "constVal (b ? e1 : e2) = Some c" .
+ note c = `constVal (b ? e1 : e2) = Some c`
then obtain cb c1 c2 where
cb: "constVal b = Some cb" and
c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2"
by (auto split: bool.splits)
- have wt: "Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean" .
+ note wt = `Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean`
then
obtain T1 T2
where "Env\<turnstile>b\<Colon>-PrimT Boolean" and
@@ -2255,28 +2257,28 @@
case Abrupt thus ?case by simp
next
case (NewC s0 C s1 a s2)
- have "Env\<turnstile>NewC C\<Colon>-PrimT Boolean" .
- hence False
+ from `Env\<turnstile>NewC C\<Colon>-PrimT Boolean`
+ have False
by cases simp
thus ?case ..
next
case (NewA s0 T s1 e i s2 a s3)
- have "Env\<turnstile>New T[e]\<Colon>-PrimT Boolean" .
- hence False
+ from `Env\<turnstile>New T[e]\<Colon>-PrimT Boolean`
+ have False
by cases simp
thus ?case ..
next
case (Cast s0 e b s1 s2 T)
- have s2: "s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1".
+ note s2 = `s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1`
have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
proof -
- have "normal s2" .
- with s2 have "normal s1"
+ from s2 and `normal s2`
+ have "normal s1"
by (cases s1) simp
moreover
- have "Env\<turnstile>Cast T e\<Colon>-PrimT Boolean" .
- hence "Env\<turnstile>e\<Colon>- PrimT Boolean"
- by (cases) (auto dest: cast_Boolean2)
+ from `Env\<turnstile>Cast T e\<Colon>-PrimT Boolean`
+ have "Env\<turnstile>e\<Colon>- PrimT Boolean"
+ by cases (auto dest: cast_Boolean2)
ultimately show ?thesis
by (rule Cast.hyps [elim_format]) auto
qed
@@ -2286,15 +2288,15 @@
finally show ?case by simp
next
case (Inst s0 e v s1 b T)
- have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and "normal s1" .
- hence "assignsE e \<subseteq> dom (locals (store s1))"
+ from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1` and `normal s1`
+ have "assignsE e \<subseteq> dom (locals (store s1))"
by (rule assignsE_good_approx)
thus ?case
by simp
next
case (Lit s v)
- have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
- hence "typeof empty_dt v = Some (PrimT Boolean)"
+ from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+ 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)
@@ -2302,13 +2304,13 @@
by simp
next
case (UnOp s0 e v s1 unop)
- have bool: "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
+ note bool = `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
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
- have "normal s1" .
+ note `normal s1`
moreover note bool_e
ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
by (rule UnOp.hyps [elim_format]) auto
@@ -2324,8 +2326,8 @@
next
case (Some c)
moreover
- have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
- hence "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1"
+ from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+ 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"
@@ -2342,7 +2344,7 @@
qed
next
case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
- have bool: "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
+ note bool = `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
show ?case
proof (cases "constVal (BinOp binop e1 e2)")
case (Some c)
@@ -2395,8 +2397,8 @@
with condAnd
have need_second: "need_second_arg binop v1"
by (simp add: need_second_arg_def)
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ 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
@@ -2415,8 +2417,8 @@
obtain "the_Bool v1=True" and "the_Bool v2 = False"
by (simp add: need_second_arg_def)
moreover
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ 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
@@ -2443,8 +2445,8 @@
with condOr
have need_second: "need_second_arg binop v1"
by (simp add: need_second_arg_def)
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ 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
@@ -2463,8 +2465,8 @@
obtain "the_Bool v1=False" and "the_Bool v2 = True"
by (simp add: need_second_arg_def)
moreover
- have "normal s2" .
- hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ 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
@@ -2486,12 +2488,12 @@
qed
next
case False
- have "\<not> (binop = CondAnd \<or> binop = CondOr)" .
+ note `\<not> (binop = CondAnd \<or> binop = CondOr)`
from BinOp.hyps
have
- "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
+ "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
by - (rule eval.BinOp)
- moreover have "normal s2" .
+ moreover note `normal s2`
ultimately
have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
by (rule assignsE_good_approx)
@@ -2502,38 +2504,37 @@
qed
next
case Super
- have "Env\<turnstile>Super\<Colon>-PrimT Boolean" .
+ note `Env\<turnstile>Super\<Colon>-PrimT Boolean`
hence False
by cases simp
thus ?case ..
next
case (Acc s0 va v f s1)
- have "prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1" and "normal s1".
- hence "assignsV va \<subseteq> dom (locals (store s1))"
+ from `prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1` and `normal s1`
+ 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 have "normal (assign f v s2)" .
+ moreover note `normal (assign f v s2)`
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)
- have "Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean" .
- then obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
- wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
+ from `Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean`
+ obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
+ wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
by cases (auto dest: widen_Boolean2)
- have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
+ note eval_e0 = `prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
proof -
note eval_e0
moreover
- have "normal s2" .
- with Cond.hyps have "normal s1"
+ from Cond.hyps and `normal s2` have "normal s1"
by - (erule eval_no_abrupt_lemma [rule_format],simp)
ultimately
have "assignsE e0 \<subseteq> dom (locals (store s1))"
@@ -2551,15 +2552,15 @@
\<subseteq> dom (locals (store s2))"
proof (cases "the_Bool b")
case True
- have "normal s2" .
- hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ 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
- have "normal s2" .
- hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
+ from `normal s2`
+ 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
@@ -2578,9 +2579,9 @@
show ?thesis
proof (cases "the_Bool c")
case True
- have "normal s2" .
- hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
- by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True)
+ from `normal s2`
+ 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)
@@ -2588,9 +2589,9 @@
by simp
next
case False
- have "normal s2" .
- hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
- by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False)
+ from `normal s2`
+ 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)
@@ -2606,6 +2607,7 @@
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 `normal ((set_lvars (locals (snd s2))) s4)`
by (rule assignsE_good_approx)
thus ?case by simp
next
@@ -2695,7 +2697,7 @@
(rule Expr.hyps, auto)
next
case (Lab s0 c s1 j Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Lab.prems
obtain C l where
da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
@@ -2754,7 +2756,7 @@
ultimately show ?case by (intro conjI)
next
case (Comp s0 c1 s1 c2 s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Comp.prems
obtain C1 C2
where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
@@ -2765,7 +2767,7 @@
obtain wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases) simp
- have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) s1`
with wt_c1 da_c1 G
obtain nrm_c1: "?NormalAssigned s1 C1" and
brk_c1: "?BreakAssigned (Norm s0) s1 C1" and
@@ -2780,7 +2782,7 @@
nrm_c2: "nrm C2 \<subseteq> nrm C2'" and
brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In1r c2) s1 s2" .
+ note `PROP ?Hyp (In1r c2) s1 s2`
with wt_c2 da_c2' G
obtain nrm_c2': "?NormalAssigned s2 C2'" and
brk_c2': "?BreakAssigned s1 s2 C2'" and
@@ -2800,8 +2802,8 @@
ultimately show ?thesis by (intro conjI)
next
case False
- have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
- with False have eq_s1_s2: "s2=s1" by auto
+ with `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
+ have eq_s1_s2: "s2=s1" by auto
with False have "?NormalAssigned s2 A" by blast
moreover
have "?BreakAssigned (Norm s0) s2 A"
@@ -2827,16 +2829,16 @@
qed
next
case (If s0 e b s1 c1 c2 s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
from If.prems
obtain E C1 C2 where
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
- da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
+ da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
\<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
- da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
+ da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state)))
\<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
- A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
+ A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
by (elim da_elim_cases)
from If.prems
obtain
@@ -2923,15 +2925,15 @@
moreover
have "s2 = s1"
proof -
- have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
- with abr show ?thesis
+ from abr and `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
+ show ?thesis
by (cases s1) simp
qed
ultimately show ?thesis by simp
qed
next
case (Loop s0 e b s1 c s2 l s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
by (simp (no_asm_simp))
from Loop.prems
@@ -3137,7 +3139,7 @@
ultimately show ?case by (intro conjI)
next
case (Throw s0 e a s1 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Throw.prems obtain E where
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"
by (elim da_elim_cases)
@@ -3167,7 +3169,7 @@
ultimately show ?case by (intro conjI)
next
case (Try s0 c1 s1 s2 C vn c2 s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Try.prems obtain C1 C2 where
da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
da_c2:
@@ -3181,7 +3183,7 @@
by (elim wt_elim_cases)
have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G
by (simp (no_asm_simp))
- have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) s1`
with wt_c1 da_c1 G
obtain nrm_C1: "?NormalAssigned s1 C1" and
brk_C1: "?BreakAssigned (Norm s0) s1 C1" and
@@ -3239,8 +3241,8 @@
have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn})
\<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
proof -
- have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
- hence "dom (locals (store ((Norm s0)::state)))
+ from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+ have "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
also
@@ -3314,7 +3316,7 @@
qed
next
case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Fin.prems obtain C1 C2 where
da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
@@ -3325,7 +3327,7 @@
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)" .
+ note `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)`
with wt_c1 da_C1 G
obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and
brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and
@@ -3345,7 +3347,7 @@
nrm_C2': "nrm C2 \<subseteq> nrm C2'" and
brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
by (rule da_weakenE) simp
- have "PROP ?Hyp (In1r c2) (Norm s1) s2" .
+ note `PROP ?Hyp (In1r c2) (Norm s1) s2`
with wt_c2 da_C2' G
obtain nrmAss_C2': "?NormalAssigned s2 C2'" and
brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and
@@ -3360,12 +3362,12 @@
show ?thesis
using that resAss_s2' by simp
qed
- have s3: "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+ note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
have s1_s2: "dom (locals s1) \<subseteq> dom (locals (store s2))"
proof -
- have "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
- thus ?thesis
+ from `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`
+ show ?thesis
by (rule dom_locals_eval_mono_elim) simp
qed
@@ -3455,7 +3457,7 @@
by simp
moreover have "dom (locals (store ((Norm s1)::state)))
\<subseteq> dom (locals (store s2))"
- by (rule dom_locals_eval_mono_elim)
+ 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
@@ -3473,7 +3475,7 @@
ultimately show ?case by (intro conjI)
next
case (Init C c s0 s3 s1 s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Init.hyps
have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"
apply (simp only: G)
@@ -3483,8 +3485,7 @@
apply (simp only: if_False )
apply (elim conjE,intro conjI,assumption+,simp)
done (* auto or simp alone always do too much *)
- have "the (class G C) = c" .
- with Init.prems
+ from Init.prems and `the (class G C) = c`
have c: "class G C = Some c"
by (elim wt_elim_cases) auto
from Init.prems obtain
@@ -3529,7 +3530,7 @@
qed
next
case (NewC s0 C s1 a s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from NewC.prems
obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"
"brk A = (\<lambda> l. UNIV)"
@@ -3540,10 +3541,10 @@
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"
proof -
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule NewC.hyps)
also
have "\<dots> \<subseteq> dom (locals (store s2))"
- by (rule dom_locals_halloc_mono)
+ by (rule dom_locals_halloc_mono) (rule NewC.hyps)
finally show ?thesis .
qed
with A have "?NormalAssigned s2 A"
@@ -3553,7 +3554,7 @@
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"
- by (simp only: G) (rule eval.NewC)
+ unfolding G by (rule eval.NewC NewC.hyps)+
from NewC.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -3569,7 +3570,7 @@
ultimately show ?case by (intro conjI)
next
case (NewA s0 elT s1 e i s2 a s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from NewA.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
@@ -3577,15 +3578,15 @@
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')
- have halloc:"G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3".
+ note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3`
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule NewA.hyps)
with da_e obtain A' where
da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"
and nrm_A_A': "nrm A \<subseteq> nrm A'"
and brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"
by (rule da_weakenE) simp
- have "PROP ?Hyp (In1l e) s1 s2" .
+ note `PROP ?Hyp (In1l e) s1 s2`
with wt_size da_e' G obtain
nrmAss_A': "?NormalAssigned s2 A'" and
brkAss_A': "?BreakAssigned s1 s2 A'"
@@ -3596,7 +3597,7 @@
\<subseteq> dom (locals (store (abupd (check_neg i) s2)))"
by (simp)
also have "\<dots> \<subseteq> dom (locals (store s3))"
- by (rule dom_locals_halloc_mono)
+ by (rule dom_locals_halloc_mono) (rule NewA.hyps)
finally show ?thesis .
qed
have "?NormalAssigned s3 A"
@@ -3618,7 +3619,7 @@
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"
- by (simp only: G) (rule eval.NewA)
+ unfolding G by (rule eval.NewA NewA.hyps)+
from NewA.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -3634,19 +3635,19 @@
ultimately show ?case by (intro conjI)
next
case (Cast s0 e v s1 s2 cT Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Cast.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
from Cast.prems obtain eT where
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with wt_e da_e G obtain
nrmAss_A: "?NormalAssigned s1 A" and
brkAss_A: "?BreakAssigned (Norm s0) s1 A"
by simp
- have s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .
+ note s2 = `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
by simp
have "?NormalAssigned s2 A"
@@ -3663,7 +3664,7 @@
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"
- by (simp only: G) (rule eval.Cast)
+ unfolding G by (rule eval.Cast Cast.hyps)+
from Cast.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -3679,14 +3680,14 @@
ultimately show ?case by (intro conjI)
next
case (Inst s0 e v s1 b iT Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Inst.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
from Inst.prems obtain eT where
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with wt_e da_e G obtain
"?NormalAssigned s1 A" and
"?BreakAssigned (Norm s0) s1 A" and
@@ -3701,14 +3702,14 @@
thus ?case by simp
next
case (UnOp s0 e v s1 unop Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from UnOp.prems obtain
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
from UnOp.prems obtain eT where
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with wt_e da_e G obtain
"?NormalAssigned s1 A" and
"?BreakAssigned (Norm s0) s1 A" and
@@ -3717,19 +3718,19 @@
thus ?case by (intro conjI)
next
case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A)
- have G: "prg Env = G".
+ note G = `prg Env = G`
from BinOp.hyps
have
- eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
+ eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
by (simp only: G) (rule eval.BinOp)
have s0_s1: "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule BinOp)
also have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule BinOp)
finally
have s0_s2: "dom (locals (store ((Norm s0)::state)))
- \<subseteq> dom (locals (store s2))" .
+ \<subseteq> dom (locals (store s2))" .
from BinOp.prems obtain e1T e2T
where wt_e1: "Env\<turnstile>e1\<Colon>-e1T"
and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
@@ -3740,7 +3741,7 @@
proof
assume normal_s2: "normal s2"
have normal_s1: "normal s1"
- by (rule eval_no_abrupt_lemma [rule_format])
+ by (rule eval_no_abrupt_lemma [rule_format]) (rule BinOp.hyps, rule normal_s2)
show "nrm A \<subseteq> dom (locals (store s2))"
proof (cases "binop=CondAnd")
case True
@@ -3832,7 +3833,7 @@
where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"
and da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"
by (elim da_elim_cases) (simp_all add: notAndOr)
- have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l e1) (Norm s0) s1`
with wt_e1 da_e1 G normal_s1
obtain "?NormalAssigned s1 E1"
by simp
@@ -3883,20 +3884,21 @@
from Acc.prems
have "nrm A = dom (locals (store ((Norm s0)::state)))"
by (simp only: vn) (elim da_elim_cases,simp_all)
- moreover have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
- hence "s1=Norm s0"
+ moreover
+ from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
+ have "s1=Norm s0"
by (simp only: vn) (elim eval_elim_cases,simp)
ultimately show ?thesis by simp
next
case False
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from False Acc.prems
have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"
by (elim da_elim_cases) simp_all
from Acc.prems obtain vT where
wt_v: "Env\<turnstile>v\<Colon>=vT"
by (elim wt_elim_cases)
- have "PROP ?Hyp (In2 v) (Norm s0) s1" .
+ note `PROP ?Hyp (In2 v) (Norm s0) s1`
with wt_v da_v G obtain
"?NormalAssigned s1 A" and
"?BreakAssigned (Norm s0) s1 A" and
@@ -3906,7 +3908,7 @@
qed
next
case (Ass s0 var w upd s1 e v s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Ass.prems obtain varT eT where
wt_var: "Env\<turnstile>var\<Colon>=varT" and
wt_e: "Env\<turnstile>e\<Colon>-eT"
@@ -3920,9 +3922,9 @@
have normal_s2: "normal s2"
by (cases s2) (simp add: assign_def Let_def)
hence normal_s1: "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- have hyp_var: "PROP ?Hyp (In2 var) (Norm s0) s1" .
- have hyp_e: "PROP ?Hyp (In1l e) s1 s2" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Ass.hyps)
+ note hyp_var = `PROP ?Hyp (In2 var) (Norm s0) s1`
+ note hyp_e = `PROP ?Hyp (In1l e) s1 s2`
show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"
proof (cases "\<exists> vn. var = LVar vn")
case True
@@ -3937,9 +3939,9 @@
proof -
have "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
- with da_e show ?thesis
- by (rule da_weakenE)
+ by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
+ with da_e show thesis
+ by (rule da_weakenE) (rule that)
qed
from G eval_var vn
have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1"
@@ -4004,7 +4006,7 @@
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)
+ by (simp only: G) (rule eval.Ass Ass.hyps)+
from Ass.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4020,7 +4022,7 @@
ultimately show ?case by (intro conjI)
next
case (Cond s0 e0 b s1 e1 e2 v s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s2 A"
proof
assume normal_s2: "normal s2"
@@ -4033,7 +4035,7 @@
assigns_if False (e0 ? e1 : e2))"
by (elim da_elim_cases) simp_all
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"
- by (simp only: G) (rule eval.Cond)
+ unfolding G by (rule eval.Cond Cond.hyps)+
from eval
have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"
by (rule dom_locals_eval_mono_elim)
@@ -4075,10 +4077,11 @@
by (elim wt_elim_cases)
have s0_s1: "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
- have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" by (simp only: G)
+ by (rule dom_locals_eval_mono_elim) (rule Cond.hyps)
+ have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
+ unfolding G by (rule Cond.hyps)
have normal_s1: "normal s1"
- by (rule eval_no_abrupt_lemma [rule_format])
+ by (rule eval_no_abrupt_lemma [rule_format]) (rule Cond.hyps, rule normal_s2)
show ?thesis
proof (cases "the_Bool b")
case True
@@ -4126,7 +4129,7 @@
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"
- by (simp only: G) (rule eval.Cond)
+ unfolding G by (rule eval.Cond Cond.hyps)+
from Cond.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4142,7 +4145,7 @@
next
case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned (restore_lvars s2 s4) A"
proof
assume normal_restore_lvars: "normal (restore_lvars s2 s4)"
@@ -4156,23 +4159,23 @@
wt_e: "Env\<turnstile>e\<Colon>-eT" and
wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
by (elim wt_elim_cases)
- have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2" .
- have s3': "s3' = check_method_access G accC statT mode
- \<lparr>name=mn,parTs=pTs\<rparr> a s3" .
+ note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2`
+ note s3' = `s3' = check_method_access G accC statT mode
+ \<lparr>name=mn,parTs=pTs\<rparr> a s3`
have normal_s2: "normal s2"
proof -
from normal_restore_lvars have "normal s4"
by simp
then have "normal s3'"
- by - (rule eval_no_abrupt_lemma [rule_format])
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
with s3' have "normal s3"
by (cases s3) (simp add: check_method_access_def Let_def)
with s3 show "normal s2"
by (cases s2) (simp add: init_lvars_def Let_def)
qed
then have normal_s1: "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
+ note `PROP ?Hyp (In1l e) (Norm s0) s1`
with da_e wt_e G normal_s1
have "nrm E \<subseteq> dom (locals (store s1))"
by simp
@@ -4180,7 +4183,7 @@
da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In3 args) s1 s2" .
+ note `PROP ?Hyp (In3 args) s1 s2`
with da_args' wt_args G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4197,7 +4200,7 @@
proof -
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v
\<rightarrow> (restore_lvars s2 s4)"
- by (simp only: G) (rule eval.Call)
+ unfolding G by (rule eval.Call Call)+
from Call.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4214,7 +4217,7 @@
ultimately show ?case by (intro conjI)
next
case (Methd s0 D sig v s1 Env T A)
- have G: "prg Env = G".
+ note G = `prg Env = G`
from Methd.prems obtain m where
m: "methd (prg Env) D sig = Some m" and
da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state))))
@@ -4224,7 +4227,7 @@
isCls: "is_class (prg Env) D" and
wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"
by - (erule wt_elim_cases,simp)
- have "PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1" .
+ note `PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1`
moreover
from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"
using isCls m G by (simp add: body_def2)
@@ -4236,13 +4239,13 @@
using G by simp
next
case (Body s0 D s1 c s2 s3 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
from Body.prems
have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"
by (elim da_elim_cases) simp
have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
\<rightarrow>abupd (absorb Ret) s3"
- by (simp only: G) (rule eval.Body)
+ unfolding G by (rule eval.Body Body.hyps)+
hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
by (simp only: nrm_A) (rule dom_locals_eval_mono_elim)
hence "?NormalAssigned (abupd (absorb Ret) s3) A"
@@ -4262,14 +4265,14 @@
thus ?case by simp
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s3 A"
proof
assume normal_s3: "normal s3"
show "nrm A \<subseteq> dom (locals (store s3))"
proof -
- have fvar: "(v, s2') = fvar statDeclC stat fn a s2" and
- s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+ note fvar = `(v, s2') = fvar statDeclC stat fn a s2` and
+ s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
from FVar.prems
have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
by (elim da_elim_cases)
@@ -4278,7 +4281,7 @@
by (elim wt_elim_cases)
have "(dom (locals (store ((Norm s0)::state))))
\<subseteq> dom (locals (store s1))"
- by (rule dom_locals_eval_mono_elim)
+ by (rule dom_locals_eval_mono_elim) (rule FVar.hyps)
with da_e obtain A' where
da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
@@ -4292,7 +4295,7 @@
show "normal s2"
by (cases s2) (simp add: fvar_def2)
qed
- have "PROP ?Hyp (In1l e) s1 s2" .
+ note `PROP ?Hyp (In1l e) s1 s2`
with da_e' wt_e G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4318,7 +4321,7 @@
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)
+ 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
@@ -4334,13 +4337,13 @@
ultimately show ?case by (intro conjI)
next
case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s2' A"
proof
assume normal_s2': "normal s2'"
show "nrm A \<subseteq> dom (locals (store s2'))"
proof -
- have avar: "(v, s2') = avar G i a s2" .
+ note avar = `(v, s2') = avar G i a s2`
from AVar.prems obtain E1 where
da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and
da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"
@@ -4353,15 +4356,15 @@
have normal_s2: "normal s2"
by (cases s2) (simp add: avar_def2)
hence "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- moreover have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule AVar, rule normal_s2)
+ moreover note `PROP ?Hyp (In1l e1) (Norm s0) s1`
ultimately have "nrm E1 \<subseteq> dom (locals (store s1))"
using da_e1 wt_e1 G by simp
with da_e2 obtain A' where
da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In1l e2) s1 s2" .
+ note `PROP ?Hyp (In1l e2) s1 s2`
with da_e2' wt_e2 G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4384,7 +4387,7 @@
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'"
- by (simp only: G v) (rule eval.AVar)
+ unfolding G v by (rule eval.AVar AVar.hyps)+
from AVar.prems
obtain T' where "T=Inl T'"
by (elim wt_elim_cases) simp
@@ -4406,7 +4409,7 @@
thus ?case by simp
next
case (Cons s0 e v s1 es vs s2 Env T A)
- have G: "prg Env = G" .
+ note G = `prg Env = G`
have "?NormalAssigned s2 A"
proof
assume normal_s2: "normal s2"
@@ -4421,15 +4424,15 @@
wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"
by (elim wt_elim_cases)
have "normal s1"
- by - (rule eval_no_abrupt_lemma [rule_format])
- moreover have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+ by - (rule eval_no_abrupt_lemma [rule_format], rule Cons.hyps, rule normal_s2)
+ moreover note `PROP ?Hyp (In1l e) (Norm s0) s1`
ultimately have "nrm E \<subseteq> dom (locals (store s1))"
using da_e wt_e G by simp
with da_es obtain A' where
da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
nrm_A_A': "nrm A \<subseteq> nrm A'"
by (rule da_weakenE) iprover
- have "PROP ?Hyp (In3 es) s1 s2" .
+ note `PROP ?Hyp (In3 es) s1 s2`
with da_es' wt_es G normal_s2
have "nrm A' \<subseteq> dom (locals (store s2))"
by simp
@@ -4442,7 +4445,7 @@
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"
- by (simp only: G) (rule eval.Cons)
+ unfolding G by (rule eval.Cons Cons.hyps)+
from Cons.prems
obtain T' where "T=Inr T'"
by (elim wt_elim_cases) simp