Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
authorschirmer
Wed, 10 Jul 2002 15:07:02 +0200
changeset 13337 f75dfc606ac7
parent 13336 1bd21b082466
child 13338 20ca66539bef
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/ROOT.ML
src/HOL/Bali/State.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/Trans.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/AxCompl.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -467,6 +467,43 @@
 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: 
+"\<lbrakk>wf_prog G; G,A\<turnstile>{=:n} In1r stmt1\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1r stmt2\<succ> {G\<rightarrow>}\<rbrakk>
+ \<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In1r (stmt1 Finally stmt2)\<succ> {G\<rightarrow>}"
+apply (tactic "wt_conf_prepare_tac 1")
+apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s' \<and> s\<Colon>\<preceq>(G, L)) 
+\<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
+apply (tactic "forw_hyp_tac 1")
+apply (tactic "clarsimp_tac eval_css 1")
+apply (rule allI)
+apply (tactic "clarsimp_tac eval_css 1")
+apply (tactic "forw_hyp_tac 1")
+apply (tactic {* pair_tac "sb" 1 *})
+apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
+apply (rule wf_eval_Fin)
+apply auto
+done
+
 text {* For @{text MGFn_lemma} we need the wellformedness of the program to
 switch from the evaln-semantics to the eval-semantics cf. @{text MGFn_call}, 
 @{text MGFn_FVar}*}
@@ -483,14 +520,15 @@
 apply  (induct_tac "t")
 apply    (induct_tac "a")
 apply     fast+
-apply (rule var_expr_stmt.induct)
-(* 28 subgoals *)
-prefer 14 apply fast (* Methd *)
-prefer 13 apply (erule (3) MGFn_Call)
+apply (rule var_expr_stmt.induct) 
+(* 34 subgoals *)
+prefer 17 apply fast (* Methd *)
+prefer 16 apply (erule (3) MGFn_Call)
 prefer 2  apply (drule MGFn_Init,erule (2) MGFn_FVar)
 apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *)
-apply (erule_tac [23] MGFn_Init)
-prefer 18 apply (erule (1) MGFn_Loop)
+apply (erule_tac [29] MGFn_Init)
+prefer 23 apply (erule (1) MGFn_Loop)
+prefer 26 apply (erule (2) MGFn_Fin)
 apply (tactic "ALLGOALS compl_prepare_tac")
 
 apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1")
@@ -499,6 +537,8 @@
 apply  (erule MGFnD [THEN ax_NormalD])
 apply (tactic "forw_hyp_eval_Force_tac 1")
 
+apply (rule ax_derivs.InstInitV)
+
 apply (rule ax_derivs.NewC)
 apply (erule MGFn_InitD [THEN conseq2])
 apply (tactic "eval_Force_tac 1")
@@ -516,6 +556,12 @@
 
 apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1")
 apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1")
+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 (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")
 
@@ -541,6 +587,10 @@
 apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *})
 apply (erule (1) eval.Body)
 
+apply (rule ax_derivs.InstInitE)
+
+apply (rule ax_derivs.Callee)
+
 apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
 
 apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1")
@@ -576,14 +626,7 @@
 apply (tactic "clarsimp_tac eval_css 1")
 apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext])
 
-apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
-apply  (tactic "forw_hyp_eval_Force_tac 1")
-apply (rule allI)
-apply (tactic "forw_hyp_tac 1")
-apply (tactic {* pair_tac "sb" 1 *})
-apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
-apply (drule (1) eval.Fin)
-apply clarsimp
+apply (rule ax_derivs.FinA)
 
 apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1")
 
--- a/src/HOL/Bali/AxSem.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/AxSem.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -536,6 +536,16 @@
 
   Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
 
+  UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
+          \<Longrightarrow>
+          G,A\<turnstile>{Normal P} UnOp unop e-\<succ> {Q}"
+
+  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>
+    \<Longrightarrow>
+    G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}" 
+
   Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
 
   Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
@@ -583,7 +593,7 @@
   Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
                                  G,A\<turnstile>{Normal P} .Expr e. {Q}"
 
-  Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb (Break l)) .; Q}\<rbrakk> \<Longrightarrow>
+  Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
                            G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
 
   Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
@@ -627,6 +637,14 @@
               .init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
                                G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
 
+-- {* Some dummy rules for the intermediate terms @{text Callee},
+@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep 
+semantics.
+*}
+  InstInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
+  InstInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
+  Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
+  FinA:      " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
 axioms (** these terms are the same as above, but with generalized typing **)
   polymorphic_conseq:
         "\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
@@ -667,9 +685,9 @@
 apply              (fast intro: ax_derivs.asm)
 (*apply           (fast intro: ax_derivs.cut) *)
 apply            (fast intro: ax_derivs.weaken)
-apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
-(* 31 subgoals *)
-prefer 16 (* Methd *)
+apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) 
+(* 37 subgoals *)
+prefer 18 (* Methd *)
 apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
 apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
                      THEN_ALL_NEW Blast_tac) *})
@@ -696,7 +714,7 @@
 lemma weaken: 
  "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
 apply (erule ax_derivs.induct)
-(*36 subgoals*)
+(*42 subgoals*)
 apply       (tactic "ALLGOALS strip_tac")
 apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
          etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
@@ -708,7 +726,7 @@
 (*apply  (blast intro: ax_derivs.cut) *)
 apply   (fast intro: ax_derivs.weaken)
 apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
-(*31 subgoals*)
+(*37 subgoals*)
 apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
                    THEN_ALL_NEW Fast_tac) *})
 (*1 subgoal*)
--- a/src/HOL/Bali/AxSound.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/AxSound.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -313,17 +313,18 @@
   "\<forall>a vs D l. (P' a vs D l \<and> P a vs D l) \<Longrightarrow> \<forall>a vs D l. P a vs D l"
 by fast
 
+
 lemmas sound_lemmas = Init_sound Loop_sound Methd_sound
 
 lemma ax_sound2: "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts"
 apply (erule ax_derivs.induct)
-prefer 20 (* Call *)
+prefer 22 (* Call *)
 apply (erule (1) Call_sound) apply simp apply force apply force 
 
 apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW 
     eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *})
 
-apply(tactic "COND (has_fewer_prems(30+3)) (ALLGOALS sound_prepare_tac) no_tac")
+apply(tactic "COND (has_fewer_prems(30+9)) (ALLGOALS sound_prepare_tac) no_tac")
 
                (*empty*)
 apply        fast (* insert *)
@@ -336,7 +337,13 @@
 apply   (simp (no_asm_use) add: type_ok_def,fast)(* hazard *)
 apply  force (* Abrupt *)
 
