# HG changeset patch
# User schirmer
# Date 1026843921 -7200
# Node ID a34e3815441361951ef2d39be7429d1015815a19
# Parent  041d78bf9403715015acc245960a450621bbe5da
Added conditional and (&&) and or (||).

diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -467,24 +467,6 @@
 apply       (auto dest: eval_type_sound)
 done
 
-(* FIXME To TypeSafe *)
-lemma wf_eval_Fin: 
-  assumes wf:    "wf_prog G" and
-          wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
-        conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
-        eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
-        eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
-            s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
-  shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
-proof -
-  from eval_c1 wt_c1 wf conf_s0
-  have "error_free (x1,s1)"
-    by (auto dest: eval_type_sound)
-  with eval_c1 eval_c2 s3
-  show ?thesis
-    by - (rule eval.Fin, auto simp add: error_free_def)
-qed
-
 text {* For @{text MGFn_Fin} we need the wellformedness of the program to
 switch from the evaln-semantics to the eval-semantics *}
 lemma MGFn_Fin: 
@@ -559,8 +541,24 @@
 apply (rule ax_derivs.UnOp, tactic "forw_hyp_eval_Force_tac 1")
 
 apply (rule ax_derivs.BinOp)
-apply  (erule MGFnD [THEN ax_NormalD])
-apply (tactic "forw_hyp_eval_Force_tac 1")
+apply   (erule MGFnD [THEN ax_NormalD])
+
+apply   (rule allI)
+apply   (case_tac "need_second_arg binop v1")
+apply     simp
+apply     (tactic "forw_hyp_eval_Force_tac 1")
+
+apply     simp
+apply     (rule ax_Normal_cases)
+apply       (rule ax_derivs.Skip [THEN conseq1])
+apply       clarsimp
+
+apply       (rule eval_BinOp_arg2_indepI)
+apply       simp
+apply       simp
+
+apply  (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
+apply  (tactic "eval_Force_tac 1")
 
 apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
 apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/AxSem.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -483,7 +483,6 @@
 claset_ref () := claset () delSWrapper "split_all_tac"
 *}
 
-
 inductive "ax_derivs G" intros
 
   empty: " G,A|\<turnstile>{}"
@@ -542,7 +541,9 @@
 
   BinOp:
    "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
