diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Eval.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -455,8 +455,6 @@
 "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))"
@@ -482,7 +480,25 @@
 "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))"
+"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
 
+constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
+"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
+                               (binop=CondOr  \<and> the_Bool v1))"
+text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
+ if the value isn't already determined by the first argument*}
+
+lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
+by (simp add: need_second_arg_def)
+
+lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
+by (simp add: need_second_arg_def)
+
+lemma need_second_arg_strict[simp]: 
+ "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
+by (cases binop) 
+   (simp_all add: need_second_arg_def)
 
 consts
   eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
@@ -550,6 +566,11 @@
   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)"
 
+text {* 
+\par
+*} (* dummy text command to break paragraph for latex;
+              large paragraphs exhaust memory of debian pdflatex *)
+
 inductive "eval G" intros
 
 (* propagation of abrupt completion *)
@@ -671,8 +692,11 @@
 
   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> 
+ 
+  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; 
+          G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
+                \<succ>\<rightarrow> (In1 v2,s2)
+          \<rbrakk> 
          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
    
   (* cf. 15.10.2 *)
@@ -764,6 +788,10 @@
 *}
 
 
+text {* 
+\par
+*} (* dummy text command to break paragraph for latex;
+              large paragraphs exhaust memory of debian pdflatex *)
 
 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
    and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
@@ -1104,6 +1132,31 @@
 apply force
 done
 
+lemma eval_binop_arg2_indep:
+"\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
+by (cases binop)
+   (simp_all add: need_second_arg_def)
+
+
+lemma eval_BinOp_arg2_indepI:
+  assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
+          no_need: "\<not> need_second_arg binop v1" 
+  shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
+         (is "?EvalBinOp v2")
+proof -
+  from eval_e1 
+  have "?EvalBinOp Unit" 
+    by (rule eval.BinOp)
+       (simp add: no_need)
+  moreover
+  from no_need 
+  have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
+    by (simp add: eval_binop_arg2_indep)
+  ultimately
+  show ?thesis
+    by simp
+qed
+
 
 section "single valued"