-(* 25 subgoals *)
+prefer 28 apply (simp add: evaln_InsInitV)
+prefer 28 apply (simp add: evaln_InsInitE)
+prefer 28 apply (simp add: evaln_Callee)
+prefer 28 apply (simp add: evaln_FinA)
+
+(* 27 subgoals *)
+apply (tactic {* sound_elim_tac 1 *})
 apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *)
 apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset() 
                           delsimps [thm "all_empty"])) *})    (* Done *)
@@ -347,12 +354,11 @@
 apply (simp,simp,simp) 
 apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
 apply (tactic "ALLGOALS sound_valid2_tac")
-apply (tactic "TRYALL sound_forw_hyp_tac") (* Cast, Inst, Acc, Expr *)
+apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *)
 apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, 
   dtac spec], dtac conjunct2, smp_tac 1, 
   TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *})
-apply (frule_tac [14] x = x1 in conforms_NormI)  (* for Fin *)
-
+apply (frule_tac [15] x = x1 in conforms_NormI)  (* for Fin *)
 
 (* 15 subgoals *)
 (* FVar *)
@@ -383,6 +389,9 @@
 apply (rule conjI,blast)
 apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def)
 
+(* BinOp *)
+apply (tactic "sound_forw_hyp_tac 1")
+
 (* Ass *)
 apply (tactic "sound_forw_hyp_tac 1")
 apply (case_tac "aa")
--- a/src/HOL/Bali/Eval.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Eval.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -447,6 +447,43 @@
        
 section "evaluation judgments"
 
+consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
+primrec
+"eval_unop UPlus   v = Intg (the_Intg v)"
+"eval_unop UMinus  v = Intg (- (the_Intg v))"
+"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
+"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))"
+"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
+"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
+"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
+
+-- "Be aware of the explicit coercion of the shift distance to nat"
+"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
+"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
+"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
+
+"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
+"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
+"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
+"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
+
+"eval_binop Eq      v1 v2 = Bool (v1=v2)"
+"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
+"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+"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))"
+
+
 consts
   eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
   halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
@@ -513,7 +550,6 @@
   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)"
 
-
 inductive "eval G" intros
 
 (* propagation of abrupt completion *)
@@ -533,7 +569,7 @@
 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
 
   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
-                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
+                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
   (* cf. 14.2 *)
   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
 	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
@@ -573,9 +609,12 @@
 
   (* cf. 14.18.2 *)
   Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
-	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
-               G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
-
+	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
+          s3=(if (\<exists> err. x1=Some (Error err)) 
+              then (x1,s1) 
+              else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
+          \<Longrightarrow>
+          G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
   (* cf. 12.4.2, 8.5 *)
   Init:	"\<lbrakk>the (class G C) = c;
 	  if inited C (globs s0) then s3 = Norm s0
@@ -630,8 +669,12 @@
   (* cf. 15.7.1 *)
   Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
 
+  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> 
+         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
+   
   (* cf. 15.10.2 *)
   Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
 
@@ -666,11 +709,14 @@
 
   Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
-
+  (* The local variables l are just a dummy here. The are only used by
+     the smallstep semantics *)
   (* cf. 14.15, 12.4.1 *)
   Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
-
+           G\<turnstile>Norm s0 \<midarrow>Body D c
+            -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
+  (* The local variables l are just a dummy here. The are only used by
+     the smallstep semantics *)
 (* evaluation of variables *)
 
   (* cf. 15.13.1, 15.7.2 *)
@@ -704,21 +750,24 @@
 				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
 
 (* Rearrangement of premisses:
-[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
- 17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
- 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
- 27(AVar),22(Call)]
+[0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
+ 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
+ 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
+ 29(AVar),24(Call)]
 *)
 ML {*
 bind_thm ("eval_induct_", rearrange_prems 
-[0,1,2,8,4,28,29,25,15,16,
- 17,18,19,3,5,23,24,21,6,
- 7,11,9,13,14,12,20,10,26,
- 27,22] (thm "eval.induct"))
+[0,1,2,8,4,30,31,27,15,16,
+ 17,18,19,20,21,3,5,25,26,23,6,
+ 7,11,9,13,14,12,22,10,28,
+ 29,24] (thm "eval.induct"))
 *}
 
+
+
 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
-   and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and 
+   and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
+   and and 
    s2 (* Fin *) and and s2 (* NewC *)] 
 
 declare split_if     [split del] split_if_asm     [split del] 
@@ -757,6 +806,8 @@
 	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"
+        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> vs'"
+        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"
@@ -802,6 +853,7 @@
 apply auto
 done
 
+
 ML_setup {*
 fun eval_fun nam inj rhs =
 let
@@ -827,6 +879,68 @@
 
 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
 
+text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
+used in smallstep semantics, not in the bigstep semantics. So their is no
+valid evaluation of these terms 
+*}
+
+
+lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1l (Callee l e)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }  
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
+
+lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1l (InsInitE c e)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
+lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In2 (InsInitV c w)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }  
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
+lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1r (FinA a c)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }  
+  then show ?thesis
+    by (cases s') fastsimp 
+qed
 
 lemma eval_no_abrupt_lemma: 
    "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
@@ -909,7 +1023,8 @@
 apply (case_tac "s", case_tac "a = None")
 by (auto intro!: eval.If)
 
-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'"
+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'"
 apply (case_tac "s", case_tac "a = None")
 by (auto intro!: eval.Methd)
 
@@ -979,7 +1094,8 @@
 *)
 
 lemma eval_Methd: 
-  "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')"
+  "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')"
 apply (case_tac "s")
 apply (case_tac "a")
 apply clarsimp+
@@ -1025,6 +1141,12 @@
 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
 by auto
 
+lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
+                   res=the (locals (store s2) Result);
+                   s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>
+ G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"
+by (auto elim: eval.Body)
+
 lemma unique_eval [rule_format (no_asm)]: 
   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
 apply (case_tac "ws")
