1.1 --- a/src/HOL/Bali/Eval.thy Wed Jul 10 14:51:18 2002 +0200
1.2 +++ b/src/HOL/Bali/Eval.thy Wed Jul 10 15:07:02 2002 +0200
1.3 @@ -447,6 +447,43 @@
1.4
1.5 section "evaluation judgments"
1.6
1.7 +consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
1.8 +primrec
1.9 +"eval_unop UPlus v = Intg (the_Intg v)"
1.10 +"eval_unop UMinus v = Intg (- (the_Intg v))"
1.11 +"eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented"
1.12 +"eval_unop UNot v = Bool (\<not> the_Bool v)"
1.13 +
1.14 +consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
1.15 +
1.16 +
1.17 +primrec
1.18 +"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
1.19 +"eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
1.20 +"eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
1.21 +"eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
1.22 +"eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
1.23 +
1.24 +-- "Be aware of the explicit coercion of the shift distance to nat"
1.25 +"eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))"
1.26 +"eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
1.27 +"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
1.28 +
1.29 +"eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))"
1.30 +"eval_binop Le v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
1.31 +"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
1.32 +"eval_binop Ge v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
1.33 +
1.34 +"eval_binop Eq v1 v2 = Bool (v1=v2)"
1.35 +"eval_binop Neq v1 v2 = Bool (v1\<noteq>v2)"
1.36 +"eval_binop BitAnd v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
1.37 +"eval_binop And v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
1.38 +"eval_binop BitXor v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
1.39 +"eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
1.40 +"eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
1.41 +"eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
1.42 +
1.43 +
1.44 consts
1.45 eval :: "prog \<Rightarrow> (state \<times> term \<times> vals \<times> state) set"
1.46 halloc:: "prog \<Rightarrow> (state \<times> obj_tag \<times> loc \<times> state) set"
1.47 @@ -513,7 +550,6 @@
1.48 SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
1.49 G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
1.50
1.51 -
1.52 inductive "eval G" intros
1.53
1.54 (* propagation of abrupt completion *)
1.55 @@ -533,7 +569,7 @@
1.56 G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
1.57
1.58 Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
1.59 - G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
1.60 + G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
1.61 (* cf. 14.2 *)
1.62 Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
1.63 G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
1.64 @@ -573,9 +609,12 @@
1.65
1.66 (* cf. 14.18.2 *)
1.67 Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
1.68 - G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
1.69 - G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
1.70 -
1.71 + G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
1.72 + s3=(if (\<exists> err. x1=Some (Error err))
1.73 + then (x1,s1)
1.74 + else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk>
1.75 + \<Longrightarrow>
1.76 + G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
1.77 (* cf. 12.4.2, 8.5 *)
1.78 Init: "\<lbrakk>the (class G C) = c;
1.79 if inited C (globs s0) then s3 = Norm s0
1.80 @@ -630,8 +669,12 @@
1.81 (* cf. 15.7.1 *)
1.82 Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
1.83
1.84 + UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk>
1.85 + \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
1.86
1.87 -
1.88 + BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<rightarrow> s2\<rbrakk>
1.89 + \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
1.90 +
1.91 (* cf. 15.10.2 *)
1.92 Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
1.93
1.94 @@ -666,11 +709,14 @@
1.95
1.96 Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
1.97 G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
1.98 -
1.99 + (* The local variables l are just a dummy here. The are only used by
1.100 + the smallstep semantics *)
1.101 (* cf. 14.15, 12.4.1 *)
1.102 Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
1.103 - G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
1.104 -
1.105 + G\<turnstile>Norm s0 \<midarrow>Body D c
1.106 + -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
1.107 + (* The local variables l are just a dummy here. The are only used by
1.108 + the smallstep semantics *)
1.109 (* evaluation of variables *)
1.110
1.111 (* cf. 15.13.1, 15.7.2 *)
1.112 @@ -704,21 +750,24 @@
1.113 G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
1.114
1.115 (* Rearrangement of premisses:
1.116 -[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
1.117 - 17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
1.118 - 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
1.119 - 27(AVar),22(Call)]
1.120 +[0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
1.121 + 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
1.122 + 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
1.123 + 29(AVar),24(Call)]
1.124 *)
1.125 ML {*
1.126 bind_thm ("eval_induct_", rearrange_prems
1.127 -[0,1,2,8,4,28,29,25,15,16,
1.128 - 17,18,19,3,5,23,24,21,6,
1.129 - 7,11,9,13,14,12,20,10,26,
1.130 - 27,22] (thm "eval.induct"))
1.131 +[0,1,2,8,4,30,31,27,15,16,
1.132 + 17,18,19,20,21,3,5,25,26,23,6,
1.133 + 7,11,9,13,14,12,22,10,28,
1.134 + 29,24] (thm "eval.induct"))
1.135 *}
1.136
1.137 +
1.138 +
1.139 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
1.140 - and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and
1.141 + and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and
1.142 + and and
1.143 s2 (* Fin *) and and s2 (* NewC *)]
1.144
1.145 declare split_if [split del] split_if_asm [split del]
1.146 @@ -757,6 +806,8 @@
1.147 "G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> vs'"
1.148 "G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> vs'"
1.149 "G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> vs'"
1.150 + "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<rightarrow> vs'"
1.151 + "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<rightarrow> vs'"
1.152 "G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> vs'"
1.153 "G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> vs'"
1.154 "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> vs'"
1.155 @@ -802,6 +853,7 @@
1.156 apply auto
1.157 done
1.158
1.159 +
1.160 ML_setup {*
1.161 fun eval_fun nam inj rhs =
1.162 let
1.163 @@ -827,6 +879,68 @@
1.164
1.165 declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!]
1.166
1.167 +text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
1.168 +used in smallstep semantics, not in the bigstep semantics. So their is no
1.169 +valid evaluation of these terms
1.170 +*}
1.171 +
1.172 +
1.173 +lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
1.174 +proof -
1.175 + { fix s t v s'
1.176 + assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
1.177 + normal: "normal s" and
1.178 + callee: "t=In1l (Callee l e)"
1.179 + then have "False"
1.180 + proof (induct)
1.181 + qed (auto)
1.182 + }
1.183 + then show ?thesis
1.184 + by (cases s') fastsimp
1.185 +qed
1.186 +
1.187 +
1.188 +lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
1.189 +proof -
1.190 + { fix s t v s'
1.191 + assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
1.192 + normal: "normal s" and
1.193 + callee: "t=In1l (InsInitE c e)"
1.194 + then have "False"
1.195 + proof (induct)
1.196 + qed (auto)
1.197 + }
1.198 + then show ?thesis
1.199 + by (cases s') fastsimp
1.200 +qed
1.201 +
1.202 +lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
1.203 +proof -
1.204 + { fix s t v s'
1.205 + assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
1.206 + normal: "normal s" and
1.207 + callee: "t=In2 (InsInitV c w)"
1.208 + then have "False"
1.209 + proof (induct)
1.210 + qed (auto)
1.211 + }
1.212 + then show ?thesis
1.213 + by (cases s') fastsimp
1.214 +qed
1.215 +
1.216 +lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
1.217 +proof -
1.218 + { fix s t v s'
1.219 + assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
1.220 + normal: "normal s" and
1.221 + callee: "t=In1r (FinA a c)"
1.222 + then have "False"
1.223 + proof (induct)
1.224 + qed (auto)
1.225 + }
1.226 + then show ?thesis
1.227 + by (cases s') fastsimp
1.228 +qed
1.229
1.230 lemma eval_no_abrupt_lemma:
1.231 "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
1.232 @@ -909,7 +1023,8 @@
1.233 apply (case_tac "s", case_tac "a = None")
1.234 by (auto intro!: eval.If)
1.235
1.236 -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'"
1.237 +lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s'
1.238 + \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
1.239 apply (case_tac "s", case_tac "a = None")
1.240 by (auto intro!: eval.Methd)
1.241
1.242 @@ -979,7 +1094,8 @@
1.243 *)
1.244
1.245 lemma eval_Methd:
1.246 - "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')"
1.247 + "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s')
1.248 + \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
1.249 apply (case_tac "s")
1.250 apply (case_tac "a")
1.251 apply clarsimp+
1.252 @@ -1025,6 +1141,12 @@
1.253 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
1.254 by auto
1.255
1.256 +lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
1.257 + res=the (locals (store s2) Result);
1.258 + s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>
1.259 + G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"
1.260 +by (auto elim: eval.Body)
1.261 +
1.262 lemma unique_eval [rule_format (no_asm)]:
1.263 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
1.264 apply (case_tac "ws")
1.265 @@ -1033,18 +1155,18 @@
1.266 apply (erule eval_induct)
1.267 apply (tactic {* ALLGOALS (EVERY'
1.268 [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
1.269 -(* 29 subgoals *)
1.270 -prefer 26 (* Try *)
1.271 +(* 31 subgoals *)
1.272 +prefer 28 (* Try *)
1.273 apply (simp (no_asm_use) only: split add: split_if_asm)
1.274 -(* 32 subgoals *)
1.275 -prefer 28 (* Init *)
1.276 +(* 34 subgoals *)
1.277 +prefer 30 (* Init *)
1.278 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
1.279 -prefer 24 (* While *)
1.280 +prefer 26 (* While *)
1.281 apply (simp (no_asm_use) only: split add: split_if_asm, blast)
1.282 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
1.283 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
1.284 apply blast
1.285 -(* 31 subgoals *)
1.286 +(* 33 subgoals *)
1.287 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
1.288 done
1.289