src/HOL/Bali/Eval.thy
changeset 13384 a34e38154413
parent 13337 f75dfc606ac7
child 13462 56610e2ba220
     1.1 --- a/src/HOL/Bali/Eval.thy	Tue Jul 16 18:52:26 2002 +0200
     1.2 +++ b/src/HOL/Bali/Eval.thy	Tue Jul 16 20:25:21 2002 +0200
     1.3 @@ -455,8 +455,6 @@
     1.4  "eval_unop UNot    v = Bool (\<not> the_Bool v)"
     1.5  
     1.6  consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
     1.7 -
     1.8 -
     1.9  primrec
    1.10  "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
    1.11  "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
    1.12 @@ -482,7 +480,25 @@
    1.13  "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
    1.14  "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
    1.15  "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
    1.16 +"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
    1.17 +"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
    1.18  
    1.19 +constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
    1.20 +"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
    1.21 +                               (binop=CondOr  \<and> the_Bool v1))"
    1.22 +text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
    1.23 + if the value isn't already determined by the first argument*}
    1.24 +
    1.25 +lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
    1.26 +by (simp add: need_second_arg_def)
    1.27 +
    1.28 +lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
    1.29 +by (simp add: need_second_arg_def)
    1.30 +
    1.31 +lemma need_second_arg_strict[simp]: 
    1.32 + "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
    1.33 +by (cases binop) 
    1.34 +   (simp_all add: need_second_arg_def)
    1.35  
    1.36  consts
    1.37    eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
    1.38 @@ -550,6 +566,11 @@
    1.39    SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
    1.40  	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
    1.41  
    1.42 +text {* 
    1.43 +\par
    1.44 +*} (* dummy text command to break paragraph for latex;
    1.45 +              large paragraphs exhaust memory of debian pdflatex *)
    1.46 +
    1.47  inductive "eval G" intros
    1.48  
    1.49  (* propagation of abrupt completion *)
    1.50 @@ -671,8 +692,11 @@
    1.51  
    1.52    UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> 
    1.53           \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
    1.54 -
    1.55 -  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<rightarrow> s2\<rbrakk> 
    1.56 + 
    1.57 +  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; 
    1.58 +          G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
    1.59 +                \<succ>\<rightarrow> (In1 v2,s2)
    1.60 +          \<rbrakk> 
    1.61           \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
    1.62     
    1.63    (* cf. 15.10.2 *)
    1.64 @@ -764,6 +788,10 @@
    1.65  *}
    1.66  
    1.67  
    1.68 +text {* 
    1.69 +\par
    1.70 +*} (* dummy text command to break paragraph for latex;
    1.71 +              large paragraphs exhaust memory of debian pdflatex *)
    1.72  
    1.73  lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
    1.74     and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
    1.75 @@ -1104,6 +1132,31 @@
    1.76  apply force
    1.77  done
    1.78  
    1.79 +lemma eval_binop_arg2_indep:
    1.80 +"\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
    1.81 +by (cases binop)
    1.82 +   (simp_all add: need_second_arg_def)
    1.83 +
    1.84 +
    1.85 +lemma eval_BinOp_arg2_indepI:
    1.86 +  assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
    1.87 +          no_need: "\<not> need_second_arg binop v1" 
    1.88 +  shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
    1.89 +         (is "?EvalBinOp v2")
    1.90 +proof -
    1.91 +  from eval_e1 
    1.92 +  have "?EvalBinOp Unit" 
    1.93 +    by (rule eval.BinOp)
    1.94 +       (simp add: no_need)
    1.95 +  moreover
    1.96 +  from no_need 
    1.97 +  have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
    1.98 +    by (simp add: eval_binop_arg2_indep)
    1.99 +  ultimately
   1.100 +  show ?thesis
   1.101 +    by simp
   1.102 +qed
   1.103 +
   1.104  
   1.105  section "single valued"
   1.106