@@ -1033,18 +1155,18 @@
 apply (erule eval_induct)
 apply (tactic {* ALLGOALS (EVERY'
       [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
-(* 29 subgoals *)
-prefer 26 (* Try *) 
+(* 31 subgoals *)
+prefer 28 (* Try *) 
 apply (simp (no_asm_use) only: split add: split_if_asm)
-(* 32 subgoals *)
-prefer 28 (* Init *)
+(* 34 subgoals *)
+prefer 30 (* Init *)
 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
-prefer 24 (* While *)
+prefer 26 (* While *)
 apply (simp (no_asm_use) only: split add: split_if_asm, blast)
 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
 apply blast
-(* 31 subgoals *)
+(* 33 subgoals *)
 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
 done
 
--- a/src/HOL/Bali/Evaln.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Evaln.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -103,6 +103,12 @@
 
   Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
 
+  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> 
+         \<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"
 
   Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
@@ -128,7 +134,8 @@
 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
 
   Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
- G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
+         G\<turnstile>Norm s0 \<midarrow>Body D c
+          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
 
 (* evaluation of expression lists *)
 
@@ -148,7 +155,7 @@
 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
 
   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
-                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
+                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
 
   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
 	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
@@ -203,6 +210,8 @@
 	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
+        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> vs'"
+        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
@@ -262,6 +271,62 @@
 *}
 declare evaln_AbruptIs [intro!]
 
+lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1l (Callee l e)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }
+  then show ?thesis
+    by (cases s') fastsimp 
+qed
+
+lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1l (InsInitE c e)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
+lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In2 (InsInitV c w)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  }  
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
+lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
+proof -
+  { fix s t v s'
+    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
+         normal: "normal s" and
+         callee: "t=In1r (FinA a c)"
+    then have "False"
+    proof (induct)
+    qed (auto)
+  } 
+  then show ?thesis
+    by (cases s') fastsimp
+qed
+
 lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
  fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
 apply (erule evaln_cases , auto)
@@ -437,6 +502,14 @@
     case Lit
     show ?case by (rule eval.Lit)
   next
+    case UnOp
+    with wf show ?case
+      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)
+  next
     case Super
     show ?case by (rule eval.Super)
   next
@@ -494,11 +567,11 @@
          check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
       by simp
     have evaln_methd: 
-           "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
+     "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
     have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
     have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
     have hyp_methd: "PROP ?EqEval ?InitLvars s4 
-                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
+              (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
@@ -556,7 +629,7 @@
       moreover
       from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
       obtain "s4=s3'"
-	 "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	by auto
       moreover note False
       ultimately have
@@ -591,7 +664,7 @@
 	moreover
 	from eq_s3'_s3 np evaln_methd init_lvars
 	obtain "s4=s3'"
-	  "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	  by auto
 	moreover note np 
 	ultimately have
@@ -674,7 +747,7 @@
             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
 	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
 	  by - (drule wf_mdecl_bodyD,
-                simp cong add: lname.case_cong ename.case_cong)
+                auto simp: cong add: lname.case_cong ename.case_cong)
 	with dynM' iscls_invDeclC invDeclC'
 	have
 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
@@ -873,10 +946,28 @@
     show ?case
       by (rule eval.Try)
   next
-    case Fin
-    with wf show ?case
-      by -(erule wt_elim_cases, blast intro!: eval.Fin
-           dest: eval_type_sound intro: conforms_NormI)
+    case (Fin c1 c2 n s0 s1 s2 x1 L accC T)
+    have hyp_c1: "PROP ?EqEval (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
+    have hyp_c2: "PROP ?EqEval (Norm s1) (s2) (In1r c2) \<diamondsuit>" .
+    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
+    then obtain
+      wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
+      wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>" 
+      by (rule wt_elim_cases) blast
+    from conf_s0 wt_c1
+    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)"
+      by (rule hyp_c1)
+    with wf wt_c1 conf_s0
+    obtain       conf_s1: "Norm s1\<Colon>\<preceq>(G, L)" and 
+           error_free_s1: "error_free (x1,s1)"
+      by (auto dest!: eval_type_sound intro: conforms_NormI)
+    from conf_s1 wt_c2
+    have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2"
+      by (rule hyp_c2)
+    with eval_c1 error_free_s1
+    show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
+      by (auto intro: eval.Fin simp add: error_free_def)
   next
     case (Init C c n s0 s1 s2 s3 L accC T)
     have     cls: "the (class G C) = c" .
@@ -994,8 +1085,6 @@
   show ?thesis .
 qed
 
-text {* *} (* FIXME *)
-
 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  
@@ -1029,7 +1118,7 @@
     then obtain n where
       "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
       by (rules elim!: wt_elim_cases)
-    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
+    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
       by (rule evaln.Lab)
     then show ?case ..
   next
@@ -1209,16 +1298,22 @@
       by (auto intro!: evaln.Try le_maxI1 le_maxI2)
     then show ?case ..
   next
-    case (Fin c1 c2 s0 s1 s2 x1 L accC T)
-    with wf obtain n1 n2 where 
+    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
+    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
+                       then (x1, s1)
+                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+    from Fin wf obtain n1 n2 where 
       "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
-      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
+      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" and
+      error_free_s1: "error_free (x1,s1)"
       by (blast elim!: wt_elim_cases 
 	         dest: eval_type_sound intro: conforms_NormI)
     then have 
      "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
       by (blast intro: evaln.Fin dest: evaln_max2)
-    then show ?case ..
+    with error_free_s1 s3
+    show "\<exists>n. G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
+      by (auto simp add: error_free_def)
   next
     case (Init C c s0 s1 s2 s3 L accC T)
     have     cls: "the (class G C) = c" .
@@ -1340,6 +1435,24 @@
       by (rule evaln.Lit)
     then show ?case ..
   next
+    case (UnOp e s0 s1 unop v L accC T)
+    with wf obtain n where
+      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
+      by (rules elim!: wt_elim_cases)
+    hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
+      by (rule evaln.UnOp)
+    then show ?case ..
+  next
+    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)
+    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)
+    then show ?case ..
+  next
     case (Super s L accC T)
     have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
       by (rule evaln.Super)
@@ -1414,7 +1527,7 @@
     have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
     have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
     have hyp_methd: "PROP ?EqEval s3' s4 
-                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
+             (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
@@ -1475,7 +1588,7 @@
       moreover
       from eq_s3'_s3 False keep_abrupt eval_methd init_lvars
       obtain "s4=s3'"
-	 "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	by auto
       moreover note False evaln.Abrupt
       ultimately obtain m where 
@@ -1514,7 +1627,7 @@
 	moreover
 	from eq_s3'_s3 np eval_methd init_lvars
 	obtain "s4=s3'"
-	  "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
+      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
 	  by auto
 	moreover note np
 	ultimately obtain m where 
@@ -1600,7 +1713,7 @@
 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" 
 	  by - (drule wf_mdecl_bodyD,
-                simp cong add: lname.case_cong ename.case_cong)
+                auto simp: cong add: lname.case_cong ename.case_cong)
 	with dynM' iscls_invDeclC invDeclC'
 	have
 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
--- a/src/HOL/Bali/ROOT.ML	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/ROOT.ML	Wed Jul 10 15:07:02 2002 +0200
@@ -1,3 +1,5 @@
-use_thy "AxExample";
-use_thy "AxSound";
-use_thy "AxCompl";
+
+update_thy "AxExample";
+update_thy "AxSound";
+update_thy "AxCompl";
+update_thy "Trans";
--- a/src/HOL/Bali/State.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/State.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -223,13 +223,13 @@
 	= "(oref , obj) table"
 	heap
 	= "(loc  , obj) table"
