src/HOL/Bali/Trans.thy
changeset 13384 a34e38154413
parent 13354 8c8eafb63746
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/Trans.thy	Tue Jul 16 18:52:26 2002 +0200
     1.2 +++ b/src/HOL/Bali/Trans.thy	Tue Jul 16 20:25:21 2002 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4  
     1.5  theory Trans = Evaln:
     1.6  
     1.7 -
     1.8  constdefs groundVar:: "var \<Rightarrow> bool"
     1.9  "groundVar v \<equiv> (case v of
    1.10                     LVar ln \<Rightarrow> True
    1.11 @@ -162,13 +161,19 @@
    1.12  BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
    1.13             \<Longrightarrow> 
    1.14             G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
    1.15 -BinOpE2:  "\<lbrakk>G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
    1.16 +BinOpE2:  "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
    1.17             \<Longrightarrow> 
    1.18             G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
    1.19              \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
    1.20 +BinOpTerm:  "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
    1.21 +             \<Longrightarrow> 
    1.22 +             G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
    1.23 +              \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
    1.24  BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
    1.25              \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
    1.26 -
    1.27 +(* Maybe its more convenient to add: need_second_arg as precondition to BinOp 
    1.28 +   to make the choice between BinOpTerm and BinOp deterministic *)
    1.29 +   
    1.30  Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
    1.31  
    1.32  AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>