Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
--- a/src/HOL/Bali/AxCompl.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/AxCompl.thy Wed Jul 10 15:07:02 2002 +0200
@@ -467,6 +467,43 @@
apply (auto dest: eval_type_sound)
done
+(* FIXME To TypeSafe *)
+lemma wf_eval_Fin:
+ assumes wf: "wf_prog G" and
+ wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
+ conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
+ eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
+ eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
+ s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
+ shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
+proof -
+ from eval_c1 wt_c1 wf conf_s0
+ have "error_free (x1,s1)"
+ by (auto dest: eval_type_sound)
+ with eval_c1 eval_c2 s3
+ show ?thesis
+ by - (rule eval.Fin, auto simp add: error_free_def)
+qed
+
+text {* For @{text MGFn_Fin} we need the wellformedness of the program to
+switch from the evaln-semantics to the eval-semantics *}
+lemma MGFn_Fin:
+"\<lbrakk>wf_prog G; G,A\<turnstile>{=:n} In1r stmt1\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1r stmt2\<succ> {G\<rightarrow>}\<rbrakk>
+ \<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In1r (stmt1 Finally stmt2)\<succ> {G\<rightarrow>}"
+apply (tactic "wt_conf_prepare_tac 1")
+apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s' \<and> s\<Colon>\<preceq>(G, L))
+\<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
+apply (tactic "forw_hyp_tac 1")
+apply (tactic "clarsimp_tac eval_css 1")
+apply (rule allI)
+apply (tactic "clarsimp_tac eval_css 1")
+apply (tactic "forw_hyp_tac 1")
+apply (tactic {* pair_tac "sb" 1 *})
+apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
+apply (rule wf_eval_Fin)
+apply auto
+done
+
text {* For @{text MGFn_lemma} we need the wellformedness of the program to
switch from the evaln-semantics to the eval-semantics cf. @{text MGFn_call},
@{text MGFn_FVar}*}
@@ -483,14 +520,15 @@
apply (induct_tac "t")
apply (induct_tac "a")
apply fast+
-apply (rule var_expr_stmt.induct)
-(* 28 subgoals *)
-prefer 14 apply fast (* Methd *)
-prefer 13 apply (erule (3) MGFn_Call)
+apply (rule var_expr_stmt.induct)
+(* 34 subgoals *)
+prefer 17 apply fast (* Methd *)
+prefer 16 apply (erule (3) MGFn_Call)
prefer 2 apply (drule MGFn_Init,erule (2) MGFn_FVar)
apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *)
-apply (erule_tac [23] MGFn_Init)
-prefer 18 apply (erule (1) MGFn_Loop)
+apply (erule_tac [29] MGFn_Init)
+prefer 23 apply (erule (1) MGFn_Loop)
+prefer 26 apply (erule (2) MGFn_Fin)
apply (tactic "ALLGOALS compl_prepare_tac")
apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1")
@@ -499,6 +537,8 @@
apply (erule MGFnD [THEN ax_NormalD])
apply (tactic "forw_hyp_eval_Force_tac 1")
+apply (rule ax_derivs.InstInitV)
+
apply (rule ax_derivs.NewC)
apply (erule MGFn_InitD [THEN conseq2])
apply (tactic "eval_Force_tac 1")
@@ -516,6 +556,12 @@
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1")
apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1")
+apply (rule ax_derivs.UnOp, tactic "forw_hyp_eval_Force_tac 1")
+
+apply (rule ax_derivs.BinOp)
+apply (erule MGFnD [THEN ax_NormalD])
+apply (tactic "forw_hyp_eval_Force_tac 1")
+
apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
@@ -541,6 +587,10 @@
apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *})
apply (erule (1) eval.Body)
+apply (rule ax_derivs.InstInitE)
+
+apply (rule ax_derivs.Callee)
+
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1")
@@ -576,14 +626,7 @@
apply (tactic "clarsimp_tac eval_css 1")
apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext])
-apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
-apply (tactic "forw_hyp_eval_Force_tac 1")
-apply (rule allI)
-apply (tactic "forw_hyp_tac 1")
-apply (tactic {* pair_tac "sb" 1 *})
-apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
-apply (drule (1) eval.Fin)
-apply clarsimp
+apply (rule ax_derivs.FinA)
apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1")
--- a/src/HOL/Bali/AxSem.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/AxSem.thy Wed Jul 10 15:07:02 2002 +0200
@@ -536,6 +536,16 @@
Lit: "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
+ UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
+ \<Longrightarrow>
+ G,A\<turnstile>{Normal P} UnOp unop e-\<succ> {Q}"
+
+ BinOp:
+ "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
+ \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} e2-\<succ> {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
+ \<Longrightarrow>
+ G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}"
+
Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
Acc: "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
@@ -583,7 +593,7 @@
Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} .Expr e. {Q}"
- Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb (Break l)) .; Q}\<rbrakk> \<Longrightarrow>
+ Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
@@ -627,6 +637,14 @@
.init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
+-- {* Some dummy rules for the intermediate terms @{text Callee},
+@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep
+semantics.
+*}
+ InstInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
+ InstInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
+ Callee: " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
+ FinA: " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
axioms (** these terms are the same as above, but with generalized typing **)
polymorphic_conseq:
"\<forall>Y s Z . P Y s Z \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'.
@@ -667,9 +685,9 @@
apply (fast intro: ax_derivs.asm)
(*apply (fast intro: ax_derivs.cut) *)
apply (fast intro: ax_derivs.weaken)
-apply (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
-(* 31 subgoals *)
-prefer 16 (* Methd *)
+apply (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
+(* 37 subgoals *)
+prefer 18 (* Methd *)
apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))
THEN_ALL_NEW Blast_tac) *})
@@ -696,7 +714,7 @@
lemma weaken:
"G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
apply (erule ax_derivs.induct)
-(*36 subgoals*)
+(*42 subgoals*)
apply (tactic "ALLGOALS strip_tac")
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
@@ -708,7 +726,7 @@
(*apply (blast intro: ax_derivs.cut) *)
apply (fast intro: ax_derivs.weaken)
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
-(*31 subgoals*)
+(*37 subgoals*)
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))
THEN_ALL_NEW Fast_tac) *})
(*1 subgoal*)
--- a/src/HOL/Bali/AxSound.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/AxSound.thy Wed Jul 10 15:07:02 2002 +0200
@@ -313,17 +313,18 @@
"\<forall>a vs D l. (P' a vs D l \<and> P a vs D l) \<Longrightarrow> \<forall>a vs D l. P a vs D l"
by fast
+
lemmas sound_lemmas = Init_sound Loop_sound Methd_sound
lemma ax_sound2: "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts"
apply (erule ax_derivs.induct)
-prefer 20 (* Call *)
+prefer 22 (* Call *)
apply (erule (1) Call_sound) apply simp apply force apply force
apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW
eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *})
-apply(tactic "COND (has_fewer_prems(30+3)) (ALLGOALS sound_prepare_tac) no_tac")
+apply(tactic "COND (has_fewer_prems(30+9)) (ALLGOALS sound_prepare_tac) no_tac")
(*empty*)
apply fast (* insert *)
@@ -336,7 +337,13 @@
apply (simp (no_asm_use) add: type_ok_def,fast)(* hazard *)
apply force (* Abrupt *)
-(* 25 subgoals *)
+prefer 28 apply (simp add: evaln_InsInitV)
+prefer 28 apply (simp add: evaln_InsInitE)
+prefer 28 apply (simp add: evaln_Callee)
+prefer 28 apply (simp add: evaln_FinA)
+
+(* 27 subgoals *)
+apply (tactic {* sound_elim_tac 1 *})
apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *)
apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset()
delsimps [thm "all_empty"])) *}) (* Done *)
@@ -347,12 +354,11 @@
apply (simp,simp,simp)
apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
apply (tactic "ALLGOALS sound_valid2_tac")
-apply (tactic "TRYALL sound_forw_hyp_tac") (* Cast, Inst, Acc, Expr *)
+apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *)
apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1,
dtac spec], dtac conjunct2, smp_tac 1,
TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *})
-apply (frule_tac [14] x = x1 in conforms_NormI) (* for Fin *)
-
+apply (frule_tac [15] x = x1 in conforms_NormI) (* for Fin *)
(* 15 subgoals *)
(* FVar *)
@@ -383,6 +389,9 @@
apply (rule conjI,blast)
apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def)
+(* BinOp *)
+apply (tactic "sound_forw_hyp_tac 1")
+
(* Ass *)
apply (tactic "sound_forw_hyp_tac 1")
apply (case_tac "aa")
--- a/src/HOL/Bali/Eval.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Eval.thy Wed Jul 10 15:07:02 2002 +0200
@@ -447,6 +447,43 @@
section "evaluation judgments"
+consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
+primrec
+"eval_unop UPlus v = Intg (the_Intg v)"
+"eval_unop UMinus v = Intg (- (the_Intg v))"
+"eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented"
+"eval_unop UNot v = Bool (\<not> the_Bool v)"
+
+consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
+
+
+primrec
+"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
+"eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
+"eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
+"eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
+"eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
+
+-- "Be aware of the explicit coercion of the shift distance to nat"
+"eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))"
+"eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
+"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
+
+"eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))"
+"eval_binop Le v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
+"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
+"eval_binop Ge v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
+
+"eval_binop Eq v1 v2 = Bool (v1=v2)"
+"eval_binop Neq v1 v2 = Bool (v1\<noteq>v2)"
+"eval_binop BitAnd v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+"eval_binop And v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+"eval_binop BitXor v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+"eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
+"eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+"eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+
+
consts
eval :: "prog \<Rightarrow> (state \<times> term \<times> vals \<times> state) set"
halloc:: "prog \<Rightarrow> (state \<times> obj_tag \<times> loc \<times> state) set"
@@ -513,7 +550,6 @@
SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
-
inductive "eval G" intros
(* propagation of abrupt completion *)
@@ -533,7 +569,7 @@
G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
+ G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
(* cf. 14.2 *)
Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
@@ -573,9 +609,12 @@
(* cf. 14.18.2 *)
Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
- G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
-
+ G\<turnstile>Norm s1 \<midarrow>c2\<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\<rightarrow> s3"
(* cf. 12.4.2, 8.5 *)
Init: "\<lbrakk>the (class G C) = c;
if inited C (globs s0) then s3 = Norm s0
@@ -630,8 +669,12 @@
(* cf. 15.7.1 *)
Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
+ UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk>
+ \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
-
+ BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<rightarrow> s2\<rbrakk>
+ \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
+
(* cf. 15.10.2 *)
Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
@@ -666,11 +709,14 @@
Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
-
+ (* The local variables l are just a dummy here. The are only used by
+ the smallstep semantics *)
(* cf. 14.15, 12.4.1 *)
Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
-
+ G\<turnstile>Norm s0 \<midarrow>Body D c
+ -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
+ (* The local variables l are just a dummy here. The are only used by
+ the smallstep semantics *)
(* evaluation of variables *)
(* cf. 15.13.1, 15.7.2 *)
@@ -704,21 +750,24 @@
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
(* Rearrangement of premisses:
-[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
- 17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
- 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
- 27(AVar),22(Call)]
+[0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
+ 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
+ 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
+ 29(AVar),24(Call)]
*)
ML {*
bind_thm ("eval_induct_", rearrange_prems
-[0,1,2,8,4,28,29,25,15,16,
- 17,18,19,3,5,23,24,21,6,
- 7,11,9,13,14,12,20,10,26,
- 27,22] (thm "eval.induct"))
+[0,1,2,8,4,30,31,27,15,16,
+ 17,18,19,20,21,3,5,25,26,23,6,
+ 7,11,9,13,14,12,22,10,28,
+ 29,24] (thm "eval.induct"))
*}
+
+
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
- and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and
+ and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and
+ and and
s2 (* Fin *) and and s2 (* NewC *)]
declare split_if [split del] split_if_asm [split del]
@@ -757,6 +806,8 @@
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> vs'"
+ "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<rightarrow> vs'"
+ "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> vs'"
@@ -802,6 +853,7 @@
apply auto
done
+
ML_setup {*
fun eval_fun nam inj rhs =
let
@@ -827,6 +879,68 @@
declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]
+text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
+used in smallstep semantics, not in the bigstep semantics. So their is no
+valid evaluation of these terms
+*}
+
+
+lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In1l (Callee l e)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
+
+
+lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In1l (InsInitE c e)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
+
+lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In2 (InsInitV c w)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
+
+lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In1r (FinA a c)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
lemma eval_no_abrupt_lemma:
"\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
@@ -909,7 +1023,8 @@
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.If)
-lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
+lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s'
+ \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Methd)
@@ -979,7 +1094,8 @@
*)
lemma eval_Methd:
- "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
+ "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s')
+ \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
apply (case_tac "s")
apply (case_tac "a")
apply clarsimp+
@@ -1025,6 +1141,12 @@
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
by auto
+lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
+ res=the (locals (store s2) Result);
+ s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>
+ G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"
+by (auto elim: eval.Body)
+
lemma unique_eval [rule_format (no_asm)]:
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
apply (case_tac "ws")
@@ -1033,18 +1155,18 @@
apply (erule eval_induct)
apply (tactic {* ALLGOALS (EVERY'
[strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
-(* 29 subgoals *)
-prefer 26 (* Try *)
+(* 31 subgoals *)
+prefer 28 (* Try *)
apply (simp (no_asm_use) only: split add: split_if_asm)
-(* 32 subgoals *)
-prefer 28 (* Init *)
+(* 34 subgoals *)
+prefer 30 (* Init *)
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
-prefer 24 (* While *)
+prefer 26 (* While *)
apply (simp (no_asm_use) only: split add: split_if_asm, blast)
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
apply blast
-(* 31 subgoals *)
+(* 33 subgoals *)
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
done
--- a/src/HOL/Bali/Evaln.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Evaln.thy Wed Jul 10 15:07:02 2002 +0200
@@ -103,6 +103,12 @@
Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
+ UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk>
+ \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
+
+ BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n\<rightarrow> s2\<rbrakk>
+ \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
+
Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
@@ -128,7 +134,8 @@
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>
- G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
+ G\<turnstile>Norm s0 \<midarrow>Body D c
+ -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
(* evaluation of expression lists *)
@@ -148,7 +155,7 @@
G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
+ G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
@@ -203,6 +210,8 @@
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<midarrow>n\<rightarrow> vs'"
+ "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<midarrow>n\<rightarrow> vs'"
+ "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<midarrow>n\<rightarrow> vs'"
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<midarrow>n\<rightarrow> vs'"
@@ -262,6 +271,62 @@
*}
declare evaln_AbruptIs [intro!]
+lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In1l (Callee l e)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
+
+lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In1l (InsInitE c e)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
+
+lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In2 (InsInitV c w)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
+
+lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+ { fix s t v s'
+ assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+ normal: "normal s" and
+ callee: "t=In1r (FinA a c)"
+ then have "False"
+ proof (induct)
+ qed (auto)
+ }
+ then show ?thesis
+ by (cases s') fastsimp
+qed
+
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow>
fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
apply (erule evaln_cases , auto)
@@ -437,6 +502,14 @@
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_cases, blast intro!: eval.BinOp dest: eval_type_sound)
+ next
case Super
show ?case by (rule eval.Super)
next
@@ -494,11 +567,11 @@
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" .
+ "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)".
+ (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" .
@@ -556,7 +629,7 @@
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>))"
+ "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
by auto
moreover note False
ultimately have
@@ -591,7 +664,7 @@
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>))"
+ "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
by auto
moreover note np
ultimately have
@@ -674,7 +747,7 @@
\<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
by - (drule wf_mdecl_bodyD,
- simp cong add: lname.case_cong ename.case_cong)
+ auto simp: cong add: lname.case_cong ename.case_cong)
with dynM' iscls_invDeclC invDeclC'
have
"\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
@@ -873,10 +946,28 @@
show ?case
by (rule eval.Try)
next
- case Fin
- with wf show ?case
- by -(erule wt_elim_cases, blast intro!: eval.Fin
- dest: eval_type_sound intro: conforms_NormI)
+ 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" .
@@ -994,8 +1085,6 @@
show ?thesis .
qed
-text {* *} (* FIXME *)
-
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
@@ -1029,7 +1118,7 @@
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 (Break l)) s1"
+ 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
@@ -1209,16 +1298,22 @@
by (auto intro!: evaln.Try le_maxI1 le_maxI2)
then show ?case ..
next
- case (Fin c1 c2 s0 s1 s2 x1 L accC T)
- with wf obtain n1 n2 where
+ 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"
+ "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)
- then show ?case ..
+ 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" .
@@ -1340,6 +1435,24 @@
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>e2-\<succ>v2\<midarrow>n2\<rightarrow> s2"
+ by (blast elim!: wt_elim_cases 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)
@@ -1414,7 +1527,7 @@
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)".
+ (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" .
@@ -1475,7 +1588,7 @@
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>))"
+ "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
by auto
moreover note False evaln.Abrupt
ultimately obtain m where
@@ -1514,7 +1627,7 @@
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>))"
+ "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
by auto
moreover note np
ultimately obtain m where
@@ -1600,7 +1713,7 @@
"\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
\<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT"
by - (drule wf_mdecl_bodyD,
- simp cong add: lname.case_cong ename.case_cong)
+ auto simp: cong add: lname.case_cong ename.case_cong)
with dynM' iscls_invDeclC invDeclC'
have
"\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
--- a/src/HOL/Bali/ROOT.ML Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/ROOT.ML Wed Jul 10 15:07:02 2002 +0200
@@ -1,3 +1,5 @@
-use_thy "AxExample";
-use_thy "AxSound";
-use_thy "AxCompl";
+
+update_thy "AxExample";
+update_thy "AxSound";
+update_thy "AxCompl";
+update_thy "Trans";
--- a/src/HOL/Bali/State.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/State.thy Wed Jul 10 15:07:02 2002 +0200
@@ -223,13 +223,13 @@
= "(oref , obj) table"
heap
= "(loc , obj) table"
- locals
- = "(lname, val) table" (* local variables *)
+(* locals
+ = "(lname, val) table" *) (* defined in Value.thy local variables *)
translations
"globs" <= (type) "(oref , obj) table"
"heap" <= (type) "(loc , obj) table"
- "locals" <= (type) "(lname, val) table"
+(* "locals" <= (type) "(lname, val) table" *)
datatype st = (* pure state, i.e. contents of all variables *)
st globs locals
@@ -487,18 +487,7 @@
section "abrupt completion"
-datatype xcpt (* exception *)
- = Loc loc (* location of allocated execption object *)
- | Std xname (* intermediate standard exception, see Eval.thy *)
-datatype error
- = AccessViolation (* Access to a member that isn't permitted *)
-
-datatype abrupt (* abrupt completion *)
- = Xcpt xcpt (* exception *)
- | Jump jump (* break, continue, return *)
- | Error error (* runtime errors, we wan't to detect and proof absent
- in welltyped programms *)
consts
the_Xcpt :: "abrupt \<Rightarrow> xcpt"
@@ -511,8 +500,7 @@
primrec "the_Loc (Loc a) = a"
primrec "the_Std (Std x) = x"
-types
- abopt = "abrupt option"
+
constdefs
--- a/src/HOL/Bali/Table.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Table.thy Wed Jul 10 15:07:02 2002 +0200
@@ -41,7 +41,7 @@
syntax
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" (* concrete table *)
-
+
translations
"table_of" == "map_of"
--- a/src/HOL/Bali/Term.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Term.thy Wed Jul 10 15:07:02 2002 +0200
@@ -6,7 +6,7 @@
header {* Java expressions and statements *}
-theory Term = Value:
+theory Term = Value + Table:
text {*
design issues:
@@ -58,6 +58,40 @@
\end{itemize}
*}
+
+
+types locals = "(lname, val) table" (* local variables *)
+
+
+datatype jump
+ = Break label (* break *)
+ | Cont label (* continue *)
+ | Ret (* return from method *)
+
+datatype xcpt (* exception *)
+ = Loc loc (* location of allocated execption object *)
+ | Std xname (* intermediate standard exception, see Eval.thy *)
+
+datatype error
+ = AccessViolation (* Access to a member that isn't permitted *)
+
+datatype abrupt (* abrupt completion *)
+ = Xcpt xcpt (* exception *)
+ | Jump jump (* break, continue, return *)
+ | Error error (* runtime errors, we wan't to detect and proof absent
+ in welltyped programms *)
+types
+ abopt = "abrupt option"
+
+text {* Local variable store and exception.
+Anticipation of State.thy used by smallstep semantics. For a method call,
+we save the local variables of the caller in the term Callee to restore them
+after method return. Also an exception must be restored after the finally
+statement *}
+
+translations
+ "locals" <= (type) "(lname, val) table"
+
datatype inv_mode (* invocation mode for method calls *)
= Static (* static *)
| SuperM (* super *)
@@ -71,71 +105,112 @@
"sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
"sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
-datatype jump
- = Break label (* break *)
- | Cont label (* continue *)
- | Ret (* return from method *)
+-- "function codes for unary operations"
+datatype unop = UPlus -- "+ unary plus"
+ | UMinus -- "- unary minus"
+ | UBitNot -- "~ bitwise NOT"
+ | UNot -- "! logical complement"
+
+-- "function codes for binary operations"
+datatype binop = Mul -- "* multiplication"
+ | Div -- "/ division"
+ | Mod -- "% remainder"
+ | Plus -- "+ addition"
+ | Minus -- "- subtraction"
+ | LShift -- "<< left shift"
+ | RShift -- ">> signed right shift"
+ | RShiftU -- ">>> unsigned right shift"
+ | Less -- "< less than"
+ | Le -- "<= less than or equal"
+ | Greater -- "> greater than"
+ | Ge -- ">= greater than or equal"
+ | Eq -- "== equal"
+ | Neq -- "!= not equal"
+ | BitAnd -- "& bitwise AND"
+ | And -- "& boolean AND"
+ | BitXor -- "^ bitwise Xor"
+ | Xor -- "^ boolean Xor"
+ | BitOr -- "| bitwise Or"
+ | Or -- "| boolean Or"
datatype var
= LVar lname(* local variable (incl. parameters) *)
| FVar qtname qtname bool expr vname
(*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
- | AVar expr expr (* array component *) ("_.[_]"[90,10 ]90)
+ | AVar expr expr (* array component *) ("_.[_]"[90,10 ]90)
+ | InsInitV stmt var (* insertion of initialization before
+ evaluation of var (for smallstep sem.) *)
and expr
- = NewC qtname (* class instance creation *)
- | NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85)
- | Cast ty expr (* type cast *)
- | Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85)
- | Lit val (* literal value, references not allowed *)
- | Super (* special Super keyword *)
- | Acc var (* variable access *)
- | Ass var expr (* variable assign *) ("_:=_" [90,85 ]85)
- | Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80)
- | Call qtname ref_ty inv_mode expr mname "(ty list)" (* method call *)
- "(expr list)" ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
- | Methd qtname sig (* (folded) method (see below) *)
- | Body qtname stmt (* (unfolded) method body *)
+ = NewC qtname (* class instance creation *)
+ | NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85)
+ | Cast ty expr (* type cast *)
+ | Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85)
+ | Lit val (* literal value, references not allowed *)
+ | UnOp unop expr (* unary operation *)
+ | BinOp binop expr expr (* binary operation *)
+
+ | Super (* special Super keyword *)
+ | Acc var (* variable access *)
+ | Ass var expr (* variable assign *) ("_:=_" [90,85 ]85)
+ | Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80)
+ | Call qtname ref_ty inv_mode expr mname "(ty list)"
+ "(expr list)" (* method call *)
+ ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
+ | Methd qtname sig (* (folded) method (see below) *)
+ | Body qtname stmt (* (unfolded) method body *)
+ | InsInitE stmt expr (* insertion of initialization before
+ evaluation of expr (for smallstep sem.) *)
+ | Callee locals expr (* save Callers locals in Callee-Frame
+ (for smallstep semantics) *)
and stmt
- = Skip (* empty statement *)
- | Expr expr (* expression statement *)
- | Lab label stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66)
- (* handles break *)
- | Comp stmt stmt ("_;; _" [ 66,65]65)
- | If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
- | Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70)
- | Do jump (* break, continue, return *)
+ = Skip (* empty statement *)
+ | Expr expr (* expression statement *)
+ | Lab jump stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66)
+ (* handles break *)
+ | Comp stmt stmt ("_;; _" [ 66,65]65)
+ | If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
+ | Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70)
+ | Do jump (* break, continue, return *)
| Throw expr
| TryC stmt
- qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70)
- | Fin stmt stmt ("_ Finally _" [ 79,79]70)
+ qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70)
+ | Fin stmt stmt ("_ Finally _" [ 79,79]70)
+ | FinA abopt stmt (* Save abruption of first statement
+ (for smallstep sem.) *)
| Init qtname (* class initialization *)
text {*
The expressions Methd and Body are artificial program constructs, in the
sense that they are not used to define a concrete Bali program. In the
-evaluation semantic definition they are "generated on the fly" to decompose
-the task to define the behaviour of the Call expression. They are crucial
-for the axiomatic semantics to give a syntactic hook to insert
-some assertions (cf. AxSem.thy, Eval.thy).
-Also the Init statement (to initialize a class on its first use) is inserted
-in various places by the evaluation semantics.
+operational semantic's they are "generated on the fly"
+to decompose the task to define the behaviour of the Call expression.
+They are crucial for the axiomatic semantics to give a syntactic hook to insert
+some assertions (cf. AxSem.thy, Eval.thy).
+The Init statement (to initialize a class on its first use) is
+inserted in various places by the semantics.
+Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
+smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the
+local variables of the caller for method return. So ve avoid modelling a
+frame stack.
+The InsInitV/E terms are only used by the smallstep semantics to model the
+intermediate steps of class-initialisation.
*}
-types "term" = "(expr+stmt, var, expr list) sum3"
+types "term" = "(expr+stmt,var,expr list) sum3"
translations
"sig" <= (type) "mname \<times> ty list"
"var" <= (type) "Term.var"
"expr" <= (type) "Term.expr"
"stmt" <= (type) "Term.stmt"
- "term" <= (type) "(expr+stmt, var, expr list) sum3"
+ "term" <= (type) "(expr+stmt,var,expr list) sum3"
syntax
this :: expr
- LAcc :: "vname \<Rightarrow> expr" ("!!")
- LAss :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
+ LAcc :: "vname \<Rightarrow> expr" ("!!")
+ LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
Return :: "expr \<Rightarrow> stmt"
StatRef :: "ref_ty \<Rightarrow> expr"
--- a/src/HOL/Bali/Trans.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Trans.thy Wed Jul 10 15:07:02 2002 +0200
@@ -7,175 +7,434 @@
execution of Java expressions and statements
PRELIMINARY!!!!!!!!
-
-improvements over Java Specification 1.0 (cf. 15.11.4.4):
-* dynamic method lookup does not need to check the return type
-* throw raises a NullPointer exception if a null reference is given, and each
- throw of a system exception yield a fresh exception object (was not specified)
-* if there is not enough memory even to allocate an OutOfMemory exception,
- evaluation/execution fails, i.e. simply stops (was not specified)
-
-design issues:
-* Lit expressions and Skip statements are considered completely evaluated.
-* the expr entry in rules is redundant in case of exceptions, but its full
- inclusion helps to make the rule structure independent of exception occurence.
-* the rule format is such that the start state may contain an exception.
- ++ faciliates exception handling (to be added later)
- + symmetry
-* the rules are defined carefully in order to be applicable even in not
- type-correct situations (yielding undefined values),
- e.g. the_Adr (Val (Bool b)) = arbitrary.
- ++ fewer rules
- - less readable because of auxiliary functions like the_Adr
- Alternative: "defensive" evaluation throwing some InternalError exception
- in case of (impossible, for correct programs) type mismatches
-
-simplifications:
-* just simple handling (i.e. propagation) of exceptions so far
-* dynamic method lookup does not check return type (should not be necessary)
*)
-Trans = Eval +
+theory Trans = Evaln:
+(*
+constdefs inj_stmt:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 83)
+ "\<langle>s\<rangle>\<^sub>s \<equiv> In1r s"
+
+constdefs inj_expr:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 83)
+ "\<langle>e\<rangle>\<^sub>e \<equiv> In1l e"
+*)
+axclass inj_term < "type"
+consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
+
+instance stmt::inj_term ..
+
+defs (overloaded)
+stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+
+lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
+by (simp add: stmt_inj_term_def)
+
+instance expr::inj_term ..
+
+defs (overloaded)
+expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+
+lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
+by (simp add: expr_inj_term_def)
+
+instance var::inj_term ..
+
+defs (overloaded)
+var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+
+lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
+by (simp add: var_inj_term_def)
+
+instance "list":: (type) inj_term ..
+
+defs (overloaded)
+expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+
+lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
+by (simp add: expr_list_inj_term_def)
+
+constdefs groundVar:: "var \<Rightarrow> bool"
+"groundVar v \<equiv> (case v of
+ LVar ln \<Rightarrow> True
+ | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
+ | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
+ | InsInitV c v \<Rightarrow> False)"
+
+lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
+ assumes ground: "groundVar v" and
+ LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
+ FVar: "\<And> accC statDeclC stat a fn.
+ \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
+ AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
+ shows "P"
+proof -
+ from ground LVar FVar AVar
+ show ?thesis
+ apply (cases v)
+ apply (simp add: groundVar_def)
+ apply (simp add: groundVar_def,blast)
+ apply (simp add: groundVar_def,blast)
+ apply (simp add: groundVar_def)
+ done
+qed
+
+constdefs groundExprs:: "expr list \<Rightarrow> bool"
+"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
+
+consts the_val:: "expr \<Rightarrow> val"
+primrec
+"the_val (Lit v) = v"
+
+consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
+primrec
+"the_var G s (LVar ln) =(lvar ln (store s),s)"
+the_var_FVar_def:
+"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
+the_var_AVar_def:
+"the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
+
+lemma the_var_FVar_simp[simp]:
+"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
+by (simp)
+declare the_var_FVar_def [simp del]
+
+lemma the_var_AVar_simp:
+"the_var G s ((Lit a).[Lit i]) = avar G i a s"
+by (simp)
+declare the_var_AVar_def [simp del]
consts
- texpr_tstmt :: "prog ë (((expr ò state) ò (expr ò state)) +
- ((stmt ò state) ò (stmt ò state))) set"
+ step :: "prog \<Rightarrow> ((term \<times> state) \<times> (term \<times> state)) set"
syntax (symbols)
- texpr :: "[prog, expr ò state, expr ò state] ë bool "("_É_ è1 _"[61,82,82] 81)
- tstmt :: "[prog, stmt ò state, stmt ò state] ë bool "("_É_ í1 _"[61,82,82] 81)
- Ref :: "loc ë expr"
+ step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
+ stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool"
+ ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
+"step*":: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
+ Ref :: "loc \<Rightarrow> expr"
+ SKIP :: "expr"
translations
-
- "GÉe_s è1 ex_s'" == "Inl (e_s, ex_s') Î texpr_tstmt G"
- "GÉs_s í1 s'_s'" == "Inr (s_s, s'_s') Î texpr_tstmt G"
+ "G\<turnstile>p \<mapsto>1 p' " == "(p,p') \<in> step G"
+ "G\<turnstile>p \<mapsto>n p' " == "(p,p') \<in> (step G)^n"
+ "G\<turnstile>p \<mapsto>* p' " == "(p,p') \<in> (step G)\<^sup>*"
"Ref a" == "Lit (Addr a)"
+ "SKIP" == "Lit Unit"
-constdefs
-
- sub_expr_expr :: "(expr ë expr) ë prop"
- "sub_expr_expr ef Ú (ÄG e s e' s'. GÉ( e,s) è1 ( e',s') êë
- GÉ(ef e,s) è1 (ef e',s'))"
-
-inductive "texpr_tstmt G" intrs
+inductive "step G" intros
(* evaluation of expression *)
(* cf. 15.5 *)
- XcptE "ËÂv. e Û Lit vÌ êë
- GÉ(e,Some xc,s) è1 (Lit arbitrary,Some xc,s)"
-
- CastXX "PROP sub_expr_expr (Cast T)"
-
-(*
- (* cf. 15.8.1 *)
- NewC "Ënew_Addr (heap s) = Some (a,x);
- s' = assign (hupd[aíinit_Obj G C]s) (x,s)Ì êë
- GÉ(NewC C,None,s) è1 (Ref a,s')"
-
- (* cf. 15.9.1 *)
-(*NewA1 "sub_expr_expr (NewA T)"*)
- NewA1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
- GÉ(New T[e],None,s) è1 (New T[e'],s')"
- NewA "Ëi = the_Intg i'; new_Addr (heap s) = Some (a, x);
- s' = assign (hupd[aíinit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s)Ì êë
- GÉ(New T[Lit i'],None,s) è1 (Ref a,s')"
- (* cf. 15.15 *)
- Cast1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
- GÉ(Cast T e,None,s) è1 (Cast T e',s')"
- Cast "Ëx'= raise_if (\<questiondown>G,sÉv fits T) ClassCast NoneÌ êë
- GÉ(Cast T (Lit v),None,s) è1 (Lit v,x',s)"
+Abrupt: "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
+ \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
+ \<forall> C vn c. t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
+ \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
+ \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
- (* cf. 15.7.1 *)
-(*Lit "GÉ(Lit v,None,s) è1 (Lit v,None,s)"*)
-
- (* cf. 15.13.1, 15.2 *)
- LAcc "Ëv = the (locals s vn)Ì êë
- GÉ(LAcc vn,None,s) è1 (Lit v,None,s)"
-
- (* cf. 15.25.1 *)
- LAss1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
- GÉ(f vn:=e,None,s) è1 (vn:=e',s')"
- LAss "GÉ(f vn:=Lit v,None,s) è1 (Lit v,None,lupd[vnív]s)"
+InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
- (* cf. 15.10.1, 15.2 *)
- FAcc1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
- GÉ({T}e..fn,None,s) è1 ({T}e'..fn,s')"
- FAcc "Ëv = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T))Ì êë
- GÉ({T}Lit a'..fn,None,s) è1 (Lit v,np a' None,s)"
-
- (* cf. 15.25.1 *)
- FAss1 "ËGÉ(e1,None,s) è1 (e1',s')Ì êë
- GÉ(f ({T}e1..fn):=e2,None,s) è1 (f({T}e1'..fn):=e2,s')"
- FAss2 "ËGÉ(e2,np a' None,s) è1 (e2',s')Ì êë
- GÉ(f({T}Lit a'..fn):=e2,None,s) è1 (f({T}Lit a'..fn):=e2',s')"
- FAss "Ëa = the_Addr a'; (c,fs) = the_Obj (heap s a);
- s'= assign (hupd[aíObj c (fs[(fn,T)ív])]s) (None,s)Ì êë
- GÉ(f({T}Lit a'..fn):=Lit v,None,s) è1 (Lit v,s')"
-
-
+(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
+(* Specialised rules to evaluate:
+ InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
+
+ (* cf. 15.8.1 *)
+NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
+NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
- (* cf. 15.12.1 *)
- AAcc1 "ËGÉ(e1,None,s) è1 (e1',s')Ì êë
- GÉ(e1[e2],None,s) è1 (e1'[e2],s')"
- AAcc2 "ËGÉ(e2,None,s) è1 (e2',s')Ì êë
- GÉ(Lit a'[e2],None,s) è1 (Lit a'[e2'],s')"
- AAcc "Ëvo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
- x' = raise_if (vo = None) IndOutBound (np a' None)Ì êë
- GÉ(Lit a'[Lit i'],None,s) è1 (Lit (the vo),x',s)"
+(* Alternative when rule SeqE is present
+NewCInited: "\<lbrakk>inited C (globs s);
+ G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
+
+NewC:
+ "\<lbrakk>\<not> inited C (globs s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
+
+*)
+ (* cf. 15.9.1 *)
+NewA:
+ "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
+InsInitNewAIdx:
+ "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
+InsInitNewA:
+ "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
+
+ (* cf. 15.15 *)
+CastE:
+ "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')"
+Cast:
+ "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) (Norm s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+ (* can be written without abupd, since we know Norm s *)
- (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
- Call1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
- GÉ(e..mn({pT}p),None,s) è1 (e'..mn({pT}p),s')"
- Call2 "ËGÉ(p,None,s) è1 (p',s')Ì êë
- GÉ(Lit a'..mn({pT}p),None,s) è1 (Lit a'..mn({pT}p'),s')"
- Call "Ëa = the_Addr a'; (md,(pn,rT),lvars,blk,res) =
- the (cmethd G (fst (the_Obj (h a))) (mn,pT))Ì êë
- GÉ(Lit a'..mn({pT}Lit pv),None,(h,l)) è1
- (Body blk res l,np a' x,(h,init_vals lvars[Thisía'][Supería'][pnípv]))"
- Body1 "ËGÉ(s0,None,s) í1 (s0',s')Ì êë
- GÉ(Body s0 e l,None,s) è1 (Body s0' e l,s')"
- Body2 "ËGÉ(e ,None,s) è1 (e',s')Ì êë
- GÉ(Body Skip e l,None,s) è1 (Body Skip e' l,s')"
- Body "GÉ(Body Skip (Lit v) l,None,s) è1 (Lit v,None,(heap s,l))"
+InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
+Inst: "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
+
+ (* cf. 15.7.1 *)
+(*Lit "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
+
+UnOpE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
+UnOp: "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
+
+BinOpE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
+BinOpE2: "\<lbrakk>G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
+BinOp: "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
+
+Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
+
+AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
+Acc: "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+
+(*
+AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
+AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+*)
+AssVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
+AssE: "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
+Ass: "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
+
+CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
+Cond: "G\<turnstile>(\<langle>Lit b? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>if the_Bool b then e1 else e2\<rangle>,Norm s)"
+
+
+CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
+CallArgs: "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
+Call: "\<lbrakk>groundExprs args; vs = map the_val args;
+ D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
+ s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
+
+Callee: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
+
+CalleeRet: "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
+
+Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
+
+Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
+
+InsInitBody:
+ "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
+InsInitBodyRet:
+ "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
+
+(* LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
+
+FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
+InsInitFVarE:
+ "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
+InsInitFVar:
+ "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
+-- {* Notice, that we do not have literal values for @{text vars}.
+The rules for accessing variables (@{text Acc}) and assigning to variables
+(@{text Ass}), test this with the predicate @{text groundVar}. After
+initialisation is done and the @{text FVar} is evaluated, we can't just
+throw away the @{text InsInitFVar} term and return a literal value, as in the
+cases of @{text New} or @{text NewC}. Instead we just return the evaluated
+@{text FVar} and test for initialisation in the rule @{text FVar}.
+*}
+
+
+AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
+
+AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s')
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
+
+(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
+
+(* evaluation of expression lists *)
+
+ -- {* @{text Nil} is fully evaluated *}
+
+ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
+
+ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
(* execution of statements *)
- (* cf. 14.1 *)
- XcptS "Ës0 Û SkipÌ êë
- GÉ(s0,Some xc,s) í1 (Skip,Some xc,s)"
-
(* cf. 14.5 *)
-(*Skip "GÉ(Skip,None,s) í1 (Skip,None,s)"*)
+Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
- (* cf. 14.2 *)
- Comp1 "ËGÉ(s1,None,s) í1 (s1',s')Ì êë
- GÉ(s1;; s2,None,s) í1 (s1';; s2,s')"
- Comp "GÉ(Skip;; s2,None,s) í1 (s2,None,s)"
-
-
-
-
+ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
+Expr: "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
- (* cf. 14.7 *)
- Expr1 "ËGÉ(e ,None,s) è1 (e',s')Ì êë
- GÉ(Expr e,None,s) í1 (Expr e',s')"
- Expr "GÉ(Expr (Lit v),None,s) í1 (Skip,None,s)"
+LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
+Lab: "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
+
+ (* cf. 14.2 *)
+CompC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
+
+Comp: "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
(* cf. 14.8.2 *)
- If1 "ËGÉ(e ,None,s) è1 (e',s')Ì êë
- GÉ(If(e) s1 Else s2,None,s) í1 (If(e') s1 Else s2,s')"
- If "GÉ(If(Lit v) s1 Else s2,None,s) í1
- (if the_Bool v then s1 else s2,None,s)"
+IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
+If: "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
(* cf. 14.10, 14.10.1 *)
- Loop "GÉ(While(e) s0,None,s) í1
- (If(e) (s0;; While(e) s0) Else Skip,None,s)"
+Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
+
+Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
+
+ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
+Throw: "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
+
+TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
+Try: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s)
+ \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
+ else (\<langle>Skip\<rangle>,s'))"
+
+FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
+
+Fin: "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
+
+FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
+FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
+
+
+Init1: "\<lbrakk>inited C (globs s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
+Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>
+ \<Longrightarrow>
+ G\<turnstile>(\<langle>Init C\<rangle>,Norm s)
+ \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
+ Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
+ ,Norm (init_class_obj G C s))"
+-- {* @{text InsInitE} is just used as trick to embed the statement
+@{text "init c"} into an expression*}
+InsInitESKIP:
+ "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
+
+(* Equivalenzen:
+ Bigstep zu Smallstep komplett.
+ Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
*)
- con_defs "[sub_expr_expr_def]"
-end
+lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
+proof -
+ assume "p \<in> R\<^sup>*"
+ moreover obtain x y where p: "p = (x,y)" by (cases p)
+ ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
+ hence "\<exists>n. (x,y) \<in> R^n"
+ proof induct
+ fix a have "(a,a) \<in> R^0" by simp
+ thus "\<exists>n. (a,a) \<in> R ^ n" ..
+ next
+ fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
+ then obtain n where "(a,b) \<in> R^n" ..
+ moreover assume "(b,c) \<in> R"
+ ultimately have "(a,c) \<in> R^(Suc n)" by auto
+ thus "\<exists>n. (a,c) \<in> R^n" ..
+ qed
+ with p show ?thesis by hypsubst
+qed
+
+(*
+lemma imp_eval_trans:
+ assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
+ shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
+*)
+(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
+ Sowas blödes:
+ Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
+ the_vals definieren\<dots>
+ G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
+*)
+
+
+end
\ No newline at end of file
--- a/src/HOL/Bali/TypeSafe.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Wed Jul 10 15:07:02 2002 +0200
@@ -173,7 +173,7 @@
| In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))
| In3 vs \<Rightarrow> True)"
apply (erule eval_induct)
-prefer 24
+prefer 26
apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
apply (auto del: conjI dest!: not_initedD gext_new sxalloc_gext halloc_gext
simp add: lvar_def fvar_def2 avar_def2 init_lvars_def2
@@ -1257,13 +1257,13 @@
obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
error_free_s1: "error_free s1"
by (blast)
- from conf_s1 have "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L)"
+ from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
by (cases s1) (auto intro: conforms_absorb)
with wt error_free_s1
- show "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L) \<and>
- (normal (abupd (absorb (Break l)) s1)
- \<longrightarrow> G,L,store (abupd (absorb (Break l)) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
- (error_free (Norm s0) = error_free (abupd (absorb (Break l)) s1))"
+ show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
+ (normal (abupd (absorb l) s1)
+ \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
+ (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
by (simp)
next
case (Comp c1 c2 s0 s1 s2 L accC T)
@@ -1463,9 +1463,12 @@
qed
qed
next
- case (Fin c1 c2 s0 s1 s2 x1 L accC T)
+ case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
have c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
+ have s3: "s3= (if \<exists>err. x1 = Some (Error err)
+ then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
have hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
have hyp_c2: "PROP ?TypeSafe (Norm s1) s2 (In1r c2) \<diamondsuit>" .
have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
@@ -1482,14 +1485,14 @@
with wt_c2 hyp_c2
obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
by blast
- show "abupd (abrupt_if (x1 \<noteq> None) x1) s2\<Colon>\<preceq>(G, L) \<and>
- (normal (abupd (abrupt_if (x1 \<noteq> None) x1) s2)
- \<longrightarrow> G,L,store (abupd (abrupt_if (x1 \<noteq> None) x1) s2)
- \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
- (error_free (Norm s0) =
- error_free (abupd (abrupt_if (x1 \<noteq> None) x1) s2))"
+ from error_free_s1 s3
+ have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
+ by simp
+ show "s3\<Colon>\<preceq>(G, L) \<and>
+ (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
+ (error_free (Norm s0) = error_free s3)"
proof (cases x1)
- case None with conf_s2 wt show ?thesis by auto
+ case None with conf_s2 s3' wt show ?thesis by auto
next
case (Some x)
with c2 wf conf_s1 conf_s2
@@ -1501,7 +1504,7 @@
with error_free_s2
have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
by (cases s2) simp
- with Some wt conf show ?thesis
+ with Some wt conf s3' show ?thesis
by (cases s2) auto
qed
next
@@ -1679,6 +1682,60 @@
by (auto elim!: wt_elim_cases
intro: conf_litval simp add: empty_dt_def)
next
+ case (UnOp e s0 s1 unop v L accC T)
+ have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
+ have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+ have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
+ then obtain eT
+ where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
+ wt_unop: "wt_unop unop eT" and
+ T: "T=Inl (PrimT (unop_type unop))"
+ by (auto elim!: wt_elim_cases)
+ from conf_s0 wt_e
+ obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
+ wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
+ error_free_s1: "error_free s1"
+ by (auto dest!: hyp)
+ from wt_v T wt_unop
+ have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
+ by (cases unop) auto
+ with conf_s1 error_free_s1
+ show "s1\<Colon>\<preceq>(G, L) \<and>
+ (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T) \<and>
+ error_free (Norm s0) = error_free s1"
+ by simp
+ next
+ case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
+ have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
+ have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" .
+ have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+ have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
+ then obtain e1T e2T where
+ wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
+ wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
+ wt_binop: "wt_binop G binop e1T e2T" and
+ T: "T=Inl (PrimT (binop_type binop))"
+ by (auto elim!: wt_elim_cases)
+ from conf_s0 wt_e1
+ obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
+ wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
+ error_free_s1: "error_free s1"
+ by (auto dest!: hyp_e1)
+ from conf_s1 wt_e2 error_free_s1
+ obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
+ wt_v2: "normal s2 \<longrightarrow> G,store s2\<turnstile>v2\<Colon>\<preceq>e2T" and
+ error_free_s2: "error_free s2"
+ by (auto dest!: hyp_e2)
+ from wt_v1 wt_v2 wt_binop T
+ have "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
+ by (cases binop) auto
+ with conf_s2 error_free_s2
+ show "s2\<Colon>\<preceq>(G, L) \<and>
+ (normal s2 \<longrightarrow>
+ G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
+ error_free (Norm s0) = error_free s2"
+ by simp
+ next
case (Super s L accC T)
have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
@@ -1818,7 +1875,7 @@
have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a')" .
have hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
have hyp_methd: "PROP ?TypeSafe s3' s4
- (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
+ (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" .
@@ -1995,7 +2052,7 @@
\<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
by - (drule wf_mdecl_bodyD,
- simp cong add: lname.case_cong ename.case_cong)
+ auto simp: cong add: lname.case_cong ename.case_cong)
with dynM' iscls_invDeclC invDeclC'
have
"\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
@@ -2031,14 +2088,14 @@
next
case (Methd D s0 s1 sig v L accC T)
have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
- have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
+ have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
then obtain m bodyT where
D: "is_class G D" and
m: "methd G D sig = Some m" and
wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
- \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
+ \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
T: "T=Inl bodyT"
by (rule wt_elim_cases) auto
with hyp [of _ _ "(Inl bodyT)"] conf_s0
@@ -2079,7 +2136,7 @@
show "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L) \<and>
(normal (abupd (absorb Ret) s2) \<longrightarrow>
G,L,store (abupd (absorb Ret) s2)
- \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
+ \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
(error_free (Norm s0) = error_free (abupd (absorb Ret) s2)) "
by (cases s2) (auto intro: conforms_locals)
next
--- a/src/HOL/Bali/WellType.thy Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/WellType.thy Wed Jul 10 15:07:02 2002 +0200
@@ -180,7 +180,67 @@
apply (clarsimp simp add: invmode_IntVir_eq)
done
+consts unop_type :: "unop \<Rightarrow> prim_ty"
+primrec
+"unop_type UPlus = Integer"
+"unop_type UMinus = Integer"
+"unop_type UBitNot = Integer"
+"unop_type UNot = Boolean"
+consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
+primrec
+"wt_unop UPlus t = (t = PrimT Integer)"
+"wt_unop UMinus t = (t = PrimT Integer)"
+"wt_unop UBitNot t = (t = PrimT Integer)"
+"wt_unop UNot t = (t = PrimT Boolean)"
+
+consts binop_type :: "binop \<Rightarrow> prim_ty"
+primrec
+"binop_type Mul = Integer"
+"binop_type Div = Integer"
+"binop_type Mod = Integer"
+"binop_type Plus = Integer"
+"binop_type Minus = Integer"
+"binop_type LShift = Integer"
+"binop_type RShift = Integer"
+"binop_type RShiftU = Integer"
+"binop_type Less = Boolean"
+"binop_type Le = Boolean"
+"binop_type Greater = Boolean"
+"binop_type Ge = Boolean"
+"binop_type Eq = Boolean"
+"binop_type Neq = Boolean"
+"binop_type BitAnd = Integer"
+"binop_type And = Boolean"
+"binop_type BitXor = Integer"
+"binop_type Xor = Boolean"
+"binop_type BitOr = Integer"
+"binop_type Or = Boolean"
+
+consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
+primrec
+"wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
+"wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
+"wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+"wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+"wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+
+
types tys = "ty + ty list"
translations
"tys" <= (type) "ty + ty list"
@@ -237,6 +297,7 @@
"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
+
inductive wt intros
@@ -312,6 +373,15 @@
Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Lit x\<Colon>-T"
+ UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk>
+ \<Longrightarrow>
+ E,dt\<Turnstile>UnOp unop e\<Colon>-T"
+
+ BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
+ T=PrimT (binop_type binop)\<rbrakk>
+ \<Longrightarrow>
+ E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
+
(* cf. 15.10.2, 15.11.1 *)
Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
@@ -348,6 +418,9 @@
(* The class C is the dynamic class of the method call (cf. Eval.thy).
* It hasn't got to be directly accessible from the current package (pkg E).
* Only the static class must be accessible (enshured indirectly by Call).
+ * Note that l is just a dummy value. It is only used in the smallstep
+ * semantics. To proof typesafety directly for the smallstep semantics
+ * we would have to assume conformance of l here!
*)
Body: "\<lbrakk>is_class (prg E) D;
@@ -359,7 +432,8 @@
* from the current package (pkg E), but can also be indirectly accessible
* due to inheritance (enshured in Call)
* The result type hasn't got to be accessible in Java! (If it is not
- * accessible you can only assign it to Object)
+ * accessible you can only assign it to Object).
+ * For dummy value l see rule Methd.
*)
(* well-typed variables *)
@@ -404,6 +478,8 @@
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T"
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T"
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T"
+ "E,dt\<Turnstile>In1l (UnOp unop e) \<Colon>T"
+ "E,dt\<Turnstile>In1l (BinOp binop e1 e2) \<Colon>T"
"E,dt\<Turnstile>In1l (Super) \<Colon>T"
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T"
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T"
@@ -566,11 +642,11 @@
apply (simp_all (no_asm_use) split del: split_if_asm)
apply (safe del: disjE)
(* 17 subgoals *)
-apply (tactic {* ALLGOALS (fn i => if i = 9 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
+apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
(*apply (safe del: disjE elim!: wt_elim_cases)*)
apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
apply (simp_all (no_asm_use) split del: split_if_asm)
-apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
+apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
apply ((blast del: equalityCE dest: sym [THEN trans])+)
done