-	locals
-	= "(lname, val) table" (* local variables *)
+(*	locals                   
+	= "(lname, val) table" *) (* defined in Value.thy local variables *)
 
 translations
  "globs"  <= (type) "(oref , obj) table"
  "heap"   <= (type) "(loc  , obj) table"
- "locals" <= (type) "(lname, val) table"
+(*  "locals" <= (type) "(lname, val) table" *)
 
 datatype st = (* pure state, i.e. contents of all variables *)
 	 st globs locals
@@ -487,18 +487,7 @@
 section "abrupt completion"
 
 
-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 *)
-
-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 *)
 consts
 
   the_Xcpt :: "abrupt \<Rightarrow> xcpt"
@@ -511,8 +500,7 @@
 primrec "the_Loc (Loc a) = a"
 primrec "the_Std (Std x) = x"
 
-types
-  abopt  = "abrupt option"
+
 	
 
 constdefs
--- a/src/HOL/Bali/Table.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Table.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -41,7 +41,7 @@
 
 syntax
   table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"    (* concrete table *)
-
+  
 translations
   "table_of" == "map_of"
   
--- a/src/HOL/Bali/Term.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Term.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -6,7 +6,7 @@
 
 header {* Java expressions and statements *}
 
-theory Term = Value:
+theory Term = Value + Table:
 
 text {*
 design issues:
@@ -58,6 +58,40 @@
 \end{itemize}
 *}
 
+
+
+types locals = "(lname, val) table"  (* local variables *)
+
+
+datatype jump
+        = 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 error
+       = 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 *)
+types
+  abopt  = "abrupt option"
+
+text {* Local variable store and exception. 
+Anticipation of State.thy used by smallstep semantics. For a method call, 
+we save the local variables of the caller in the term Callee to restore them 
+after method return. Also an exception must be restored after the finally
+statement *}
+
+translations
+ "locals" <= (type) "(lname, val) table"
+
 datatype inv_mode                  (* invocation mode for method calls *)
 	= Static                   (* static *)
 	| SuperM                   (* super  *)
@@ -71,71 +105,112 @@
   "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
   "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
 
-datatype jump
-        = Break label (* break *)
-        | Cont label  (* continue *)
-        | Ret         (* return from method *)
+-- "function codes for unary operations"
+datatype unop =  UPlus    -- "+ unary plus" 
+               | UMinus   -- "- unary minus"
+               | UBitNot  -- "~ bitwise NOT"
+               | UNot     -- "! logical complement"
+
+-- "function codes for binary operations"
+datatype binop = Mul     -- "*   multiplication"
+               | Div     -- "/   division"
+               | Mod     -- "%   remainder"
+               | Plus    -- "+   addition"
+               | Minus   -- "-   subtraction"
+               | LShift  -- "<<  left shift"
+               | RShift  -- ">>  signed right shift"
+               | RShiftU -- ">>> unsigned right shift"
+               | Less    -- "<   less than"
+               | Le      -- "<=  less than or equal"
+               | Greater -- ">   greater than"
+               | Ge      -- ">=  greater than or equal"
+               | Eq      -- "==  equal"
+               | Neq     -- "!=  not equal"
+               | BitAnd  -- "&   bitwise AND"
+               | And     -- "&   boolean AND"
+               | BitXor  -- "^   bitwise Xor"
+               | Xor     -- "^   boolean Xor"
+               | BitOr   -- "|   bitwise Or"
+               | Or      -- "|   boolean Or"
 
 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)
+	| AVar expr expr    (* array component *) ("_.[_]"[90,10   ]90)
+        | InsInitV stmt var (* insertion of initialization before
+                                   evaluation of var (for smallstep sem.) *)
 
 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 *)
-	| 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)" (* method call *)
-                  "(expr list)" ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
-        | Methd qtname sig          (*   (folded) method (see below) *)
-        | Body qtname stmt          (* (unfolded) method body *)
+	= 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 *)
+        
+	| 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) *)
 and  stmt
-	= Skip                     (* empty      statement *)
-	| Expr  expr               (* expression statement *)
-        | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
-                                   (* 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 *)
+	= Skip                  (* empty      statement *)
+	| Expr  expr            (* expression statement *)
+        | Lab   jump stmt       ("_\<bullet> _"(* labeled statement*)[      99,66]66)
+                                (* 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 *)
 	| Throw expr
         | TryC  stmt
-	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
-	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
+	     qtname vname stmt ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
+	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
+        | FinA abopt stmt        (* Save abruption of first statement 
+                                    (for smallstep sem.) *)
 	| Init  qtname              (* class initialization *)
 
 
 text {*
 The expressions Methd and Body are artificial program constructs, in the
 sense that they are not used to define a concrete Bali program. In the 
-evaluation semantic definition they are "generated on the fly" to decompose 
-the task to define the behaviour of the Call expression. They are crucial 
-for the axiomatic semantics to give a syntactic hook to insert 
-some assertions (cf. AxSem.thy, Eval.thy).
-Also the Init statement (to initialize a class on its first use) is inserted 
-in various places by the evaluation semantics.   
+operational semantic's they are "generated on the fly" 
+to decompose the task to define the behaviour of the Call expression. 
+They are crucial for the axiomatic semantics to give a syntactic hook to insert 
+some assertions (cf. AxSem.thy, Eval.thy). 
+The Init statement (to initialize a class on its first use) is 
+inserted in various places by the semantics. 
+Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
+smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
+local variables of the caller for method return. So ve avoid modelling a 
+frame stack.
+The InsInitV/E terms are only used by the smallstep semantics to model the
+intermediate steps of class-initialisation.
 *}
  
-types "term" = "(expr+stmt, var, expr list) sum3"
+types "term" = "(expr+stmt,var,expr list) sum3"
 translations
   "sig"   <= (type) "mname \<times> ty list"
   "var"   <= (type) "Term.var"
   "expr"  <= (type) "Term.expr"
   "stmt"  <= (type) "Term.stmt"
-  "term"  <= (type) "(expr+stmt, var, expr list) sum3"
+  "term"  <= (type) "(expr+stmt,var,expr list) sum3"
 
 syntax
   
   this    :: expr
-  LAcc    :: "vname \<Rightarrow>         expr" ("!!")
-  LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
+  LAcc    :: "vname \<Rightarrow> expr" ("!!")
+  LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   Return  :: "expr \<Rightarrow> stmt"
   StatRef :: "ref_ty \<Rightarrow> expr"
 
--- a/src/HOL/Bali/Trans.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/Trans.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -7,175 +7,434 @@
 execution of Java expressions and statements
 
 PRELIMINARY!!!!!!!!