-     \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} e2-\<succ> {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
+     \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} 
+               (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ>
+               {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
     \<Longrightarrow>
     G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}" 
 
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/AxSound.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -391,6 +391,9 @@
 
 (* BinOp *)
 apply (tactic "sound_forw_hyp_tac 1")
+apply (case_tac "need_second_arg binop v1")
+apply   fastsimp
+apply   simp
 
 (* Ass *)
 apply (tactic "sound_forw_hyp_tac 1")
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"
 
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Evaln.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -106,7 +106,9 @@
   UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
 
-  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n\<rightarrow> s2\<rbrakk> 
+  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; 
+           G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
+            \<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk> 
          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
 
   Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
@@ -388,6 +390,21 @@
 apply auto
 done
 
+(* ##### FIXME: To WellType *)
+lemma wt_elim_BinOp:
+  "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
+    \<And>T1 T2 T3.
+       \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
+          E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
+          T = Inl (PrimT (binop_type binop))\<rbrakk>
+       \<Longrightarrow> P\<rbrakk>
+\<Longrightarrow> P"
+apply (erule wt_elim_cases)
+apply (cases b)
+apply auto
+done
+
+section {* evaln implies eval *}
 lemma evaln_eval:  
   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
              wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
@@ -507,8 +524,8 @@
       by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
   next
     case BinOp
-    with wf show ?case
-      by - (erule wt_elim_cases, blast intro!: eval.BinOp dest: eval_type_sound)
+    with wf show ?case 
+      by - (erule wt_elim_BinOp, blast intro!: eval.BinOp dest: eval_type_sound)
   next
     case Super
     show ?case by (rule eval.Super)
@@ -1085,6 +1102,7 @@
   show ?thesis .
 qed
 
+section {* eval implies evaln *}
 lemma eval_evaln: 
   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
@@ -1446,8 +1464,9 @@
     case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
     with wf obtain n1 n2 where 
       "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
-      "G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n2\<rightarrow> s2"    
-      by (blast elim!: wt_elim_cases dest: eval_type_sound)
+      "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+               else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
+      by (blast elim!: wt_elim_BinOp dest: eval_type_sound)
     hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
            \<rightarrow> s2"
       by (blast intro!: evaln.BinOp dest: evaln_max2)
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Term.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -60,26 +60,26 @@
 
 
 
-types locals = "(lname, val) table"  (* local variables *)
+types locals = "(lname, val) table"  --{* local variables *}
 
 
 datatype jump
-        = Break label (* break *)
-        | Cont label  (* continue *)
-        | Ret         (* return from method *)
+        = Break label --{* break *}
+        | Cont label  --{* continue *}
+        | Ret         --{* return from method *}
 
-datatype xcpt        (* exception *)
-	= Loc loc    (* location of allocated execption object *)
-	| Std xname  (* intermediate standard exception, see Eval.thy *)
+datatype xcpt        --{* exception *}
+	= Loc loc    --{* location of allocated execption object *}
+	| Std xname  --{* intermediate standard exception, see Eval.thy *}
 
 datatype error
-       = AccessViolation (* Access to a member that isn't permitted *)
+       = AccessViolation --{* Access to a member that isn't permitted *}
 
-datatype abrupt      (* abrupt completion *) 
-        = Xcpt xcpt  (* exception *)
-        | Jump jump  (* break, continue, return *)
-        | Error error (* runtime errors, we wan't to detect and proof absent
-                         in welltyped programms *)
+datatype abrupt       --{* abrupt completion *} 
+        = Xcpt xcpt   --{* exception *}
+        | Jump jump   --{* break, continue, return *}
+        | Error error -- {* runtime errors, we wan't to detect and proof absent
+                            in welltyped programms *}
 types
   abopt  = "abrupt option"
 
@@ -92,93 +92,132 @@
 translations
  "locals" <= (type) "(lname, val) table"
 
-datatype inv_mode                  (* invocation mode for method calls *)
-	= Static                   (* static *)
-	| SuperM                   (* super  *)
-	| IntVir                   (* interface or virtual *)
+datatype inv_mode                  --{* invocation mode for method calls *}
+	= Static                   --{* static *}
+	| SuperM                   --{* super  *}
+	| IntVir                   --{* interface or virtual *}
 
-record  sig =            (* signature of a method, cf. 8.4.2  *)
-	  name ::"mname"      (* acutally belongs to Decl.thy *)
+record  sig =              --{* signature of a method, cf. 8.4.2  *}
+	  name ::"mname"   --{* acutally belongs to Decl.thy *}
           parTs::"ty list"        
 
 translations
   "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
   "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
 
--- "function codes for unary operations"
-datatype unop =  UPlus    
-               | UMinus   
-               | UBitNot  
-               | UNot     
+--{* function codes for unary operations *}
+datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
+               | UMinus   -- {*{\tt -} unary minus*}
+               | UBitNot  -- {*{\tt ~} bitwise NOT*}
+               | UNot     -- {*{\tt !} logical complement*}
 
--- "function codes for binary operations"
-datatype binop = Mul     
-               | Div     
-               | Mod     
-               | Plus    
-               | Minus   
-               | LShift  
-               | RShift  
-               | RShiftU 
-               | Less    
-               | Le      
-               | Greater 
-               | Ge      
-               | Eq      
-               | Neq     
-               | BitAnd  
-               | And     
-               | BitXor  
-               | Xor     
-               | BitOr   
-               | Or      
+--{* function codes for binary operations *}
+datatype binop = Mul     -- {*{\tt * }   multiplication*}
+               | Div     -- {*{\tt /}   division*}
+               | Mod     -- {*{\tt \%}   remainder*}
+               | Plus    -- {*{\tt +}   addition*}
+               | Minus   -- {*{\tt -}   subtraction*}
+               | LShift  -- {*{\tt <<}  left shift*}
+               | RShift  -- {*{\tt >>}  signed right shift*}
+               | RShiftU -- {*{\tt >>>} unsigned right shift*}
+               | Less    -- {*{\tt <}   less than*}
+               | Le      -- {*{\tt <=}  less than or equal*}
+               | Greater -- {*{\tt >}   greater than*}
+               | Ge      -- {*{\tt >=}  greater than or equal*}
+               | Eq      -- {*{\tt ==}  equal*}
+               | Neq     -- {*{\tt !=}  not equal*}
+               | BitAnd  -- {*{\tt \&}   bitwise AND*}
+               | And     -- {*{\tt \&}   boolean AND*}
+               | BitXor  -- {*{\texttt \^}   bitwise Xor*}
+               | Xor     -- {*{\texttt \^}   boolean Xor*}
+               | BitOr   -- {*{\tt |}   bitwise Or*}
+               | Or      -- {*{\tt |}   boolean Or*}
+               | CondAnd -- {*{\tt \&\&}  conditional And*}
+               | CondOr  -- {*{\tt ||}  conditional Or *}
+text{* The boolean operators {\tt \&} and {\tt |} strictly evaluate both
+of their arguments. The conditional operators {\tt \&\&} and {\tt ||} only 
+evaluate the second argument if the value of the whole expression isn't 
+allready determined by the first argument.
+e.g.: {\tt false \&\& e} e is not evaluated;  
+      {\tt true || e} e is not evaluated; 
+*}
 
 datatype var
-	= LVar                  lname(* local variable (incl. parameters) *)
-        | FVar qtname qtname bool expr vname
-                                (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
-	| AVar expr expr    (* array component *) ("_.[_]"[90,10   ]90)
-        | InsInitV stmt var (* insertion of initialization before
-                                   evaluation of var (for smallstep sem.) *)
+	= LVar lname --{* local variable (incl. parameters) *}
+        | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
+                     --{* class field *}
+                     --{* @{term "{accC,statDeclC,stat}e..fn"}   *}
+                     --{* @{text accC}: accessing class (static class were *}
+                     --{* the code is declared. Annotation only needed for *}
+                     --{* evaluation to check accessibility) *}
+                     --{* @{text statDeclC}: static declaration class of field*}
+                     --{* @{text stat}: static or instance field?*}
+                     --{* @{text e}: reference to object*}
+                     --{* @{text fn}: field name*}
+	| AVar expr expr ("_.[_]"[90,10   ]90)
+                     --{* array component *}
+                     --{* @{term "e1.[e2]"}: e1 array reference; e2 index *}
+        | InsInitV stmt var 
+                     --{* insertion of initialization before evaluation   *}
+                     --{* of var (technical term for smallstep semantics.)*}
 
 and expr
-	= NewC qtname         (* class instance creation *)
-	| NewA ty expr        (* array creation *) ("New _[_]"[99,10   ]85)
-	| Cast ty expr        (* type cast  *)
-	| Inst expr ref_ty    (* instanceof *)     ("_ InstOf _"[85,99] 85)
-	| Lit  val            (* literal value, references not allowed *)
-        | UnOp unop expr        (* unary operation *)
-        | BinOp binop expr expr (* binary operation *)
+	= NewC qtname         --{* class instance creation *}
+	| NewA ty expr ("New _[_]"[99,10   ]85) 
+                              --{* array creation *} 
+	| Cast ty expr        --{* type cast  *}
+	| Inst expr ref_ty ("_ InstOf _"[85,99] 85)   
+                              --{* instanceof *}     
+	| Lit  val              --{* literal value, references not allowed *}
+        | UnOp unop expr        --{* unary operation *}
+        | BinOp binop expr expr --{* binary operation *}
         
-	| Super               (* special Super keyword *)
-	| Acc  var            (* variable access *)
-	| Ass  var expr       (* variable assign *) ("_:=_"   [90,85   ]85)
-	| Cond expr expr expr (* conditional *)  ("_ ? _ : _" [85,85,80]80)
-        | Call qtname ref_ty inv_mode expr mname "(ty list)" 
-               "(expr list)"  (* method call *) 
-                              ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
-        | Methd qtname sig    (*   (folded) method (see below) *)
-        | Body qtname stmt    (* (unfolded) method body *)
-        | InsInitE stmt expr      (* insertion of initialization before
-                                   evaluation of expr (for smallstep sem.) *)
-        | Callee locals expr      (* save Callers locals in Callee-Frame
-                                     (for smallstep semantics) *)
+	| Super               --{* special Super keyword *}
+	| Acc  var            --{* variable access *}
+	| Ass  var expr       ("_:=_"   [90,85   ]85)
+                              --{* variable assign *} 
+	| Cond expr expr expr ("_ ? _ : _" [85,85,80]80) --{* conditional *}  
+        | Call qtname ref_ty inv_mode expr mname "(ty list)" "(expr list)"  
+            ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) 
+                    --{* method call *} 
+                    --{* @{term "{accC,statT,mode}e\<cdot>mn({pTs}args)"} " *}
+                    --{* @{text accC}: accessing class (static class were *}
+                    --{* the call code is declared. Annotation only needed for*}
+                    --{* evaluation to check accessibility) *}
+                    --{* @{text statT}: static declaration class/interface of *}
+                    --{* method *}
+                    --{* @{text mode}: invocation mode *}
+                    --{* @{text e}: reference to object*}
+                    --{* @{text mn}: field name*}   
+                    --{* @{text pTs}: types of parameters *}
+                    --{* @{text args}: the actual parameters/arguments *} 
+        | Methd qtname sig    --{*   (folded) method (see below) *}
+        | Body qtname stmt    --{* (unfolded) method body *}
+        | InsInitE stmt expr  
+                 --{* insertion of initialization before *}
+                 --{* evaluation of expr (technical term for smallstep sem.) *}
+        | Callee locals expr  --{* save callers locals in callee-Frame *}
+                              --{* (technical term for smallstep semantics) *}
 and  stmt
-	= Skip                  (* empty      statement *)
-	| Expr  expr            (* expression statement *)
-        | Lab   jump stmt       ("_\<bullet> _"(* labeled statement*)[      99,66]66)
-                                (* handles break *)
+	= Skip                  --{* empty      statement *}
+	| Expr  expr            --{* expression statement *}
+        | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
+                                --{* labeled statement; handles break *}
 	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
-	| If_   expr stmt stmt  ("If'(_') _ Else _"          [   80,79,79]70)
-	| Loop  label expr stmt ("_\<bullet> While'(_') _"           [   99,80,79]70)
-        | Do jump               (* break, continue, return *)
+	| If_   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
+	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
+        | Do jump               --{* break, continue, return *}
 	| Throw expr
-        | TryC  stmt
-	     qtname vname stmt ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
+        | TryC  stmt qtname vname stmt ("Try _ Catch'(_ _') _"  [79,99,80,79]70)
+             --{* @{term "Try c1 Catch(C vn) c2"} *} 
+             --{* @{text c1}: block were exception may be thrown *}
+             --{* @{text C}:  execption class to catch *}
+             --{* @{text vn}: local name for exception used in @{text c2}*}
+             --{* @{text c2}: block to execute when exception is cateched*}
 	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
-        | FinA abopt stmt        (* Save abruption of first statement 
-                                    (for smallstep sem.) *)
-	| Init  qtname              (* class initialization *)
+        | FinA abopt stmt       --{* Save abruption of first statement *} 
+                                --{* technical term  for smallstep sem.) *}
+	| Init  qtname          --{* class initialization *}
 
 
 text {*
@@ -220,7 +259,7 @@
  "!!v"        == "Acc (LVar (EName (VNam v)))"
  "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
  "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
-                                                   (* Res := e;; Do Ret *)
+                  --{* \tt Res := e;; Do Ret *}
  "StatRef rt" == "Cast (RefT rt) (Lit Null)"
   
 constdefs
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/Trans.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -11,7 +11,6 @@
 
 theory Trans = Evaln:
 
-
 constdefs groundVar:: "var \<Rightarrow> bool"
 "groundVar v \<equiv> (case v of
                    LVar ln \<Rightarrow> True
@@ -162,13 +161,19 @@
 BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
            \<Longrightarrow> 
            G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
-BinOpE2:  "\<lbrakk>G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
+BinOpE2:  "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
            \<Longrightarrow> 
            G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
             \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
+BinOpTerm:  "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk>
+             \<Longrightarrow> 
+             G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
+              \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
 BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
             \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
-
+(* Maybe its more convenient to add: need_second_arg as precondition to BinOp 
+   to make the choice between BinOpTerm and BinOp deterministic *)
+   
 Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
 
 AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -854,6 +854,10 @@
 
 subsection "accessibility"
 
+text {* 
+\par
+*} (* dummy text command to break paragraph for latex;
+              large paragraphs exhaust memory of debian pdflatex *)
 
 (* #### stat raus und gleich is_static f schreiben *) 
 theorem dynamic_field_access_ok:
@@ -1707,7 +1711,9 @@
   next
     case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
-    have hyp_e2: "PROP ?TypeSafe       s1  s2 (In1l e2) (In1 v2)" .
+    have hyp_e2: "PROP ?TypeSafe       s1  s2 
+                   (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
+                   (In1 v2)" .
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
     then obtain e1T e2T where
@@ -1716,20 +1722,22 @@
       wt_binop: "wt_binop G binop e1T e2T" and
              T: "T=Inl (PrimT (binop_type binop))"
       by (auto elim!: wt_elim_cases)
+    have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
+      by simp
     from conf_s0 wt_e1 
     obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
                   wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
           error_free_s1: "error_free s1"
       by (auto dest!: hyp_e1)
-    from conf_s1 wt_e2 error_free_s1
+    from conf_s1 wt_e2 wt_Skip error_free_s1
     obtain      conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
-                  wt_v2: "normal s2 \<longrightarrow> G,store s2\<turnstile>v2\<Colon>\<preceq>e2T" and
           error_free_s2: "error_free s2"
-      by (auto dest!: hyp_e2)
-    from wt_v1 wt_v2 wt_binop T
+      by (cases "need_second_arg binop v1")
+         (auto dest!: hyp_e2 )
+    from wt_binop T
     have "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
       by (cases binop) auto
-    with conf_s2 error_free_s2
+    with conf_s2 conf_s1 error_free_s2 error_free_s1
     show "s2\<Colon>\<preceq>(G, L) \<and>
           (normal s2 \<longrightarrow>
         G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
@@ -2364,6 +2372,12 @@
   qed
   then show ?thesis .
 qed
+
+text {* 
+
+
+*} (* dummy text command to break paragraph for latex;
+              large paragraphs exhaust memory of debian pdflatex *)
  
 corollary eval_ts: 
  "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T\<rbrakk> 
@@ -2395,4 +2409,22 @@
 apply (drule (3) eval_type_sound)
 apply clarsimp
 done
+
+lemma wf_eval_Fin: 
+  assumes wf:    "wf_prog G" and
+          wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
+        conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
+        eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
+        eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
+            s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
+  shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
+proof -
+  from eval_c1 wt_c1 wf conf_s0
+  have "error_free (x1,s1)"
+    by (auto dest: eval_type_sound)
+  with eval_c1 eval_c2 s3
+  show ?thesis
+    by - (rule eval.Fin, auto simp add: error_free_def)
+qed
+
 end
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/WellType.thy	Tue Jul 16 20:25:21 2002 +0200
@@ -216,6 +216,8 @@
 "binop_type Xor      = Boolean"
 "binop_type BitOr    = Integer"
 "binop_type Or       = Boolean"
+"binop_type CondAnd  = Boolean"
+"binop_type CondOr   = Boolean"
 
 consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
 primrec
@@ -239,8 +241,10 @@
 "wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 "wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
 "wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+"wt_binop G CondOr  t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
 
-      
+
 types tys  =        "ty + ty list"
 translations
   "tys"   <= (type) "ty + ty list"
diff -r 041d78bf9403 -r a34e38154413 src/HOL/Bali/document/root.tex
--- a/src/HOL/Bali/document/root.tex	Tue Jul 16 18:52:26 2002 +0200
+++ b/src/HOL/Bali/document/root.tex	Tue Jul 16 20:25:21 2002 +0200
@@ -152,6 +152,9 @@
 for the maximal recursive depth. The semantics is not altered. The annotation
 is needed for the soundness proof of the axiomatic semantics.
 
+\item[Trans]
+A smallstep operational semantics for JavaCard.
+
 \item[AxSem]
 An axiomatic semantics (Hoare logic) for JavaCard.
 
@@ -209,6 +212,8 @@
 
 \chapter{Evaln}
 \input{Evaln}         
+\chapter{Trans}
+\input{Trans}         
 \chapter{AxSem}
 \input{AxSem}      
 \chapter{AxSound}