src/HOL/Bali/Eval.thy
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13384 a34e38154413
     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