-
-improvements over Java Specification 1.0 (cf. 15.11.4.4):
-* dynamic method lookup does not need to check the return type
-* throw raises a NullPointer exception if a null reference is given, and each
-  throw of a system exception yield a fresh exception object (was not specified)
-* if there is not enough memory even to allocate an OutOfMemory exception,
-  evaluation/execution fails, i.e. simply stops (was not specified)
-
-design issues:
-* Lit expressions and Skip statements are considered completely evaluated.
-* the expr entry in rules is redundant in case of exceptions, but its full
-  inclusion helps to make the rule structure independent of exception occurence.
-* the rule format is such that the start state may contain an exception.
-  ++ faciliates exception handling (to be added later)
-  +  symmetry
-* the rules are defined carefully in order to be applicable even in not
-  type-correct situations (yielding undefined values),
-  e.g. the_Adr (Val (Bool b)) = arbitrary.
-  ++ fewer rules 
-  -  less readable because of auxiliary functions like the_Adr
-  Alternative: "defensive" evaluation throwing some InternalError exception
-               in case of (impossible, for correct programs) type mismatches
-
-simplifications:
-* just simple handling (i.e. propagation) of exceptions so far
-* dynamic method lookup does not check return type (should not be necessary)
 *)
 
-Trans = Eval +
+theory Trans = Evaln:
+(*
+constdefs inj_stmt:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 83)
+    "\<langle>s\<rangle>\<^sub>s \<equiv> In1r s"
+
+constdefs inj_expr:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 83)
+    "\<langle>e\<rangle>\<^sub>e \<equiv> In1l e"
+*)
+axclass inj_term < "type"
+consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
+
+instance stmt::inj_term ..
+
+defs (overloaded)
+stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+
+lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
+by (simp add: stmt_inj_term_def)
+
+instance expr::inj_term ..
+
+defs (overloaded)
+expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+
+lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
+by (simp add: expr_inj_term_def)
+
+instance var::inj_term ..
+
+defs (overloaded)
+var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+
+lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
+by (simp add: var_inj_term_def)
+
+instance "list":: (type) inj_term ..
+
+defs (overloaded)
+expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+
+lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
+by (simp add: expr_list_inj_term_def)
+
+constdefs groundVar:: "var \<Rightarrow> bool"
+"groundVar v \<equiv> (case v of
+                   LVar ln \<Rightarrow> True
+                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
+                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
+                 | InsInitV c v \<Rightarrow> False)"
+
+lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
+  assumes ground: "groundVar v" and
+          LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
+          FVar: "\<And> accC statDeclC stat a fn. 
+                    \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
+          AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+proof -
+  from ground LVar FVar AVar
+  show ?thesis
+    apply (cases v)
+    apply (simp add: groundVar_def)
+    apply (simp add: groundVar_def,blast)
+    apply (simp add: groundVar_def,blast)
+    apply (simp add: groundVar_def)
+    done
+qed
+
+constdefs groundExprs:: "expr list \<Rightarrow> bool"
+"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
+  
+consts the_val:: "expr \<Rightarrow> val"
+primrec
+"the_val (Lit v) = v"
+
+consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
+primrec
+"the_var G s (LVar ln)                    =(lvar ln (store s),s)"
+the_var_FVar_def:
+"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
+the_var_AVar_def:
+"the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
+
+lemma the_var_FVar_simp[simp]:
+"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
+by (simp)
+declare the_var_FVar_def [simp del]
+
+lemma the_var_AVar_simp:
+"the_var G s ((Lit a).[Lit i]) = avar G i a s"
+by (simp)
+declare the_var_AVar_def [simp del]
 
 consts
-  texpr_tstmt	:: "prog  (((expr  state)  (expr  state)) +
-		            ((stmt  state)  (stmt  state))) set"
+  step	:: "prog \<Rightarrow> ((term \<times> state) \<times> (term \<times> state)) set"
 
 syntax (symbols)
-  texpr :: "[prog, expr  state, expr  state]  bool "("__ 1 _"[61,82,82] 81)
-  tstmt :: "[prog, stmt  state, stmt  state]  bool "("__ 1 _"[61,82,82] 81)
-  Ref   :: "loc  expr"
+  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
+  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" 
+                                                  ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
+"step*":: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
+  Ref  :: "loc \<Rightarrow> expr"
+  SKIP :: "expr"
 
 translations
-
-  "Ge_s 1 ex_s'" == "Inl (e_s, ex_s')  texpr_tstmt G"
-  "Gs_s 1 s'_s'" == "Inr (s_s, s'_s')  texpr_tstmt G"
+  "G\<turnstile>p \<mapsto>1 p' " == "(p,p') \<in> step G"
+  "G\<turnstile>p \<mapsto>n p' " == "(p,p') \<in> (step G)^n"
+  "G\<turnstile>p \<mapsto>* p' " == "(p,p') \<in> (step G)\<^sup>*"
   "Ref a" == "Lit (Addr a)"
+  "SKIP"  == "Lit Unit"
 
-constdefs
-  
-  sub_expr_expr :: "(expr  expr)  prop"
-  "sub_expr_expr ef  (G e s e' s'. G(   e,s) 1 (   e',s') 
-				     G(ef e,s) 1 (ef e',s'))"
-
-inductive "texpr_tstmt G" intrs 
+inductive "step G" intros 
 
 (* evaluation of expression *)
   (* cf. 15.5 *)
