--- a/src/HOL/Bali/Evaln.thy Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/Evaln.thy Thu Oct 31 18:27:10 2002 +0100
@@ -7,13 +7,26 @@
statements
*}
-theory Evaln = Eval + TypeSafe:
+theory Evaln = TypeSafe:
+
text {*
-Variant of eval relation with counter for bounded recursive depth.
-Evaln omits the technical accessibility tests @{term check_field_access}
-and @{term check_method_access}, since we proved the absence of errors for
-wellformed programs.
+Variant of @{term eval} relation with counter for bounded recursive depth.
+In principal @{term evaln} could replace @{term eval}.
+
+Validity of the axiomatic semantics builds on @{term evaln}.
+For recursive method calls the axiomatic semantics rule assumes the method ok
+to derive a proof for the body. To prove the method rule sound we need to
+perform induction on the recursion depth.
+For the completeness proof of the axiomatic semantics the notion of the most
+general formula is used. The most general formula right now builds on the
+ordinary evaluation relation @{term eval}.
+So sometimes we have to switch between @{term evaln} and @{term eval} and vice
+versa. To make
+this switch easy @{term evaln} also does all the technical accessibility tests
+@{term check_field_access} and @{term check_method_access} like @{term eval}.
+If it would omit them @{term evaln} and @{term eval} would only be equivalent
+for welltyped, and definitely assigned terms.
*}
consts
@@ -63,18 +76,19 @@
inductive "evaln G" intros
-(* propagation of abrupt completion *)
+--{* propagation of abrupt completion *}
Abrupt: "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
-(* evaluation of variables *)
+--{* evaluation of variables *}
LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
- FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s2;
- (v,s2') = fvar statDeclC stat fn a' s2\<rbrakk> \<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
+ FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
+ (v,s2') = fvar statDeclC stat fn a s2;
+ s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
+ G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2;
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
@@ -83,7 +97,7 @@
-(* evaluation of expressions *)
+--{* evaluation of expressions *}
NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
@@ -127,19 +141,25 @@
Call:
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2;
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
- G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2
- \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
+ s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
+ s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
+ G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4
+ \<rbrakk>
\<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
+ G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
- Body: "\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
+ Body: "\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
+ 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)\<rbrakk>\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Body D c
- -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
+ -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s3"
-(* evaluation of expression lists *)
+--{* evaluation of expression lists *}
Nil:
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
@@ -149,7 +169,7 @@
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
-(* execution of statements *)
+--{* execution of statements *}
Skip: "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
@@ -168,13 +188,13 @@
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
- if normal s1 \<and> the_Bool b
+ if the_Bool b
then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and>
G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
else s3 = s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
- Do: "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
+ Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
@@ -185,8 +205,11 @@
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
- G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
+ G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
+ s3=(if (\<exists> err. x1=Some (Error err))
+ then (x1,s1)
+ else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
+ G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
Init: "\<lbrakk>the (class G C) = c;
if inited C (globs s0) then s3 = Norm s0
@@ -202,12 +225,17 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
+ not_None_eq [simp del]
+ split_paired_All [simp del] split_paired_Ex [simp del]
+ML_setup {*
+simpset_ref() := simpset() delloop "split_all_tac"
+*}
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
inductive_cases evaln_elim_cases:
"G\<turnstile>(Some xc, s) \<midarrow>t \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<midarrow>n\<rightarrow> xs'"
- "G\<turnstile>Norm s \<midarrow>In1r (Do j) \<succ>\<midarrow>n\<rightarrow> xs'"
+ "G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<midarrow>n\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<midarrow>n\<rightarrow> xs'"
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<midarrow>n\<rightarrow> vs'"
@@ -236,9 +264,15 @@
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> xs'"
+ "G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<midarrow>n\<rightarrow> xs'"
+
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
-
+ not_None_eq [simp]
+ split_paired_All [simp] split_paired_Ex [simp]
+ML_setup {*
+simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
+*}
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>
(case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)
| In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
@@ -248,6 +282,13 @@
apply auto
done
+text {* The following simplification procedures set up the proper injections of
+ terms and their corresponding values in the evaluation relation:
+ E.g. an expression
+ (injection @{term In1l} into terms) always evaluates to ordinary values
+ (injection @{term In1} into generalised values @{term vals}).
+*}
+
ML_setup {*
fun enf nam inj rhs =
let
@@ -390,663 +431,47 @@
apply auto
done
-(* ##### FIXME: To WellType *)
-lemma wt_elim_BinOp:
- "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
- \<And>T1 T2 T3.
- \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
- E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
- T = Inl (PrimT (binop_type binop))\<rbrakk>
- \<Longrightarrow> P\<rbrakk>
-\<Longrightarrow> P"
-apply (erule wt_elim_cases)
-apply (cases b)
-apply auto
-done
+
+
section {* evaln implies eval *}
+
lemma evaln_eval:
- assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
- wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
- conf_s0: "s0\<Colon>\<preceq>(G, L)" and
- wf: "wf_prog G"
-
+ assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
-proof -
- from evaln
- show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
- \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
- (is "PROP ?EqEval s0 s1 t v")
- proof (induct)
- case Abrupt
- show ?case by (rule eval.Abrupt)
- next
- case LVar
- show ?case by (rule eval.LVar)
- next
- case (FVar a accC' e fn n s0 s1 s2 s2' stat statDeclC v L accC T)
- have eval_initn: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1" .
- have eval_en: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" .
- have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
- have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
- have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In2 ({accC',statDeclC,stat}e..fn)\<Colon>T" .
- then obtain statC f where
- wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
- accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
- stat: "stat=is_static f" and
- accC': "accC'=accC" and
- T: "T=(Inl (type f))"
- by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
- from wf wt_e
- have iscls_statC: "is_class G statC"
- by (auto dest: ty_expr_is_type type_is_class)
- with wf accfield
- have iscls_statDeclC: "is_class G statDeclC"
- by (auto dest!: accfield_fields dest: fields_declC)
- then
- have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
- by simp
- from conf_s0 wt_init
- have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
- by (rule hyp_init)
- with wt_init conf_s0 wf
- have conf_s1: "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: exec_ts)
- with hyp_e wt_e
- have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
- by blast
- with wf conf_s1 wt_e
- obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
- conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
- by (auto dest!: eval_type_sound)
- obtain s3 where
- check: "s3 = check_field_access G accC statDeclC fn stat a s2'"
- by simp
- from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check wf
- have eq_s3_s2': "s3=s2'"
- by (auto dest!: error_free_field_access)
- with eval_init eval_e fvar check accC'
- show "G\<turnstile>Norm s0 \<midarrow>{accC',statDeclC,stat}e..fn=\<succ>v\<rightarrow> s2'"
- by (auto intro: eval.FVar)
- next
- case AVar
- with wf show ?case
- apply -
- apply (erule wt_elim_cases)
- apply (blast intro!: eval.AVar dest: eval_type_sound)
- done
- next
- case NewC
- with wf show ?case
- apply -
- apply (erule wt_elim_cases)
- apply (blast intro!: eval.NewC dest: eval_type_sound is_acc_classD)
- done
- next
- case (NewA T a e i n s0 s1 s2 s3 L accC Ta)
- have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
- have hyp_size: "PROP ?EqEval s1 s2 (In1l e) (In1 i)" .
- have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
- then obtain
- wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
- wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer"
- by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- from this wt_init
- have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1"
- by (rule hyp_init)
- moreover
- from eval_init wt_init wf conf_s0
- have "s1\<Colon>\<preceq>(G, L)"
- by (auto dest: eval_type_sound)
- from this wt_size
- have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2"
- by (rule hyp_size)
- moreover note NewA
- ultimately show ?case
- by (blast intro!: eval.NewA)
- next
- case Cast
- with wf show ?case
- by - (erule wt_elim_cases, rule eval.Cast,auto dest: eval_type_sound)
- next
- case Inst
- with wf show ?case
- by - (erule wt_elim_cases, rule eval.Inst,auto dest: eval_type_sound)
- next
- case Lit
- show ?case by (rule eval.Lit)
- next
- case UnOp
- with wf show ?case
- by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
- next
- case BinOp
- with wf show ?case
- by - (erule wt_elim_BinOp, blast intro!: eval.BinOp dest: eval_type_sound)
- next
- case Super
- show ?case by (rule eval.Super)
- next
- case Acc
- then show ?case
- by - (erule wt_elim_cases, rule eval.Acc,auto dest: eval_type_sound)
- next
- case Ass
- with wf show ?case
- by - (erule wt_elim_cases, blast intro!: eval.Ass dest: eval_type_sound)
- next
- case (Cond b e0 e1 e2 n s0 s1 s2 v L accC T)
- have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
- have hyp_if: "PROP ?EqEval s1 s2
- (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
- then obtain T1 T2 statT where
- wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
- wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
- wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and
- statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2 \<or> G\<turnstile>T2\<preceq>T1 \<and> statT = T1" and
- T : "T=Inl statT"
- by (rule wt_elim_cases) auto
- from conf_s0 wt_e0
- have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
- by (rule hyp_e0)
- moreover
- from eval_e0 conf_s0 wf wt_e0
- have "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- with wt_e1 wt_e2 statT hyp_if
- have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2"
- by (cases "the_Bool b") auto
- ultimately
- show ?case
- by (rule eval.Cond)
- next
- case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT
- v vs L accC T)
- txt {* Repeats large parts of the type soundness proof. One should factor
- out some lemmata about the relations and conformance of @{text
- s2}, @{text s3} and @{text s3'} *}
- have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
- have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
- have invDeclC: "invDeclC
- = invocation_declclass G mode (store s2) a' statT
- \<lparr>name = mn, parTs = pTs'\<rparr>" .
- let ?InitLvars
- = "init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2"
- obtain s3 s3' where
- init_lvars: "s3 =
- init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" and
- check: "s3' =
- check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
- by simp
- have evaln_methd:
- "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
- have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
- have hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
- have hyp_methd: "PROP ?EqEval ?InitLvars s4
- (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
- \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
- from wt obtain pTs statDeclT statM where
- wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
- wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
- statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr>
- = {((statDeclT,statM),pTs')}" and
- mode: "mode = invmode statM e" and
- T: "T =Inl (resTy statM)" and
- eq_accC_accC': "accC=accC'"
- by (rule wt_elim_cases) fastsimp+
- from conf_s0 wt_e hyp_e
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
- by blast
- with wf conf_s0 wt_e
- obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
- conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT"
- by (auto dest!: eval_type_sound)
- from conf_s1 wt_args hyp_args
- have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
- by blast
- with wt_args conf_s1 wf
- obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
- conf_args: "normal s2
- \<Longrightarrow> list_all2 (conf G (store s2)) vs pTs"
- by (auto dest!: eval_type_sound)
- from statM
- obtain
- statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
- pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
- by (blast dest: max_spec2mheads)
- from check
- have eq_store_s3'_s3: "store s3'=store s3"
- by (cases s3) (simp add: check_method_access_def Let_def)
- obtain invC
- where invC: "invC = invocation_class mode (store s2) a' statT"
- by simp
- with init_lvars
- have invC': "invC = (invocation_class mode (store s3) a' statT)"
- by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
- show "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)
- -\<succ>v\<rightarrow> (set_lvars (locals (store s2))) s4"
- proof (cases "normal s2")
- case False
- with 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 False check
- have eq_s3'_s3: "s3'=s3"
- by (auto simp add: check_method_access_def Let_def)
- moreover
- from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
- obtain "s4=s3'"
- "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
- by auto
- moreover note False
- ultimately have
- "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
- by (auto)
- from eval_e eval_args invDeclC init_lvars check this
- show ?thesis
- by (rule eval.Call)
- next
- case True
- note normal_s2 = True
- with eval_args
- have normal_s1: "normal s1"
- by (cases "normal s1") auto
- with conf_a' eval_args
- have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
- by (auto dest: eval_gext intro: conf_gext)
- show ?thesis
- proof (cases "a'=Null \<longrightarrow> is_static statM")
- case False
- then obtain not_static: "\<not> is_static statM" and Null: "a'=Null"
- by blast
- with normal_s2 init_lvars mode
- obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" 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 np check
- have eq_s3'_s3: "s3'=s3"
- by (auto simp add: check_method_access_def Let_def)
- moreover
- from eq_s3'_s3 np evaln_methd init_lvars
- obtain "s4=s3'"
- "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
- by auto
- moreover note np
- ultimately have
- "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
- by (auto)
- from eval_e eval_args invDeclC init_lvars check this
- show ?thesis
- by (rule eval.Call)
- next
- case True
- with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
- by (auto dest!: Null_staticD)
- with conf_s2 conf_a'_s2 wf invC
- have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
- by (cases s2) (auto intro: DynT_propI)
- with wt_e statM' invC mode wf
- obtain dynM where
- dynM: "dynlookup G statT invC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
- acc_dynM: "G \<turnstile>Methd \<lparr>name=mn,parTs=pTs'\<rparr> dynM
- in invC dyn_accessible_from accC"
- by (force dest!: call_access_ok)
- with invC' check eq_accC_accC'
- have eq_s3'_s3: "s3'=s3"
- by (auto simp add: check_method_access_def Let_def)
- from dynT_prop wf wt_e statM' mode invC invDeclC dynM
- obtain
- wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
- dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
- iscls_invDeclC: "is_class G invDeclC" and
- invDeclC': "invDeclC = declclass dynM" and
- invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
- is_static_eq: "is_static dynM = is_static statM" and
- involved_classes_prop:
- "(if invmode statM e = IntVir
- then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
- else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
- (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
- statDeclT = ClassT invDeclC)"
- by (auto dest: DynT_mheadsD)
- obtain L' where
- L':"L'=(\<lambda> k.
- (case k of
- EName e
- \<Rightarrow> (case e of
- VNam v
- \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
- (pars (mthd dynM)[\<mapsto>]pTs')) v
- | Res \<Rightarrow> Some (resTy dynM))
- | This \<Rightarrow> if is_static statM
- then None else Some (Class invDeclC)))"
- by simp
- from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
- wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
- have conf_s3: "s3\<Colon>\<preceq>(G,L')"
- apply -
- (*FIXME confomrs_init_lvars should be
- adjusted to be more directy applicable *)
- apply (drule conforms_init_lvars [of G invDeclC
- "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2"
- L statT invC a' "(statDeclT,statM)" e])
- apply (rule wf)
- apply (rule conf_args,assumption)
- apply (simp add: pTs_widen)
- apply (cases s2,simp)
- apply (rule dynM')
- apply (force dest: ty_expr_is_type)
- apply (rule invC_widen)
- apply (force intro: conf_gext dest: eval_gext)
- apply simp
- apply simp
- apply (simp add: invC)
- apply (simp add: invDeclC)
- apply (force dest: wf_mdeclD1 is_acc_typeD)
- apply (cases s2, simp add: L' init_lvars
- cong add: lname.case_cong ename.case_cong)
- done
- from is_static_eq wf_dynM L'
- obtain mthdT where
- "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
- \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
- mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
- by - (drule wf_mdecl_bodyD,
- auto simp: cong add: lname.case_cong ename.case_cong)
- with dynM' iscls_invDeclC invDeclC'
- have
- "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
- \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
- by (auto intro: wt.Methd)
- with conf_s3 hyp_methd init_lvars eq_s3'_s3
- have "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
- by auto
- from eval_e eval_args invDeclC init_lvars check this
- show ?thesis
- by (rule eval.Call)
- qed
- qed
- next
- case Methd
- with wf show ?case
- by - (erule wt_elim_cases, rule eval.Methd,
- auto dest: eval_type_sound simp add: body_def2)
- next
- case Body
- with wf show ?case
- by - (erule wt_elim_cases, blast intro!: eval.Body dest: eval_type_sound)
- next
- case Nil
- show ?case by (rule eval.Nil)
- next
- case Cons
- with wf show ?case
- by - (erule wt_elim_cases, blast intro!: eval.Cons dest: eval_type_sound)
- next
- case Skip
- show ?case by (rule eval.Skip)
- next
- case Expr
- with wf show ?case
- by - (erule wt_elim_cases, rule eval.Expr,auto dest: eval_type_sound)
- next
- case Lab
- with wf show ?case
- by - (erule wt_elim_cases, rule eval.Lab,auto dest: eval_type_sound)
- next
- case Comp
- with wf show ?case
- by - (erule wt_elim_cases, blast intro!: eval.Comp dest: eval_type_sound)
- next
- case (If b c1 c2 e n s0 s1 s2 L accC T)
- have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
- have hyp_then_else:
- "PROP ?EqEval s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
- then obtain
- wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
- wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
- by (rule wt_elim_cases) (auto split add: split_if)
- from conf_s0 wt_e
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
- by (rule hyp_e)
- moreover
- from eval_e wt_e conf_s0 wf
- have "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- from this wt_then_else
- have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2"
- by (rule hyp_then_else)
- ultimately
- show ?case
- by (rule eval.If)
- next
- case (Loop b c e l n s0 s1 s2 s3 L accC T)
- have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
- then 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 (rule wt_elim_cases) (blast)
- from conf_s0 wt_e
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
- by (rule hyp_e)
- moreover
- from eval_e wt_e conf_s0 wf
- have conf_s1: "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- have "if normal s1 \<and> the_Bool b
- then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and>
- G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
- else s3 = s1"
- proof (cases "normal s1 \<and> the_Bool b")
- case True
- from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
- by (auto)
- from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
- s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
- by (auto)
- from conf_s1 wt_c
- have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
- by (rule hyp_c)
- moreover
- from eval_c conf_s1 wt_c wf
- have "s2\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- then
- have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
- by (cases s2) (auto intro: conforms_absorb)
- from this and wt
- have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
- by (rule hyp_w)
- moreover note True
- ultimately
- show ?thesis
- by simp
- next
- case False
- with Loop have "s3 = s1" by simp
- with False
- show ?thesis
- by auto
- qed
- ultimately
- show ?case
- by (rule eval.Loop)
- next
- case Do
- show ?case by (rule eval.Do)
- next
- case Throw
- with wf show ?case
- by - (erule wt_elim_cases, rule eval.Throw,auto dest: eval_type_sound)
- next
- case (Try c1 c2 n s0 s1 s2 s3 catchC vn L accC T)
- have hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
- have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
- have wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
- then obtain
- wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
- wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
- by (rule wt_elim_cases) (auto)
- from conf_s0 wt_c1
- have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
- by (rule hyp_c1)
- moreover
- have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
- moreover
- from eval_c1 wt_c1 conf_s0 wf
- have "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- with sxalloc wf
- have conf_s2: "s2\<Colon>\<preceq>(G, L)"
- by (auto dest: sxalloc_type_sound split: option.splits)
- have "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
- proof (cases "G,s2\<turnstile>catch catchC")
- case True
- note Catch = this
- with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
- by auto
- show ?thesis
- proof (cases "normal s1")
- case True
- with sxalloc wf
- have eq_s2_s1: "s2=s1"
- by (auto dest: sxalloc_type_sound split: option.splits)
- with True
- have "\<not> G,s2\<turnstile>catch catchC"
- by (simp add: catch_def)
- with Catch show ?thesis
- by (contradiction)
- next
- case False
- with sxalloc wf
- obtain a
- where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
- by (auto dest!: sxalloc_type_sound split: option.splits)
- with Catch
- have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
- by (cases s2) simp
- with xcpt_s2 conf_s2 wf
- have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
- by (auto dest: Try_lemma)
- from this wt_c2
- have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3"
- by (auto intro: hyp_c2)
- with Catch
- show ?thesis
- by simp
- qed
- next
- case False
- with Try
- have "s3=s2"
- by simp
- with False
- show ?thesis
- by simp
- qed
- ultimately
- show ?case
- by (rule eval.Try)
- next
- case (Fin c1 c2 n s0 s1 s2 x1 L accC T)
- have hyp_c1: "PROP ?EqEval (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
- have hyp_c2: "PROP ?EqEval (Norm s1) (s2) (In1r c2) \<diamondsuit>" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
- then obtain
- wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
- wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
- by (rule wt_elim_cases) blast
- from conf_s0 wt_c1
- have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)"
- by (rule hyp_c1)
- with wf wt_c1 conf_s0
- obtain conf_s1: "Norm s1\<Colon>\<preceq>(G, L)" and
- error_free_s1: "error_free (x1,s1)"
- by (auto dest!: eval_type_sound intro: conforms_NormI)
- from conf_s1 wt_c2
- have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2"
- by (rule hyp_c2)
- with eval_c1 error_free_s1
- show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
- by (auto intro: eval.Fin simp add: error_free_def)
- next
- case (Init C c n s0 s1 s2 s3 L accC T)
- have cls: "the (class G C) = c" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
- with cls
- have cls_C: "class G C = Some c"
- by - (erule wt_elim_cases,auto)
- have "if inited C (globs s0) then s3 = Norm s0
- else (G\<turnstile>Norm (init_class_obj G C s0)
- \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
- G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)"
- proof (cases "inited C (globs s0)")
- case True
- with Init have "s3 = Norm s0"
- by simp
- with True show ?thesis
- by simp
- next
- case False
- with Init
- obtain
- hyp_init_super:
- "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
- (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
- and
- hyp_init_c:
- "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
- s3: "s3 = (set_lvars (locals (store s1))) s2"
- by (simp only: if_False)
- from conf_s0 wf cls_C False
- have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
- by (auto dest: conforms_init_class_obj)
- moreover
- from wf cls_C
- have wt_init_super:
- "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
- \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
- by (cases "C=Object")
- (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
- ultimately
- have eval_init_super:
- "G\<turnstile>Norm ((init_class_obj G C) s0)
- \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
- by (rule hyp_init_super)
- with conf_s0' wt_init_super wf
- have "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- then
- have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
- by (cases s1) (auto dest: conforms_set_locals )
- with wf cls_C
- have eval_init_c: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2"
- by (auto intro!: hyp_init_c dest: wf_prog_cdecl wf_cdecl_wt_init)
- from False eval_init_super eval_init_c s3
- show ?thesis
- by simp
- qed
- with cls show ?case
- by (rule eval.Init)
- qed
-qed
+using evaln
+proof (induct)
+ case (Loop b c e l n s0 s1 s2 s3)
+ have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
+ moreover
+ have "if the_Bool b
+ then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and>
+ G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
+ else s3 = s1"
+ using Loop.hyps by simp
+ ultimately show ?case by (rule eval.Loop)
+next
+ case (Try c1 c2 n s0 s1 s2 s3 C vn)
+ have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
+ moreover
+ have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
+ moreover
+ have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
+ using Try.hyps by simp
+ ultimately show ?case by (rule eval.Try)
+next
+ case (Init C c n s0 s1 s2 s3)
+ have "the (class G C) = c".
+ moreover
+ have "if inited C (globs s0)
+ then s3 = Norm s0
+ else G\<turnstile>Norm ((init_class_obj G C) s0)
+ \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
+ G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
+ s3 = (set_lvars (locals (store s1))) s2"
+ using Init.hyps by simp
+ ultimately show ?case by (rule eval.Init)
+qed (rule eval.intros,(assumption+ | assumption?))+
lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
apply (frule Suc_le_D)
@@ -1068,8 +493,13 @@
lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2\<rbrakk> \<Longrightarrow>
G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1 \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2"
-apply (fast intro: le_maxI1 le_maxI2)
-done
+by (fast intro: le_maxI1 le_maxI2)
+
+corollary evaln_max2E [consumes 2]:
+ "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2;
+ \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1;G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2 \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
+by (drule (1) evaln_max2) simp
+
lemma evaln_max3:
"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> ws3\<rbrakk> \<Longrightarrow>
@@ -1080,6 +510,16 @@
apply (fast intro!: le_maxI1 le_maxI2)
done
+corollary evaln_max3E:
+"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> ws3;
+ \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1;
+ G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2;
+ G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3
+ \<rbrakk> \<Longrightarrow> P
+ \<rbrakk> \<Longrightarrow> P"
+by (drule (2) evaln_max3) simp
+
+
lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
proof -
have "n2 \<le> max n2 n3"
@@ -1102,755 +542,328 @@
show ?thesis .
qed
+ML {*
+Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
+*}
+
section {* eval implies evaln *}
lemma eval_evaln:
- assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
- wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
- conf_s0: "s0\<Colon>\<preceq>(G, L)" and
- wf: "wf_prog G"
+ assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
shows "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
-proof -
- from eval
- show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
- \<Longrightarrow> \<exists> n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
- (is "PROP ?EqEval s0 s1 t v")
- proof (induct)
- case (Abrupt s t xc L accC T)
- obtain n where
- "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
- by (rules intro: evaln.Abrupt)
- then show ?case ..
- next
- case Skip
- show ?case by (blast intro: evaln.Skip)
- next
- case (Expr e s0 s1 v L accC T)
- then obtain n where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules elim!: wt_elim_cases)
- then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
- by (rule evaln.Expr)
- then show ?case ..
- next
- case (Lab c l s0 s1 L accC T)
- then obtain n where
- "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
- by (rules elim!: wt_elim_cases)
- then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
- by (rule evaln.Lab)
- then show ?case ..
- next
- case (Comp c1 c2 s0 s1 s2 L accC T)
- with wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
- by (blast elim!: wt_elim_cases dest: eval_type_sound)
- then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
- by (blast intro: evaln.Comp dest: evaln_max2 )
- then show ?case ..
- next
- case (If b c1 c2 e s0 s1 s2 L accC T)
- with wf obtain
- "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
- "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
- by (cases "the_Bool b") (auto elim!: wt_elim_cases)
- with If wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
- by (blast dest: eval_type_sound)
- then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
- by (blast intro: evaln.If dest: evaln_max2)
- then show ?case ..
- next
- case (Loop b c e l s0 s1 s2 s3 L accC T)
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
- have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
- then 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 (rule wt_elim_cases) (blast)
- from conf_s0 wt_e
- obtain n1 where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
- by (rules dest: hyp_e)
- moreover
- from eval_e wt_e conf_s0 wf
- have conf_s1: "s1\<Colon>\<preceq>(G, L)"
- by (rules dest: eval_type_sound)
- obtain n2 where
- "if normal s1 \<and> the_Bool b
- then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and>
- G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
- else s3 = s1"
- proof (cases "normal s1 \<and> the_Bool b")
- case True
- from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
- by (auto)
- from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
- s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
- by (auto)
- from Loop True have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
- by simp
- from conf_s1 wt_c
- obtain m1 where
- evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>m1\<rightarrow> s2"
- by (rules dest: hyp_c)
- moreover
- from eval_c conf_s1 wt_c wf
- have "s2\<Colon>\<preceq>(G, L)"
- by (rules dest: eval_type_sound)
- then
- have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
- by (cases s2) (auto intro: conforms_absorb)
- from this and wt
- obtain m2 where
- "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<midarrow>m2\<rightarrow> s3"
- by (blast dest: hyp_w)
- moreover note True and that
- ultimately show ?thesis
- by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
- next
- case False
- with Loop have "s3 = s1"
- by simp
- with False that
- show ?thesis
- by auto
- qed
- ultimately
- have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
- apply -
- apply (rule evaln.Loop)
- apply (rules intro: evaln_nonstrict intro: le_maxI1)
+using eval
+proof (induct)
+ case (Abrupt s t xc)
+ obtain n where
+ "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
+ by (rules intro: evaln.Abrupt)
+ then show ?case ..
+next
+ case Skip
+ show ?case by (blast intro: evaln.Skip)
+next
+ case (Expr e s0 s1 v)
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
+ by (rule evaln.Expr)
+ then show ?case ..
+next
+ case (Lab c l s0 s1)
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
+ by (rule evaln.Lab)
+ then show ?case ..
+next
+ case (Comp c1 c2 s0 s1 s2)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
+ by (rules)
+ then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
+ by (blast intro: evaln.Comp dest: evaln_max2 )
+ then show ?case ..
+next
+ case (If b c1 c2 e s0 s1 s2)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
+ by (rules)
+ then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
+ by (blast intro: evaln.If dest: evaln_max2)
+ then show ?case ..
+next
+ case (Loop b c e l s0 s1 s2 s3)
+ from Loop.hyps obtain n1 where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
+ by (rules)
+ moreover from Loop.hyps obtain n2 where
+ "if the_Bool b
+ then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and>
+ G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
+ else s3 = s1"
+ by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
+ apply -
+ apply (rule evaln.Loop)
+ apply (rules intro: evaln_nonstrict intro: le_maxI1)
- apply (auto intro: evaln_nonstrict intro: le_maxI2)
- done
- then show ?case ..
- next
- case (Do j s L accC T)
- have "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
- by (rule evaln.Do)
- then show ?case ..
- next
- case (Throw a e s0 s1 L accC T)
- then obtain n where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
- by (rules elim!: wt_elim_cases)
- then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
- by (rule evaln.Throw)
- then show ?case ..
- next
- case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
- have hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
- have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
- then obtain
- wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
- wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
- by (rule wt_elim_cases) (auto)
- from conf_s0 wt_c1
- obtain n1 where
- "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
- by (blast dest: hyp_c1)
- moreover
- have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
- moreover
- from eval_c1 wt_c1 conf_s0 wf
- have "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- with sxalloc wf
- have conf_s2: "s2\<Colon>\<preceq>(G, L)"
- by (auto dest: sxalloc_type_sound split: option.splits)
- obtain n2 where
- "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
- proof (cases "G,s2\<turnstile>catch catchC")
- case True
- note Catch = this
- with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
- by auto
- show ?thesis
- proof (cases "normal s1")
- case True
- with sxalloc wf
- have eq_s2_s1: "s2=s1"
- by (auto dest: sxalloc_type_sound split: option.splits)
- with True
- have "\<not> G,s2\<turnstile>catch catchC"
- by (simp add: catch_def)
- with Catch show ?thesis
- by (contradiction)
- next
- case False
- with sxalloc wf
- obtain a
- where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
- by (auto dest!: sxalloc_type_sound split: option.splits)
- with Catch
- have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
- by (cases s2) simp
- with xcpt_s2 conf_s2 wf
- have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
- by (auto dest: Try_lemma)
- (* FIXME extract lemma for this conformance, also useful for
- eval_type_sound and evaln_eval *)
- from this wt_c2
- obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
- by (auto dest: hyp_c2)
- with True that
- show ?thesis
- by simp
- qed
- next
- case False
- with Try
- have "s3=s2"
- by simp
- with False and that
- show ?thesis
- by simp
- qed
- ultimately
- have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
- by (auto intro!: evaln.Try le_maxI1 le_maxI2)
- then show ?case ..
- next
- case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
- have s3: "s3 = (if \<exists>err. x1 = Some (Error err)
- then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
- from Fin wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
- "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" and
- error_free_s1: "error_free (x1,s1)"
- by (blast elim!: wt_elim_cases
- dest: eval_type_sound intro: conforms_NormI)
- then have
- "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
- by (blast intro: evaln.Fin dest: evaln_max2)
- with error_free_s1 s3
- show "\<exists>n. G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
- by (auto simp add: error_free_def)
- next
- case (Init C c s0 s1 s2 s3 L accC T)
- have cls: "the (class G C) = c" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
- with cls
- have cls_C: "class G C = Some c"
- by - (erule wt_elim_cases,auto)
- obtain n where
+ apply (auto intro: evaln_nonstrict intro: le_maxI2)
+ done
+ then show ?case ..
+next
+ case (Jmp j s)
+ have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
+ by (rule evaln.Jmp)
+ then show ?case ..
+next
+ case (Throw a e s0 s1)
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
+ by (rule evaln.Throw)
+ then show ?case ..
+next
+ case (Try catchC c1 c2 s0 s1 s2 s3 vn)
+ from Try.hyps obtain n1 where
+ "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
+ by (rules)
+ moreover
+ have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
+ moreover
+ from Try.hyps obtain n2 where
+ "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
+ by fastsimp
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
+ by (auto intro!: evaln.Try le_maxI1 le_maxI2)
+ then show ?case ..
+next
+ case (Fin c1 c2 s0 s1 s2 s3 x1)
+ from Fin obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
+ "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
+ by rules
+ moreover
+ have s3: "s3 = (if \<exists>err. x1 = Some (Error err)
+ then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+ ultimately
+ have
+ "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
+ by (blast intro: evaln.Fin dest: evaln_max2)
+ then show ?case ..
+next
+ case (Init C c s0 s1 s2 s3)
+ have cls: "the (class G C) = c" .
+ moreover from Init.hyps obtain n where
"if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
s3 = restore_lvars s1 s2)"
- proof (cases "inited C (globs s0)")
- case True
- with Init have "s3 = Norm s0"
- by simp
- with True that show ?thesis
- by simp
- next
- case False
- with Init
- obtain
- hyp_init_super:
- "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
- (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
- and
- hyp_init_c:
- "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
- s3: "s3 = (set_lvars (locals (store s1))) s2" and
- eval_init_super:
- "G\<turnstile>Norm ((init_class_obj G C) s0)
- \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
- by (simp only: if_False)
- from conf_s0 wf cls_C False
- have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
- by (auto dest: conforms_init_class_obj)
- moreover
- from wf cls_C
- have wt_init_super:
- "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
- \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
- by (cases "C=Object")
- (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
- ultimately
- obtain m1 where
- "G\<turnstile>Norm ((init_class_obj G C) s0)
- \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>m1\<rightarrow> s1"
- by (rules dest: hyp_init_super)
- moreover
- from eval_init_super conf_s0' wt_init_super wf
- have "s1\<Colon>\<preceq>(G, L)"
- by (rules dest: eval_type_sound)
- then
- have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
- by (cases s1) (auto dest: conforms_set_locals )
- with wf cls_C
- obtain m2 where
- "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<midarrow>m2\<rightarrow> s2"
- by (blast dest!: hyp_init_c
- dest: wf_prog_cdecl intro!: wf_cdecl_wt_init)
- moreover note s3 and False and that
- ultimately show ?thesis
- by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
- qed
- from cls this have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
- by (rule evaln.Init)
- then show ?case ..
- next
- case (NewC C a s0 s1 s2 L accC T)
- with wf obtain n where
- "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
- by (blast elim!: wt_elim_cases dest: is_acc_classD)
- with NewC
- have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
- by (rules intro: evaln.NewC)
- then show ?case ..
- next
- case (NewA T a e i s0 s1 s2 s3 L accC Ta)
- hence "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>"
- by (auto elim!: wt_elim_cases
- intro!: wt_init_comp_ty dest: is_acc_typeD)
- with NewA wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"
- by (blast elim!: wt_elim_cases dest: eval_type_sound)
- moreover
- have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
- ultimately
- have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
- by (blast intro: evaln.NewA dest: evaln_max2)
- then show ?case ..
- next
- case (Cast castT e s0 s1 s2 v L accC T)
- with wf obtain n where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules elim!: wt_elim_cases)
- moreover
- have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
- ultimately
- have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
- by (rule evaln.Cast)
- then show ?case ..
- next
- case (Inst T b e s0 s1 v L accC T')
- with wf obtain n where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules elim!: wt_elim_cases)
- moreover
- have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
- ultimately
- have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
- by (rule evaln.Inst)
- then show ?case ..
- next
- case (Lit s v L accC T)
- have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
- by (rule evaln.Lit)
- then show ?case ..
- next
- case (UnOp e s0 s1 unop v L accC T)
- with wf obtain n where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rules elim!: wt_elim_cases)
- hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
- by (rule evaln.UnOp)
- then show ?case ..
- next
- case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
- with wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+ by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
+ ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
+ by (rule evaln.Init)
+ then show ?case ..
+next
+ case (NewC C a s0 s1 s2)
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ with NewC
+ have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
+ by (rules intro: evaln.NewC)
+ then show ?case ..
+next
+ case (NewA T a e i s0 s1 s2 s3)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"
+ by (rules)
+ moreover
+ have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
+ by (blast intro: evaln.NewA dest: evaln_max2)
+ then show ?case ..
+next
+ case (Cast castT e s0 s1 s2 v)
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ moreover
+ have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
+ by (rule evaln.Cast)
+ then show ?case ..
+next
+ case (Inst T b e s0 s1 v)
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ moreover
+ have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
+ by (rule evaln.Inst)
+ then show ?case ..
+next
+ case (Lit s v)
+ have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
+ by (rule evaln.Lit)
+ then show ?case ..
+next
+ case (UnOp e s0 s1 unop v )
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
+ by (rule evaln.UnOp)
+ then show ?case ..
+next
+ case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"
- by (blast elim!: wt_elim_BinOp dest: eval_type_sound)
- hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
- \<rightarrow> s2"
- by (blast intro!: evaln.BinOp dest: evaln_max2)
- then show ?case ..
- next
- case (Super s L accC T)
- have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
- by (rule evaln.Super)
- then show ?case ..
- next
- case (Acc f s0 s1 v va L accC T)
- with wf obtain n where
- "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
- by (rules elim!: wt_elim_cases)
- then
- have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
- by (rule evaln.Acc)
- then show ?case ..
- next
- case (Ass e f s0 s1 s2 v var w L accC T)
- with wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"
- by (blast elim!: wt_elim_cases dest: eval_type_sound)
- then
- have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
- by (blast intro: evaln.Ass dest: evaln_max2)
- then show ?case ..
- next
- case (Cond b e0 e1 e2 s0 s1 s2 v L accC T)
- have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
- have hyp_if: "PROP ?EqEval s1 s2
- (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
- then obtain T1 T2 statT where
- wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
- wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
- wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and
- statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2 \<or> G\<turnstile>T2\<preceq>T1 \<and> statT = T1" and
- T : "T=Inl statT"
- by (rule wt_elim_cases) auto
- have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
- from conf_s0 wt_e0
- obtain n1 where
- "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
- by (rules dest: hyp_e0)
- moreover
- from eval_e0 conf_s0 wf wt_e0
- have "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- with wt_e1 wt_e2 statT hyp_if obtain n2 where
- "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
- by (cases "the_Bool b") force+
- ultimately
- have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
- by (blast intro: evaln.Cond dest: evaln_max2)
- then show ?case ..
- next
- case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT
- v vs L accC T)
- (* Repeats large parts of the type soundness proof. One should factor
- out some lemmata about the relations and conformance of s2, s3 and s3'*)
- have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1" .
- have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
- have invDeclC: "invDeclC
- = invocation_declclass G mode (store s2) a' statT
- \<lparr>name = mn, parTs = pTs'\<rparr>" .
- have
- init_lvars: "s3 =
- init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" .
- have
- check: "s3' =
- check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3" .
- have eval_methd:
- "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
- have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
- have hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
- have hyp_methd: "PROP ?EqEval s3' s4
- (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
- \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
- from wt obtain pTs statDeclT statM where
- wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
- wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
- statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr>
- = {((statDeclT,statM),pTs')}" and
- mode: "mode = invmode statM e" and
- T: "T =Inl (resTy statM)" and
- eq_accC_accC': "accC=accC'"
- by (rule wt_elim_cases) fastsimp+
- from conf_s0 wt_e
- obtain n1 where
- evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
- by (rules dest: hyp_e)
- from wf eval_e conf_s0 wt_e
- obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
- conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT"
- by (auto dest!: eval_type_sound)
- from conf_s1 wt_args
- obtain n2 where
- evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
- by (blast dest: hyp_args)
- from wt_args conf_s1 eval_args wf
- obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
- conf_args: "normal s2
- \<Longrightarrow> list_all2 (conf G (store s2)) vs pTs"
- by (auto dest!: eval_type_sound)
- from statM
- obtain
- statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
- pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
- by (blast dest: max_spec2mheads)
- from check
- have eq_store_s3'_s3: "store s3'=store s3"
- by (cases s3) (simp add: check_method_access_def Let_def)
- obtain invC
- where invC: "invC = invocation_class mode (store s2) a' statT"
- by simp
- with init_lvars
- have invC': "invC = (invocation_class mode (store s3) a' statT)"
- by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
- obtain n3 where
- "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>n3\<rightarrow>
- (set_lvars (locals (store s2))) s4"
- proof (cases "normal s2")
- case False
- with 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 False check
- have eq_s3'_s3: "s3'=s3"
- by (auto simp add: check_method_access_def Let_def)
- moreover
- from eq_s3'_s3 False keep_abrupt eval_methd init_lvars
- obtain "s4=s3'"
- "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
- by auto
- moreover note False evaln.Abrupt
- ultimately obtain m where
- "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
- by force
- from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
- have
- "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
- (set_lvars (locals (store s2))) s4"
- by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
- with that show ?thesis
- by rules
- next
- case True
- note normal_s2 = True
- with eval_args
- have normal_s1: "normal s1"
- by (cases "normal s1") auto
- with conf_a' eval_args
- have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
- by (auto dest: eval_gext intro: conf_gext)
- show ?thesis
- proof (cases "a'=Null \<longrightarrow> is_static statM")
- case False
- then obtain not_static: "\<not> is_static statM" and Null: "a'=Null"
- by blast
- with normal_s2 init_lvars mode
- obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" 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 np check
- have eq_s3'_s3: "s3'=s3"
- by (auto simp add: check_method_access_def Let_def)
- moreover
- from eq_s3'_s3 np eval_methd init_lvars
- obtain "s4=s3'"
- "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
- by auto
- moreover note np
- ultimately obtain m where
- "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
- by force
- from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
- have
- "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
+ by (rules)
+ hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
+ \<rightarrow> s2"
+ by (blast intro!: evaln.BinOp dest: evaln_max2)
+ then show ?case ..
+next
+ case (Super s )
+ have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
+ by (rule evaln.Super)
+ then show ?case ..
+next
+ case (Acc f s0 s1 v va)
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
+ by (rules)
+ then
+ have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
+ by (rule evaln.Acc)
+ then show ?case ..
+next
+ case (Ass e f s0 s1 s2 v var w)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"
+ by (rules)
+ then
+ have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
+ by (blast intro: evaln.Ass dest: evaln_max2)
+ then show ?case ..
+next
+ case (Cond b e0 e1 e2 s0 s1 s2 v)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
+ by (rules)
+ then
+ have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
+ by (blast intro: evaln.Cond dest: evaln_max2)
+ then show ?case ..
+next
+ case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT
+ v vs)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
+ by rules
+ moreover
+ have "invDeclC = invocation_declclass G mode (store s2) a' statT
+ \<lparr>name=mn,parTs=pTs'\<rparr>" .
+ moreover
+ have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
+ moreover
+ have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
+ moreover
+ from Call.hyps
+ obtain m where
+ "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
+ by rules
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
(set_lvars (locals (store s2))) s4"
- by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
- with that show ?thesis
- by rules
- next
- case True
- with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
- by (auto dest!: Null_staticD)
- with conf_s2 conf_a'_s2 wf invC
- have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
- by (cases s2) (auto intro: DynT_propI)
- with wt_e statM' invC mode wf
- obtain dynM where
- dynM: "dynlookup G statT invC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
- acc_dynM: "G \<turnstile>Methd \<lparr>name=mn,parTs=pTs'\<rparr> dynM
- in invC dyn_accessible_from accC"
- by (force dest!: call_access_ok)
- with invC' check eq_accC_accC'
- have eq_s3'_s3: "s3'=s3"
- by (auto simp add: check_method_access_def Let_def)
- from dynT_prop wf wt_e statM' mode invC invDeclC dynM
- obtain
- wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
- dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
- iscls_invDeclC: "is_class G invDeclC" and
- invDeclC': "invDeclC = declclass dynM" and
- invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
- is_static_eq: "is_static dynM = is_static statM" and
- involved_classes_prop:
- "(if invmode statM e = IntVir
- then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
- else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
- (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
- statDeclT = ClassT invDeclC)"
- by (auto dest: DynT_mheadsD)
- obtain L' where
- L':"L'=(\<lambda> k.
- (case k of
- EName e
- \<Rightarrow> (case e of
- VNam v
- \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
- (pars (mthd dynM)[\<mapsto>]pTs')) v
- | Res \<Rightarrow> Some (resTy dynM))
- | This \<Rightarrow> if is_static statM
- then None else Some (Class invDeclC)))"
- by simp
- from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
- wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
- have conf_s3: "s3\<Colon>\<preceq>(G,L')"
- apply -
- (*FIXME confomrs_init_lvars should be
- adjusted to be more directy applicable *)
- apply (drule conforms_init_lvars [of G invDeclC
- "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2"
- L statT invC a' "(statDeclT,statM)" e])
- apply (rule wf)
- apply (rule conf_args,assumption)
- apply (simp add: pTs_widen)
- apply (cases s2,simp)
- apply (rule dynM')
- apply (force dest: ty_expr_is_type)
- apply (rule invC_widen)
- apply (force intro: conf_gext dest: eval_gext)
- apply simp
- apply simp
- apply (simp add: invC)
- apply (simp add: invDeclC)
- apply (force dest: wf_mdeclD1 is_acc_typeD)
- apply (cases s2, simp add: L' init_lvars
- cong add: lname.case_cong ename.case_cong)
- done
- with is_static_eq wf_dynM L'
- obtain mthdT where
- "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
- \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT"
- by - (drule wf_mdecl_bodyD,
- auto simp: cong add: lname.case_cong ename.case_cong)
- with dynM' iscls_invDeclC invDeclC'
- have
- "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
- \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
- by (auto intro: wt.Methd)
- with conf_s3 eq_s3'_s3 hyp_methd
- obtain m where
- "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
- by (blast)
- from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
- have
- "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
- (set_lvars (locals (store s2))) s4"
- by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
- with that show ?thesis
- by rules
- qed
- qed
- then show ?case ..
- next
- case (Methd D s0 s1 sig v L accC T)
- then obtain n where
- "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
- by - (erule wt_elim_cases, force simp add: body_def2)
- then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
- by (rule evaln.Methd)
- then show ?case ..
- next
- case (Body D c s0 s1 s2 L accC T)
- with wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
- by (blast elim!: wt_elim_cases dest: eval_type_sound)
- then have
+ by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
+ thus ?case ..
+next
+ case (Methd D s0 s1 sig v )
+ then obtain n where
+ "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
+ by rules
+ then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
+ by (rule evaln.Methd)
+ then show ?case ..
+next
+ case (Body D c s0 s1 s2 s3 )
+ from Body.hyps obtain n1 n2 where
+ evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
+ evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
+ by (rules)
+ moreover
+ have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
+ fst s2 = Some (Jump (Cont l))
+ then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2
+ else s2)".
+ ultimately
+ have
"G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
- \<rightarrow> abupd (absorb Ret) s2"
- by (blast intro: evaln.Body dest: evaln_max2)
- then show ?case ..
- next
- case (LVar s vn L accC T)
- obtain n where
- "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
- by (rules intro: evaln.LVar)
- then show ?case ..
- next
- case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T)
- have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
- have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
- have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
- have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
- have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
- have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
- have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
- have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
- then obtain statC f where
- wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
- accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
- stat: "stat=is_static f" and
- accC': "accC'=accC" and
- T: "T=(Inl (type f))"
- by (rule wt_elim_cases) (fastsimp simp add: member_is_static_simp)
- from wf wt_e
- have iscls_statC: "is_class G statC"
- by (auto dest: ty_expr_is_type type_is_class)
- with wf accfield
- have iscls_statDeclC: "is_class G statDeclC"
- by (auto dest!: accfield_fields dest: fields_declC)
- then
- have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
- by simp
- from conf_s0 wt_init
- obtain n1 where
- evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
- by (rules dest: hyp_init)
- from eval_init wt_init conf_s0 wf
- have conf_s1: "s1\<Colon>\<preceq>(G, L)"
- by (blast dest: eval_type_sound)
- with wt_e
- obtain n2 where
- evaln_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
- by (blast dest: hyp_e)
- from eval_e wf conf_s1 wt_e
- obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
- conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
- by (auto dest!: eval_type_sound)
- from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check wf
- have eq_s3_s2': "s3=s2'"
- by (auto dest!: error_free_field_access)
- with evaln_init evaln_e fvar accC'
- have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
- by (auto intro: evaln.FVar dest: evaln_max2)
- then show ?case ..
- next
- case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T)
- with wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"
- by (blast elim!: wt_elim_cases dest: eval_type_sound)
- moreover
- have "(v, s2') = avar G i a s2" .
- ultimately
- have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
- by (blast intro!: evaln.AVar dest: evaln_max2)
- then show ?case ..
- next
- case (Nil s0 L accC T)
- show ?case by (rules intro: evaln.Nil)
- next
- case (Cons e es s0 s1 s2 v vs L accC T)
- with wf obtain n1 n2 where
- "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
- "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
- by (blast elim!: wt_elim_cases dest: eval_type_sound)
- then
- have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
- by (blast intro!: evaln.Cons dest: evaln_max2)
- then show ?case ..
- qed
+ \<rightarrow> abupd (absorb Ret) s3"
+ by (rules intro: evaln.Body dest: evaln_max2)
+ then show ?case ..
+next
+ case (LVar s vn )
+ obtain n where
+ "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
+ by (rules intro: evaln.LVar)
+ then show ?case ..
+next
+ case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
+ by rules
+ moreover
+ have "s3 = check_field_access G accC statDeclC fn stat a s2'"
+ "(v, s2') = fvar statDeclC stat fn a s2" .
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
+ by (rules intro: evaln.FVar dest: evaln_max2)
+ then show ?case ..
+next
+ case (AVar a e1 e2 i s0 s1 s2 s2' v )
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"
+ by rules
+ moreover
+ have "(v, s2') = avar G i a s2" .
+ ultimately
+ have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
+ by (blast intro!: evaln.AVar dest: evaln_max2)
+ then show ?case ..
+next
+ case (Nil s0)
+ show ?case by (rules intro: evaln.Nil)
+next
+ case (Cons e es s0 s1 s2 v vs)
+ then obtain n1 n2 where
+ "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
+ "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
+ by rules
+ then
+ have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
+ by (blast intro!: evaln.Cons dest: evaln_max2)
+ then show ?case ..
qed
-
+
end