-  XcptE	"v. e  Lit v 
-				  G(e,Some xc,s) 1 (Lit arbitrary,Some xc,s)"
-
- CastXX "PROP sub_expr_expr (Cast T)"
-
-(*
-  (* cf. 15.8.1 *)
-  NewC	"new_Addr (heap s) = Some (a,x);
-	  s' = assign (hupd[ainit_Obj G C]s) (x,s) 
-				G(NewC C,None,s) 1 (Ref a,s')"
-
-  (* cf. 15.9.1 *)
-(*NewA1	"sub_expr_expr (NewA T)"*)
-  NewA1	"G(e,None,s) 1 (e',s') 
-			      G(New T[e],None,s) 1 (New T[e'],s')"
-  NewA	"i = the_Intg i'; new_Addr (heap s) = Some (a, x);
-	  s' = assign (hupd[ainit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s) 
-			G(New T[Lit i'],None,s) 1 (Ref a,s')"
-  (* cf. 15.15 *)
-  Cast1	"G(e,None,s) 1 (e',s') 
-			      G(Cast T e,None,s) 1 (Cast T e',s')"
-  Cast	"x'= raise_if (\<questiondown>G,sv fits T) ClassCast None 
-		        G(Cast T (Lit v),None,s) 1 (Lit v,x',s)"
+Abrupt:	         "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
+                  \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
+                  \<forall> C vn c.  t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
+                  \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
+                  \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
+                \<Longrightarrow> 
+                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
 
-  (* cf. 15.7.1 *)
-(*Lit				"G(Lit v,None,s) 1 (Lit v,None,s)"*)
-
-  (* cf. 15.13.1, 15.2 *)
-  LAcc	"v = the (locals s vn) 
-			       G(LAcc vn,None,s) 1 (Lit v,None,s)"
-
-  (* cf. 15.25.1 *)
-  LAss1	"G(e,None,s) 1 (e',s') 
-				 G(f vn:=e,None,s) 1 (vn:=e',s')"
-  LAss			    "G(f vn:=Lit v,None,s) 1 (Lit v,None,lupd[vnv]s)"
+InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
+           \<Longrightarrow> 
+           G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
 
-  (* cf. 15.10.1, 15.2 *)
-  FAcc1	"G(e,None,s) 1 (e',s') 
-			       G({T}e..fn,None,s) 1 ({T}e'..fn,s')"
-  FAcc	"v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T)) 
-			  G({T}Lit a'..fn,None,s) 1 (Lit v,np a' None,s)"
-
-  (* cf. 15.25.1 *)
-  FAss1	"G(e1,None,s) 1 (e1',s') 
-			  G(f ({T}e1..fn):=e2,None,s) 1 (f({T}e1'..fn):=e2,s')"
-  FAss2	"G(e2,np a' None,s) 1 (e2',s') 
-		      G(f({T}Lit a'..fn):=e2,None,s) 1 (f({T}Lit a'..fn):=e2',s')"
-  FAss	"a = the_Addr a'; (c,fs) = the_Obj (heap s a);
-	  s'= assign (hupd[aObj c (fs[(fn,T)v])]s) (None,s) 
-		   G(f({T}Lit a'..fn):=Lit v,None,s) 1 (Lit v,s')"
-
-
+(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
+(* Specialised rules to evaluate: 
+   InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
+ 
+  (* cf. 15.8.1 *)
+NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
+NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
+             \<Longrightarrow> 
+             G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
 
 
 
-  (* cf. 15.12.1 *)
-  AAcc1	"G(e1,None,s) 1 (e1',s') 
-				G(e1[e2],None,s) 1 (e1'[e2],s')"
-  AAcc2	"G(e2,None,s) 1 (e2',s') 
-			    G(Lit a'[e2],None,s) 1 (Lit a'[e2'],s')"
-  AAcc	"vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
-	  x' = raise_if (vo = None) IndOutBound (np a' None) 
-			G(Lit a'[Lit i'],None,s) 1 (Lit (the vo),x',s)"
+(* Alternative when rule SeqE is present 
+NewCInited: "\<lbrakk>inited C (globs s); 
+              G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
+             \<Longrightarrow> 
+              G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
+
+NewC:
+     "\<lbrakk>\<not> inited C (globs s)\<rbrakk> 
+     \<Longrightarrow> 
+      G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
+
+*)
+  (* cf. 15.9.1 *)
+NewA: 
+   "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
+InsInitNewAIdx: 
+   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
+    \<Longrightarrow>  
+    G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
+InsInitNewA: 
+   "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
+    \<Longrightarrow>
+    G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
+ 
+  (* cf. 15.15 *)
+CastE:	
+   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
+    \<Longrightarrow>
+    G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
+Cast:	
+   "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
+    \<Longrightarrow> 
+    G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+  (* can be written without abupd, since we know Norm s *)
 
 
-  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
-  Call1	"G(e,None,s) 1 (e',s') 
-			  G(e..mn({pT}p),None,s) 1 (e'..mn({pT}p),s')"
-  Call2	"G(p,None,s) 1 (p',s') 
-		     G(Lit a'..mn({pT}p),None,s) 1 (Lit a'..mn({pT}p'),s')"
-  Call	"a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
- 			   the (cmethd G (fst (the_Obj (h a))) (mn,pT)) 
-	    G(Lit a'..mn({pT}Lit pv),None,(h,l)) 1 
-      (Body blk res l,np a' x,(h,init_vals lvars[Thisa'][Supera'][pnpv]))"
-  Body1	"G(s0,None,s) 1 (s0',s') 
-		   G(Body s0    e      l,None,s) 1 (Body s0'  e  l,s')"
-  Body2	"G(e ,None,s) 1 (e',s') 
-		   G(Body Skip  e      l,None,s) 1 (Body Skip e' l,s')"
-  Body		  "G(Body Skip (Lit v) l,None,s) 1 (Lit v,None,(heap s,l))"
+InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
+        \<Longrightarrow> 
+        G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
+Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
+        \<Longrightarrow> 
+        G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
+
+  (* cf. 15.7.1 *)
+(*Lit				"G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
+
+UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
+         \<Longrightarrow> 
+         G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
+UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
+
+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>
+           \<Longrightarrow> 
+           G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
+            \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,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)"
+
+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>
+        \<Longrightarrow> 
+        G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
+Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
+       \<Longrightarrow>  
+       G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+
+(*
+AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
+AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
+          \<Longrightarrow>  
+          G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 
+           \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
+          \<Longrightarrow>  
+          G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
+*) 
+AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
+         \<Longrightarrow> 
+         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
+AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
+         \<Longrightarrow> 
+         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
+Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
+         \<Longrightarrow> 
+         G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
+
+CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
+        \<Longrightarrow> 
+        G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
+Cond:  "G\<turnstile>(\<langle>Lit b? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>if the_Bool b then e1 else e2\<rangle>,Norm s)"
+
+
+CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
+             \<Longrightarrow>
+	     G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
+              \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
+CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
+             \<Longrightarrow>
+	     G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
+              \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
+Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
+              D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
+              s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
+             \<Longrightarrow> 
+             G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
+              \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
+           
+Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
+             \<Longrightarrow> 
+             G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
+
+CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
+               \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
+
+Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
+
+Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
+
+InsInitBody: 
+    "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
+     \<Longrightarrow> 
+     G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
+InsInitBodyRet: 
+     "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
+       \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
+
+(*   LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
+  
+FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
+       \<Longrightarrow> 
+       G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
+        \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
+InsInitFVarE:
+      "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
+       \<Longrightarrow>
+       G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
+        \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
+InsInitFVar:
+      "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
+        \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
+--  {* Notice, that we do not have literal values for @{text vars}. 
+The rules for accessing variables (@{text Acc}) and assigning to variables 
+(@{text Ass}), test this with the predicate @{text groundVar}.  After 
+initialisation is done and the @{text FVar} is evaluated, we can't just 
+throw away the @{text InsInitFVar} term and return a literal value, as in the 
+cases of @{text New}  or @{text NewC}. Instead we just return the evaluated 
+@{text FVar} and test for initialisation in the rule @{text FVar}. 
+*}
+
+
+AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
+         \<Longrightarrow> 
+         G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
+
+AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
+         \<Longrightarrow> 
+         G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
+
+(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
+
+(* evaluation of expression lists *)
+
+  -- {* @{text Nil}  is fully evaluated *}
+
+ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
+         \<Longrightarrow>
+         G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
+  
+ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
+         \<Longrightarrow>
+         G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
 
 (* execution of statements *)
 
-  (* cf. 14.1 *)
-  XcptS	"s0  Skip 
-				 G(s0,Some xc,s) 1 (Skip,Some xc,s)"
-
   (* cf. 14.5 *)
-(*Skip	 			 "G(Skip,None,s) 1 (Skip,None,s)"*)
+Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
 
-  (* cf. 14.2 *)
-  Comp1	"G(s1,None,s) 1 (s1',s') 
-			       G(s1;; s2,None,s) 1 (s1';; s2,s')"
-  Comp			    "G(Skip;; s2,None,s) 1 (s2,None,s)"
-
-
-
-
+ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
+        \<Longrightarrow> 
+        G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
+Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
 
 
-  (* cf. 14.7 *)
-  Expr1	"G(e ,None,s) 1 (e',s') 
-				G(Expr e,None,s) 1 (Expr e',s')"
-  Expr			 "G(Expr (Lit v),None,s) 1 (Skip,None,s)"
+LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
+       \<Longrightarrow>  
+       G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
+Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
+
+  (* cf. 14.2 *)
+CompC1:	"\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
+         \<Longrightarrow> 
+         G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
+
+Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
 
   (* cf. 14.8.2 *)
-  If1	"G(e ,None,s) 1 (e',s') 
-		      G(If(e) s1 Else s2,None,s) 1 (If(e') s1 Else s2,s')"
-  If		 "G(If(Lit v) s1 Else s2,None,s) 1 
-		    (if the_Bool v then s1 else s2,None,s)"
+IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
+      \<Longrightarrow>
+      G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
+If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
+       \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
 
   (* cf. 14.10, 14.10.1 *)
-  Loop			  "G(While(e) s0,None,s) 1 
-			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
+Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
+        \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
+
+Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
+
+ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
+         \<Longrightarrow>
+         G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
+Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
+
+TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
+        \<Longrightarrow>
+        G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
+Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
+        \<Longrightarrow>
+        G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
+         \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
+                              else (\<langle>Skip\<rangle>,s'))"
+
+FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
+        \<Longrightarrow>
+        G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
+
+Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
+
+FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
+        \<Longrightarrow>
+        G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
+FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
+
+
+Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
+        \<Longrightarrow> 
+        G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
+Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
+       \<Longrightarrow> 
+       G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
+        \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
+              Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
+             ,Norm (init_class_obj G C s))"
+-- {* @{text InsInitE} is just used as trick to embed the statement 
+@{text "init c"} into an expression*} 
+InsInitESKIP:
+  "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
+         
+(* Equivalenzen:
+  Bigstep zu Smallstep komplett.
+  Smallstep zu Bigstep, nur wenn nicht die Ausdrcke Callee, FinA ,\<dots>
 *)
-  con_defs "[sub_expr_expr_def]"
 
-end
+lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
+proof -
+  assume "p \<in> R\<^sup>*"
+  moreover obtain x y where p: "p = (x,y)" by (cases p)
+  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
+  hence "\<exists>n. (x,y) \<in> R^n"
+  proof induct
+    fix a have "(a,a) \<in> R^0" by simp
+    thus "\<exists>n. (a,a) \<in> R ^ n" ..
+  next
+    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
+    then obtain n where "(a,b) \<in> R^n" ..
+    moreover assume "(b,c) \<in> R"
+    ultimately have "(a,c) \<in> R^(Suc n)" by auto
+    thus "\<exists>n. (a,c) \<in> R^n" ..
+  qed
+  with p show ?thesis by hypsubst
+qed  
+
+(*
+lemma imp_eval_trans:
+  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
+    shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
+*)
+(* Jetzt muss man bei trans natrlich wieder unterscheiden: Stmt, Expr, Var!
+   Sowas bldes:
+   Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
+   the_vals definieren\<dots>
+  G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
+*)
+
+
+end
\ No newline at end of file
--- a/src/HOL/Bali/TypeSafe.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -173,7 +173,7 @@
   | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
   | In3 vs \<Rightarrow> True)"
 apply (erule eval_induct)
-prefer 24 
+prefer 26 
   apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
 apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
  simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
@@ -1257,13 +1257,13 @@
     obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
            error_free_s1: "error_free s1" 
       by (blast)
-    from conf_s1 have "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L)"
+    from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
       by (cases s1) (auto intro: conforms_absorb)
     with wt error_free_s1
-    show "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L) \<and>
-          (normal (abupd (absorb (Break l)) s1)
-           \<longrightarrow> G,L,store (abupd (absorb (Break l)) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
-          (error_free (Norm s0) = error_free (abupd (absorb (Break l)) s1))"
+    show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
+          (normal (abupd (absorb l) s1)
+           \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
+          (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
       by (simp)
   next
     case (Comp c1 c2 s0 s1 s2 L accC T)
@@ -1463,9 +1463,12 @@
       qed
     qed
   next
-    case (Fin c1 c2 s0 s1 s2 x1 L accC T)
+    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
     have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
     have c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
+    have s3: "s3= (if \<exists>err. x1 = Some (Error err) 
+                     then (x1, s1)
+                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
     have  hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
     have  hyp_c2: "PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>" .
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
@@ -1482,14 +1485,14 @@
     with wt_c2 hyp_c2
     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
       by blast
-    show "abupd (abrupt_if (x1 \<noteq> None) x1) s2\<Colon>\<preceq>(G, L) \<and>
-          (normal (abupd (abrupt_if (x1 \<noteq> None) x1) s2) 
-           \<longrightarrow> G,L,store (abupd (abrupt_if (x1 \<noteq> None) x1) s2)
-               \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
-          (error_free (Norm s0) =
-              error_free (abupd (abrupt_if (x1 \<noteq> None) x1) s2))"
+    from error_free_s1 s3 
+    have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
+      by simp
+    show "s3\<Colon>\<preceq>(G, L) \<and>
+          (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
+          (error_free (Norm s0) = error_free s3)"
     proof (cases x1)
-      case None with conf_s2 wt show ?thesis by auto
+      case None with conf_s2 s3' wt show ?thesis by auto
     next
       case (Some x) 
       with c2 wf conf_s1 conf_s2
@@ -1501,7 +1504,7 @@
       with error_free_s2
       have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
 	by (cases s2) simp
-      with Some wt conf show ?thesis
+      with Some wt conf s3' show ?thesis
 	by (cases s2) auto
     qed
   next
@@ -1679,6 +1682,60 @@
       by (auto elim!: wt_elim_cases 
                intro: conf_litval simp add: empty_dt_def)
   next
+    case (UnOp e s0 s1 unop v L accC T)
+    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
+    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
+    then obtain eT
+      where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
+            wt_unop: "wt_unop unop eT" and
+                  T: "T=Inl (PrimT (unop_type unop))" 
+      by (auto elim!: wt_elim_cases)
+    from conf_s0 wt_e 
+    obtain     conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
+                  wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
+         error_free_s1: "error_free s1"
+      by (auto dest!: hyp)
+    from wt_v T wt_unop
+    have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
+      by (cases unop) auto
+    with conf_s1 error_free_s1
+    show "s1\<Colon>\<preceq>(G, L) \<and>
+     (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T) \<and>
+     error_free (Norm s0) = error_free s1"
+      by simp
+  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 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
+         wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
+         wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
+      wt_binop: "wt_binop G binop e1T e2T" and
+             T: "T=Inl (PrimT (binop_type binop))"
+      by (auto elim!: wt_elim_cases)
+    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
+    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
+    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
+    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>
+          error_free (Norm s0) = error_free s2"
+      by simp
+  next
     case (Super s L accC T)
     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
@@ -1818,7 +1875,7 @@
     have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a')" .
     have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
     have hyp_methd: "PROP ?TypeSafe s3' s4 
-                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
+               (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
@@ -1995,7 +2052,7 @@
             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
 	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
 	  by - (drule wf_mdecl_bodyD,
-                simp cong add: lname.case_cong ename.case_cong)
+                auto simp: cong add: lname.case_cong ename.case_cong)
 	with dynM' iscls_invDeclC invDeclC'
 	have
 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
@@ -2031,14 +2088,14 @@
   next
     case (Methd D s0 s1 sig v L accC T)
     have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
-    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
+    have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
     then obtain m bodyT where
       D: "is_class G D" and
       m: "methd G D sig = Some m" and
       wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
-                   \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
+                  \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
       T: "T=Inl bodyT"
       by (rule wt_elim_cases) auto
     with hyp [of _ _ "(Inl bodyT)"] conf_s0 
@@ -2079,7 +2136,7 @@
     show "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L) \<and>
            (normal (abupd (absorb Ret) s2) \<longrightarrow>
              G,L,store (abupd (absorb Ret) s2)
-              \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
+             \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
           (error_free (Norm s0) = error_free (abupd (absorb Ret) s2)) "
       by (cases s2) (auto intro: conforms_locals)
   next
--- a/src/HOL/Bali/WellType.thy	Wed Jul 10 14:51:18 2002 +0200
+++ b/src/HOL/Bali/WellType.thy	Wed Jul 10 15:07:02 2002 +0200
@@ -180,7 +180,67 @@
 apply (clarsimp simp add: invmode_IntVir_eq)
 done
 
+consts unop_type :: "unop \<Rightarrow> prim_ty"
+primrec 
+"unop_type UPlus   = Integer"
+"unop_type UMinus  = Integer"
+"unop_type UBitNot = Integer"
+"unop_type UNot    = Boolean"    
 
+consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
+primrec
+"wt_unop UPlus   t = (t = PrimT Integer)"
+"wt_unop UMinus  t = (t = PrimT Integer)"
+"wt_unop UBitNot t = (t = PrimT Integer)"
+"wt_unop UNot    t = (t = PrimT Boolean)"
+
+consts binop_type :: "binop \<Rightarrow> prim_ty"
+primrec
+"binop_type Mul      = Integer"     
+"binop_type Div      = Integer"
+"binop_type Mod      = Integer"
+"binop_type Plus     = Integer"
+"binop_type Minus    = Integer"
+"binop_type LShift   = Integer"
+"binop_type RShift   = Integer"
+"binop_type RShiftU  = Integer"
+"binop_type Less     = Boolean"
+"binop_type Le       = Boolean"
+"binop_type Greater  = Boolean"
+"binop_type Ge       = Boolean"
+"binop_type Eq       = Boolean"
+"binop_type Neq      = Boolean"
+"binop_type BitAnd   = Integer"
+"binop_type And      = Boolean"
+"binop_type BitXor   = Integer"
+"binop_type Xor      = Boolean"
+"binop_type BitOr    = Integer"
+"binop_type Or       = Boolean"
+
+consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
+primrec
+"wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
+"wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
+"wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+"wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+"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))"
+
+      
 types tys  =        "ty + ty list"
 translations
   "tys"   <= (type) "ty + ty list"
@@ -237,6 +297,7 @@
 	"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
 
 
+
 inductive wt intros 
 
 
@@ -312,6 +373,15 @@
   Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
 					 E,dt\<Turnstile>Lit x\<Colon>-T"
 
+  UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
+          \<Longrightarrow>
+	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
+  
+  BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
+           T=PrimT (binop_type binop)\<rbrakk> 
+           \<Longrightarrow>
+	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
+  
   (* cf. 15.10.2, 15.11.1 *)
   Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
 	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
@@ -348,6 +418,9 @@
  (* The class C is the dynamic class of the method call (cf. Eval.thy). 
   * It hasn't got to be directly accessible from the current package (pkg E). 
   * Only the static class must be accessible (enshured indirectly by Call). 
+  * Note that l is just a dummy value. It is only used in the smallstep 
+  * semantics. To proof typesafety directly for the smallstep semantics 
+  * we would have to assume conformance of l here!
   *)
 
   Body:	"\<lbrakk>is_class (prg E) D;
@@ -359,7 +432,8 @@
    * from the current package (pkg E), but can also be indirectly accessible 
    * due to inheritance (enshured in Call)
    * The result type hasn't got to be accessible in Java! (If it is not 
-   * accessible you can only assign it to Object) 
+   * accessible you can only assign it to Object).
+   * For dummy value l see rule Methd. 
    *)
 
 (* well-typed variables *)
@@ -404,6 +478,8 @@
 	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
 	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
 	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
+        "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
+        "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
 	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
 	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
 	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
@@ -566,11 +642,11 @@
 apply (simp_all (no_asm_use) split del: split_if_asm)
 apply (safe del: disjE)
 (* 17 subgoals *)
-apply (tactic {* ALLGOALS (fn i => if i = 9 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
+apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
 (*apply (safe del: disjE elim!: wt_elim_cases)*)
 apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
 apply (simp_all (no_asm_use) split del: split_if_asm)
-apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
+apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
 apply ((blast del: equalityCE dest: sym [THEN trans])+)
 done