Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
authorschirmer
Wed Jul 10 15:07:02 2002 +0200 (2002-07-10)
changeset 13337f75dfc606ac7
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
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Wed Jul 10 14:51:18 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Wed Jul 10 15:07:02 2002 +0200
     1.3 @@ -467,6 +467,43 @@
     1.4  apply       (auto dest: eval_type_sound)
     1.5  done
     1.6  
     1.7 +(* FIXME To TypeSafe *)
     1.8 +lemma wf_eval_Fin: 
     1.9 +  assumes wf:    "wf_prog G" and
    1.10 +          wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
    1.11 +        conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
    1.12 +        eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
    1.13 +        eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
    1.14 +            s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
    1.15 +  shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
    1.16 +proof -
    1.17 +  from eval_c1 wt_c1 wf conf_s0
    1.18 +  have "error_free (x1,s1)"
    1.19 +    by (auto dest: eval_type_sound)
    1.20 +  with eval_c1 eval_c2 s3
    1.21 +  show ?thesis
    1.22 +    by - (rule eval.Fin, auto simp add: error_free_def)
    1.23 +qed
    1.24 +
    1.25 +text {* For @{text MGFn_Fin} we need the wellformedness of the program to
    1.26 +switch from the evaln-semantics to the eval-semantics *}
    1.27 +lemma MGFn_Fin: 
    1.28 +"\<lbrakk>wf_prog G; G,A\<turnstile>{=:n} In1r stmt1\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1r stmt2\<succ> {G\<rightarrow>}\<rbrakk>
    1.29 + \<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In1r (stmt1 Finally stmt2)\<succ> {G\<rightarrow>}"
    1.30 +apply (tactic "wt_conf_prepare_tac 1")
    1.31 +apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s' \<and> s\<Colon>\<preceq>(G, L)) 
    1.32 +\<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
    1.33 +apply (tactic "forw_hyp_tac 1")
    1.34 +apply (tactic "clarsimp_tac eval_css 1")
    1.35 +apply (rule allI)
    1.36 +apply (tactic "clarsimp_tac eval_css 1")
    1.37 +apply (tactic "forw_hyp_tac 1")
    1.38 +apply (tactic {* pair_tac "sb" 1 *})
    1.39 +apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
    1.40 +apply (rule wf_eval_Fin)
    1.41 +apply auto
    1.42 +done
    1.43 +
    1.44  text {* For @{text MGFn_lemma} we need the wellformedness of the program to
    1.45  switch from the evaln-semantics to the eval-semantics cf. @{text MGFn_call}, 
    1.46  @{text MGFn_FVar}*}
    1.47 @@ -483,14 +520,15 @@
    1.48  apply  (induct_tac "t")
    1.49  apply    (induct_tac "a")
    1.50  apply     fast+
    1.51 -apply (rule var_expr_stmt.induct)
    1.52 -(* 28 subgoals *)
    1.53 -prefer 14 apply fast (* Methd *)
    1.54 -prefer 13 apply (erule (3) MGFn_Call)
    1.55 +apply (rule var_expr_stmt.induct) 
    1.56 +(* 34 subgoals *)
    1.57 +prefer 17 apply fast (* Methd *)
    1.58 +prefer 16 apply (erule (3) MGFn_Call)
    1.59  prefer 2  apply (drule MGFn_Init,erule (2) MGFn_FVar)
    1.60  apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *)
    1.61 -apply (erule_tac [23] MGFn_Init)
    1.62 -prefer 18 apply (erule (1) MGFn_Loop)
    1.63 +apply (erule_tac [29] MGFn_Init)
    1.64 +prefer 23 apply (erule (1) MGFn_Loop)
    1.65 +prefer 26 apply (erule (2) MGFn_Fin)
    1.66  apply (tactic "ALLGOALS compl_prepare_tac")
    1.67  
    1.68  apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1")
    1.69 @@ -499,6 +537,8 @@
    1.70  apply  (erule MGFnD [THEN ax_NormalD])
    1.71  apply (tactic "forw_hyp_eval_Force_tac 1")
    1.72  
    1.73 +apply (rule ax_derivs.InstInitV)
    1.74 +
    1.75  apply (rule ax_derivs.NewC)
    1.76  apply (erule MGFn_InitD [THEN conseq2])
    1.77  apply (tactic "eval_Force_tac 1")
    1.78 @@ -516,6 +556,12 @@
    1.79  
    1.80  apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1")
    1.81  apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1")
    1.82 +apply (rule ax_derivs.UnOp, tactic "forw_hyp_eval_Force_tac 1")
    1.83 +
    1.84 +apply (rule ax_derivs.BinOp)
    1.85 +apply  (erule MGFnD [THEN ax_NormalD])
    1.86 +apply (tactic "forw_hyp_eval_Force_tac 1")
    1.87 +
    1.88  apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
    1.89  apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
    1.90  
    1.91 @@ -541,6 +587,10 @@
    1.92  apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *})
    1.93  apply (erule (1) eval.Body)
    1.94  
    1.95 +apply (rule ax_derivs.InstInitE)
    1.96 +
    1.97 +apply (rule ax_derivs.Callee)
    1.98 +
    1.99  apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
   1.100  
   1.101  apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1")
   1.102 @@ -576,14 +626,7 @@
   1.103  apply (tactic "clarsimp_tac eval_css 1")
   1.104  apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext])
   1.105  
   1.106 -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)
   1.107 -apply  (tactic "forw_hyp_eval_Force_tac 1")
   1.108 -apply (rule allI)
   1.109 -apply (tactic "forw_hyp_tac 1")
   1.110 -apply (tactic {* pair_tac "sb" 1 *})
   1.111 -apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
   1.112 -apply (drule (1) eval.Fin)
   1.113 -apply clarsimp
   1.114 +apply (rule ax_derivs.FinA)
   1.115  
   1.116  apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1")
   1.117  
     2.1 --- a/src/HOL/Bali/AxSem.thy	Wed Jul 10 14:51:18 2002 +0200
     2.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Jul 10 15:07:02 2002 +0200
     2.3 @@ -536,6 +536,16 @@
     2.4  
     2.5    Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
     2.6  
     2.7 +  UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
     2.8 +          \<Longrightarrow>
     2.9 +          G,A\<turnstile>{Normal P} UnOp unop e-\<succ> {Q}"
    2.10 +
    2.11 +  BinOp:
    2.12 +   "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
    2.13 +     \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} e2-\<succ> {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
    2.14 +    \<Longrightarrow>
    2.15 +    G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}" 
    2.16 +
    2.17    Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
    2.18  
    2.19    Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
    2.20 @@ -583,7 +593,7 @@
    2.21    Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
    2.22                                   G,A\<turnstile>{Normal P} .Expr e. {Q}"
    2.23  
    2.24 -  Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb (Break l)) .; Q}\<rbrakk> \<Longrightarrow>
    2.25 +  Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
    2.26                             G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
    2.27  
    2.28    Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
    2.29 @@ -627,6 +637,14 @@
    2.30                .init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
    2.31                                 G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
    2.32  
    2.33 +-- {* Some dummy rules for the intermediate terms @{text Callee},
    2.34 +@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep 
    2.35 +semantics.
    2.36 +*}
    2.37 +  InstInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
    2.38 +  InstInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
    2.39 +  Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
    2.40 +  FinA:      " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
    2.41  axioms (** these terms are the same as above, but with generalized typing **)
    2.42    polymorphic_conseq:
    2.43          "\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
    2.44 @@ -667,9 +685,9 @@
    2.45  apply              (fast intro: ax_derivs.asm)
    2.46  (*apply           (fast intro: ax_derivs.cut) *)
    2.47  apply            (fast intro: ax_derivs.weaken)
    2.48 -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)
    2.49 -(* 31 subgoals *)
    2.50 -prefer 16 (* Methd *)
    2.51 +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) 
    2.52 +(* 37 subgoals *)
    2.53 +prefer 18 (* Methd *)
    2.54  apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
    2.55  apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
    2.56                       THEN_ALL_NEW Blast_tac) *})
    2.57 @@ -696,7 +714,7 @@
    2.58  lemma weaken: 
    2.59   "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
    2.60  apply (erule ax_derivs.induct)
    2.61 -(*36 subgoals*)
    2.62 +(*42 subgoals*)
    2.63  apply       (tactic "ALLGOALS strip_tac")
    2.64  apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
    2.65           etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
    2.66 @@ -708,7 +726,7 @@
    2.67  (*apply  (blast intro: ax_derivs.cut) *)
    2.68  apply   (fast intro: ax_derivs.weaken)
    2.69  apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
    2.70 -(*31 subgoals*)
    2.71 +(*37 subgoals*)
    2.72  apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
    2.73                     THEN_ALL_NEW Fast_tac) *})
    2.74  (*1 subgoal*)
     3.1 --- a/src/HOL/Bali/AxSound.thy	Wed Jul 10 14:51:18 2002 +0200
     3.2 +++ b/src/HOL/Bali/AxSound.thy	Wed Jul 10 15:07:02 2002 +0200
     3.3 @@ -313,17 +313,18 @@
     3.4    "\<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"
     3.5  by fast
     3.6  
     3.7 +
     3.8  lemmas sound_lemmas = Init_sound Loop_sound Methd_sound
     3.9  
    3.10  lemma ax_sound2: "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts"
    3.11  apply (erule ax_derivs.induct)
    3.12 -prefer 20 (* Call *)
    3.13 +prefer 22 (* Call *)
    3.14  apply (erule (1) Call_sound) apply simp apply force apply force 
    3.15  
    3.16  apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW 
    3.17      eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *})
    3.18  
    3.19 -apply(tactic "COND (has_fewer_prems(30+3)) (ALLGOALS sound_prepare_tac) no_tac")
    3.20 +apply(tactic "COND (has_fewer_prems(30+9)) (ALLGOALS sound_prepare_tac) no_tac")
    3.21  
    3.22                 (*empty*)
    3.23  apply        fast (* insert *)
    3.24 @@ -336,7 +337,13 @@
    3.25  apply   (simp (no_asm_use) add: type_ok_def,fast)(* hazard *)
    3.26  apply  force (* Abrupt *)
    3.27  
    3.28 -(* 25 subgoals *)
    3.29 +prefer 28 apply (simp add: evaln_InsInitV)
    3.30 +prefer 28 apply (simp add: evaln_InsInitE)
    3.31 +prefer 28 apply (simp add: evaln_Callee)
    3.32 +prefer 28 apply (simp add: evaln_FinA)
    3.33 +
    3.34 +(* 27 subgoals *)
    3.35 +apply (tactic {* sound_elim_tac 1 *})
    3.36  apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *)
    3.37  apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset() 
    3.38                            delsimps [thm "all_empty"])) *})    (* Done *)
    3.39 @@ -347,12 +354,11 @@
    3.40  apply (simp,simp,simp) 
    3.41  apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
    3.42  apply (tactic "ALLGOALS sound_valid2_tac")
    3.43 -apply (tactic "TRYALL sound_forw_hyp_tac") (* Cast, Inst, Acc, Expr *)
    3.44 +apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *)
    3.45  apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, 
    3.46    dtac spec], dtac conjunct2, smp_tac 1, 
    3.47    TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *})
    3.48 -apply (frule_tac [14] x = x1 in conforms_NormI)  (* for Fin *)
    3.49 -
    3.50 +apply (frule_tac [15] x = x1 in conforms_NormI)  (* for Fin *)
    3.51  
    3.52  (* 15 subgoals *)
    3.53  (* FVar *)
    3.54 @@ -383,6 +389,9 @@
    3.55  apply (rule conjI,blast)
    3.56  apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def)
    3.57  
    3.58 +(* BinOp *)
    3.59 +apply (tactic "sound_forw_hyp_tac 1")
    3.60 +
    3.61  (* Ass *)
    3.62  apply (tactic "sound_forw_hyp_tac 1")
    3.63  apply (case_tac "aa")
     4.1 --- a/src/HOL/Bali/Eval.thy	Wed Jul 10 14:51:18 2002 +0200
     4.2 +++ b/src/HOL/Bali/Eval.thy	Wed Jul 10 15:07:02 2002 +0200
     4.3 @@ -447,6 +447,43 @@
     4.4         
     4.5  section "evaluation judgments"
     4.6  
     4.7 +consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
     4.8 +primrec
     4.9 +"eval_unop UPlus   v = Intg (the_Intg v)"
    4.10 +"eval_unop UMinus  v = Intg (- (the_Intg v))"
    4.11 +"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
    4.12 +"eval_unop UNot    v = Bool (\<not> the_Bool v)"
    4.13 +
    4.14 +consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
    4.15 +
    4.16 +
    4.17 +primrec
    4.18 +"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
    4.19 +"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
    4.20 +"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
    4.21 +"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
    4.22 +"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
    4.23 +
    4.24 +-- "Be aware of the explicit coercion of the shift distance to nat"
    4.25 +"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
    4.26 +"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
    4.27 +"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
    4.28 +
    4.29 +"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
    4.30 +"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
    4.31 +"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
    4.32 +"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
    4.33 +
    4.34 +"eval_binop Eq      v1 v2 = Bool (v1=v2)"
    4.35 +"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
    4.36 +"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
    4.37 +"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
    4.38 +"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
    4.39 +"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
    4.40 +"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
    4.41 +"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
    4.42 +
    4.43 +
    4.44  consts
    4.45    eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
    4.46    halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
    4.47 @@ -513,7 +550,6 @@
    4.48    SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
    4.49  	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
    4.50  
    4.51 -
    4.52  inductive "eval G" intros
    4.53  
    4.54  (* propagation of abrupt completion *)
    4.55 @@ -533,7 +569,7 @@
    4.56  				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
    4.57  
    4.58    Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
    4.59 -                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
    4.60 +                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
    4.61    (* cf. 14.2 *)
    4.62    Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
    4.63  	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
    4.64 @@ -573,9 +609,12 @@
    4.65  
    4.66    (* cf. 14.18.2 *)
    4.67    Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
    4.68 -	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
    4.69 -               G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
    4.70 -
    4.71 +	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
    4.72 +          s3=(if (\<exists> err. x1=Some (Error err)) 
    4.73 +              then (x1,s1) 
    4.74 +              else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
    4.75 +          \<Longrightarrow>
    4.76 +          G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
    4.77    (* cf. 12.4.2, 8.5 *)
    4.78    Init:	"\<lbrakk>the (class G C) = c;
    4.79  	  if inited C (globs s0) then s3 = Norm s0
    4.80 @@ -630,8 +669,12 @@
    4.81    (* cf. 15.7.1 *)
    4.82    Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
    4.83  
    4.84 +  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> 
    4.85 +         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
    4.86  
    4.87 -
    4.88 +  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<rightarrow> s2\<rbrakk> 
    4.89 +         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
    4.90 +   
    4.91    (* cf. 15.10.2 *)
    4.92    Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
    4.93  
    4.94 @@ -666,11 +709,14 @@
    4.95  
    4.96    Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
    4.97  				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
    4.98 -
    4.99 +  (* The local variables l are just a dummy here. The are only used by
   4.100 +     the smallstep semantics *)
   4.101    (* cf. 14.15, 12.4.1 *)
   4.102    Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   4.103 - G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
   4.104 -
   4.105 +           G\<turnstile>Norm s0 \<midarrow>Body D c
   4.106 +            -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
   4.107 +  (* The local variables l are just a dummy here. The are only used by
   4.108 +     the smallstep semantics *)
   4.109  (* evaluation of variables *)
   4.110  
   4.111    (* cf. 15.13.1, 15.7.2 *)
   4.112 @@ -704,21 +750,24 @@
   4.113  				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
   4.114  
   4.115  (* Rearrangement of premisses:
   4.116 -[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
   4.117 - 17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
   4.118 - 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
   4.119 - 27(AVar),22(Call)]
   4.120 +[0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
   4.121 + 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
   4.122 + 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
   4.123 + 29(AVar),24(Call)]
   4.124  *)
   4.125  ML {*
   4.126  bind_thm ("eval_induct_", rearrange_prems 
   4.127 -[0,1,2,8,4,28,29,25,15,16,
   4.128 - 17,18,19,3,5,23,24,21,6,
   4.129 - 7,11,9,13,14,12,20,10,26,
   4.130 - 27,22] (thm "eval.induct"))
   4.131 +[0,1,2,8,4,30,31,27,15,16,
   4.132 + 17,18,19,20,21,3,5,25,26,23,6,
   4.133 + 7,11,9,13,14,12,22,10,28,
   4.134 + 29,24] (thm "eval.induct"))
   4.135  *}
   4.136  
   4.137 +
   4.138 +
   4.139  lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
   4.140 -   and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and 
   4.141 +   and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
   4.142 +   and and 
   4.143     s2 (* Fin *) and and s2 (* NewC *)] 
   4.144  
   4.145  declare split_if     [split del] split_if_asm     [split del] 
   4.146 @@ -757,6 +806,8 @@
   4.147  	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"
   4.148  	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"
   4.149  	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"
   4.150 +        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> vs'"
   4.151 +        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> vs'"
   4.152  	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"
   4.153  	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"
   4.154  	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"
   4.155 @@ -802,6 +853,7 @@
   4.156  apply auto
   4.157  done
   4.158  
   4.159 +
   4.160  ML_setup {*
   4.161  fun eval_fun nam inj rhs =
   4.162  let
   4.163 @@ -827,6 +879,68 @@
   4.164  
   4.165  declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
   4.166  
   4.167 +text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
   4.168 +used in smallstep semantics, not in the bigstep semantics. So their is no
   4.169 +valid evaluation of these terms 
   4.170 +*}
   4.171 +
   4.172 +
   4.173 +lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
   4.174 +proof -
   4.175 +  { fix s t v s'
   4.176 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   4.177 +         normal: "normal s" and
   4.178 +         callee: "t=In1l (Callee l e)"
   4.179 +    then have "False"
   4.180 +    proof (induct)
   4.181 +    qed (auto)
   4.182 +  }  
   4.183 +  then show ?thesis
   4.184 +    by (cases s') fastsimp
   4.185 +qed
   4.186 +
   4.187 +
   4.188 +lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
   4.189 +proof -
   4.190 +  { fix s t v s'
   4.191 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   4.192 +         normal: "normal s" and
   4.193 +         callee: "t=In1l (InsInitE c e)"
   4.194 +    then have "False"
   4.195 +    proof (induct)
   4.196 +    qed (auto)
   4.197 +  }
   4.198 +  then show ?thesis
   4.199 +    by (cases s') fastsimp
   4.200 +qed
   4.201 +
   4.202 +lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
   4.203 +proof -
   4.204 +  { fix s t v s'
   4.205 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   4.206 +         normal: "normal s" and
   4.207 +         callee: "t=In2 (InsInitV c w)"
   4.208 +    then have "False"
   4.209 +    proof (induct)
   4.210 +    qed (auto)
   4.211 +  }  
   4.212 +  then show ?thesis
   4.213 +    by (cases s') fastsimp
   4.214 +qed
   4.215 +
   4.216 +lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
   4.217 +proof -
   4.218 +  { fix s t v s'
   4.219 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   4.220 +         normal: "normal s" and
   4.221 +         callee: "t=In1r (FinA a c)"
   4.222 +    then have "False"
   4.223 +    proof (induct)
   4.224 +    qed (auto)
   4.225 +  }  
   4.226 +  then show ?thesis
   4.227 +    by (cases s') fastsimp 
   4.228 +qed
   4.229  
   4.230  lemma eval_no_abrupt_lemma: 
   4.231     "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
   4.232 @@ -909,7 +1023,8 @@
   4.233  apply (case_tac "s", case_tac "a = None")
   4.234  by (auto intro!: eval.If)
   4.235  
   4.236 -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'"
   4.237 +lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' 
   4.238 +                \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
   4.239  apply (case_tac "s", case_tac "a = None")
   4.240  by (auto intro!: eval.Methd)
   4.241  
   4.242 @@ -979,7 +1094,8 @@
   4.243  *)
   4.244  
   4.245  lemma eval_Methd: 
   4.246 -  "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')"
   4.247 +  "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') 
   4.248 +   \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
   4.249  apply (case_tac "s")
   4.250  apply (case_tac "a")
   4.251  apply clarsimp+
   4.252 @@ -1025,6 +1141,12 @@
   4.253  lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
   4.254  by auto
   4.255  
   4.256 +lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
   4.257 +                   res=the (locals (store s2) Result);
   4.258 +                   s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>
   4.259 + G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"
   4.260 +by (auto elim: eval.Body)
   4.261 +
   4.262  lemma unique_eval [rule_format (no_asm)]: 
   4.263    "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
   4.264  apply (case_tac "ws")
   4.265 @@ -1033,18 +1155,18 @@
   4.266  apply (erule eval_induct)
   4.267  apply (tactic {* ALLGOALS (EVERY'
   4.268        [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
   4.269 -(* 29 subgoals *)
   4.270 -prefer 26 (* Try *) 
   4.271 +(* 31 subgoals *)
   4.272 +prefer 28 (* Try *) 
   4.273  apply (simp (no_asm_use) only: split add: split_if_asm)
   4.274 -(* 32 subgoals *)
   4.275 -prefer 28 (* Init *)
   4.276 +(* 34 subgoals *)
   4.277 +prefer 30 (* Init *)
   4.278  apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
   4.279 -prefer 24 (* While *)
   4.280 +prefer 26 (* While *)
   4.281  apply (simp (no_asm_use) only: split add: split_if_asm, blast)
   4.282  apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
   4.283  apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
   4.284  apply blast
   4.285 -(* 31 subgoals *)
   4.286 +(* 33 subgoals *)
   4.287  apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
   4.288  done
   4.289  
     5.1 --- a/src/HOL/Bali/Evaln.thy	Wed Jul 10 14:51:18 2002 +0200
     5.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Jul 10 15:07:02 2002 +0200
     5.3 @@ -103,6 +103,12 @@
     5.4  
     5.5    Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
     5.6  
     5.7 +  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
     5.8 +         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
     5.9 +
    5.10 +  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> 
    5.11 +         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
    5.12 +
    5.13    Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
    5.14  
    5.15    Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
    5.16 @@ -128,7 +134,8 @@
    5.17  				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
    5.18  
    5.19    Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
    5.20 - G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
    5.21 +         G\<turnstile>Norm s0 \<midarrow>Body D c
    5.22 +          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
    5.23  
    5.24  (* evaluation of expression lists *)
    5.25  
    5.26 @@ -148,7 +155,7 @@
    5.27  				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
    5.28  
    5.29    Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
    5.30 -                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
    5.31 +                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
    5.32  
    5.33    Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
    5.34  	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
    5.35 @@ -203,6 +210,8 @@
    5.36  	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
    5.37  	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
    5.38  	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
    5.39 +        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> vs'"
    5.40 +        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> vs'"
    5.41  	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
    5.42  	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
    5.43  	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
    5.44 @@ -262,6 +271,62 @@
    5.45  *}
    5.46  declare evaln_AbruptIs [intro!]
    5.47  
    5.48 +lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
    5.49 +proof -
    5.50 +  { fix s t v s'
    5.51 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
    5.52 +         normal: "normal s" and
    5.53 +         callee: "t=In1l (Callee l e)"
    5.54 +    then have "False"
    5.55 +    proof (induct)
    5.56 +    qed (auto)
    5.57 +  }
    5.58 +  then show ?thesis
    5.59 +    by (cases s') fastsimp 
    5.60 +qed
    5.61 +
    5.62 +lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
    5.63 +proof -
    5.64 +  { fix s t v s'
    5.65 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
    5.66 +         normal: "normal s" and
    5.67 +         callee: "t=In1l (InsInitE c e)"
    5.68 +    then have "False"
    5.69 +    proof (induct)
    5.70 +    qed (auto)
    5.71 +  }
    5.72 +  then show ?thesis
    5.73 +    by (cases s') fastsimp
    5.74 +qed
    5.75 +
    5.76 +lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
    5.77 +proof -
    5.78 +  { fix s t v s'
    5.79 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
    5.80 +         normal: "normal s" and
    5.81 +         callee: "t=In2 (InsInitV c w)"
    5.82 +    then have "False"
    5.83 +    proof (induct)
    5.84 +    qed (auto)
    5.85 +  }  
    5.86 +  then show ?thesis
    5.87 +    by (cases s') fastsimp
    5.88 +qed
    5.89 +
    5.90 +lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
    5.91 +proof -
    5.92 +  { fix s t v s'
    5.93 +    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
    5.94 +         normal: "normal s" and
    5.95 +         callee: "t=In1r (FinA a c)"
    5.96 +    then have "False"
    5.97 +    proof (induct)
    5.98 +    qed (auto)
    5.99 +  } 
   5.100 +  then show ?thesis
   5.101 +    by (cases s') fastsimp
   5.102 +qed
   5.103 +
   5.104  lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
   5.105   fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
   5.106  apply (erule evaln_cases , auto)
   5.107 @@ -437,6 +502,14 @@
   5.108      case Lit
   5.109      show ?case by (rule eval.Lit)
   5.110    next
   5.111 +    case UnOp
   5.112 +    with wf show ?case
   5.113 +      by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
   5.114 +  next
   5.115 +    case BinOp
   5.116 +    with wf show ?case
   5.117 +      by - (erule wt_elim_cases, blast intro!: eval.BinOp dest: eval_type_sound)
   5.118 +  next
   5.119      case Super
   5.120      show ?case by (rule eval.Super)
   5.121    next
   5.122 @@ -494,11 +567,11 @@
   5.123           check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
   5.124        by simp
   5.125      have evaln_methd: 
   5.126 -           "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
   5.127 +     "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
   5.128      have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
   5.129      have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
   5.130      have hyp_methd: "PROP ?EqEval ?InitLvars s4 
   5.131 -                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
   5.132 +              (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
   5.133      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   5.134      have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   5.135                      \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
   5.136 @@ -556,7 +629,7 @@
   5.137        moreover
   5.138        from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
   5.139        obtain "s4=s3'"
   5.140 -	 "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.141 +      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.142  	by auto
   5.143        moreover note False
   5.144        ultimately have
   5.145 @@ -591,7 +664,7 @@
   5.146  	moreover
   5.147  	from eq_s3'_s3 np evaln_methd init_lvars
   5.148  	obtain "s4=s3'"
   5.149 -	  "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.150 +      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.151  	  by auto
   5.152  	moreover note np 
   5.153  	ultimately have
   5.154 @@ -674,7 +747,7 @@
   5.155              \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
   5.156  	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
   5.157  	  by - (drule wf_mdecl_bodyD,
   5.158 -                simp cong add: lname.case_cong ename.case_cong)
   5.159 +                auto simp: cong add: lname.case_cong ename.case_cong)
   5.160  	with dynM' iscls_invDeclC invDeclC'
   5.161  	have
   5.162  	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
   5.163 @@ -873,10 +946,28 @@
   5.164      show ?case
   5.165        by (rule eval.Try)
   5.166    next
   5.167 -    case Fin
   5.168 -    with wf show ?case
   5.169 -      by -(erule wt_elim_cases, blast intro!: eval.Fin
   5.170 -           dest: eval_type_sound intro: conforms_NormI)
   5.171 +    case (Fin c1 c2 n s0 s1 s2 x1 L accC T)
   5.172 +    have hyp_c1: "PROP ?EqEval (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
   5.173 +    have hyp_c2: "PROP ?EqEval (Norm s1) (s2) (In1r c2) \<diamondsuit>" .
   5.174 +    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   5.175 +    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
   5.176 +    then obtain
   5.177 +      wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   5.178 +      wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>" 
   5.179 +      by (rule wt_elim_cases) blast
   5.180 +    from conf_s0 wt_c1
   5.181 +    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)"
   5.182 +      by (rule hyp_c1)
   5.183 +    with wf wt_c1 conf_s0
   5.184 +    obtain       conf_s1: "Norm s1\<Colon>\<preceq>(G, L)" and 
   5.185 +           error_free_s1: "error_free (x1,s1)"
   5.186 +      by (auto dest!: eval_type_sound intro: conforms_NormI)
   5.187 +    from conf_s1 wt_c2
   5.188 +    have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2"
   5.189 +      by (rule hyp_c2)
   5.190 +    with eval_c1 error_free_s1
   5.191 +    show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
   5.192 +      by (auto intro: eval.Fin simp add: error_free_def)
   5.193    next
   5.194      case (Init C c n s0 s1 s2 s3 L accC T)
   5.195      have     cls: "the (class G C) = c" .
   5.196 @@ -994,8 +1085,6 @@
   5.197    show ?thesis .
   5.198  qed
   5.199  
   5.200 -text {* *} (* FIXME *)
   5.201 -
   5.202  lemma eval_evaln: 
   5.203    assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
   5.204              wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
   5.205 @@ -1029,7 +1118,7 @@
   5.206      then obtain n where
   5.207        "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
   5.208        by (rules elim!: wt_elim_cases)
   5.209 -    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb (Break l)) s1"
   5.210 +    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   5.211        by (rule evaln.Lab)
   5.212      then show ?case ..
   5.213    next
   5.214 @@ -1209,16 +1298,22 @@
   5.215        by (auto intro!: evaln.Try le_maxI1 le_maxI2)
   5.216      then show ?case ..
   5.217    next
   5.218 -    case (Fin c1 c2 s0 s1 s2 x1 L accC T)
   5.219 -    with wf obtain n1 n2 where 
   5.220 +    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
   5.221 +    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
   5.222 +                       then (x1, s1)
   5.223 +                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
   5.224 +    from Fin wf obtain n1 n2 where 
   5.225        "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
   5.226 -      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   5.227 +      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" and
   5.228 +      error_free_s1: "error_free (x1,s1)"
   5.229        by (blast elim!: wt_elim_cases 
   5.230  	         dest: eval_type_sound intro: conforms_NormI)
   5.231      then have 
   5.232       "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
   5.233        by (blast intro: evaln.Fin dest: evaln_max2)
   5.234 -    then show ?case ..
   5.235 +    with error_free_s1 s3
   5.236 +    show "\<exists>n. G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
   5.237 +      by (auto simp add: error_free_def)
   5.238    next
   5.239      case (Init C c s0 s1 s2 s3 L accC T)
   5.240      have     cls: "the (class G C) = c" .
   5.241 @@ -1340,6 +1435,24 @@
   5.242        by (rule evaln.Lit)
   5.243      then show ?case ..
   5.244    next
   5.245 +    case (UnOp e s0 s1 unop v L accC T)
   5.246 +    with wf obtain n where
   5.247 +      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   5.248 +      by (rules elim!: wt_elim_cases)
   5.249 +    hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
   5.250 +      by (rule evaln.UnOp)
   5.251 +    then show ?case ..
   5.252 +  next
   5.253 +    case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
   5.254 +    with wf obtain n1 n2 where 
   5.255 +      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
   5.256 +      "G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n2\<rightarrow> s2"    
   5.257 +      by (blast elim!: wt_elim_cases dest: eval_type_sound)
   5.258 +    hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
   5.259 +           \<rightarrow> s2"
   5.260 +      by (blast intro!: evaln.BinOp dest: evaln_max2)
   5.261 +    then show ?case ..
   5.262 +  next
   5.263      case (Super s L accC T)
   5.264      have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   5.265        by (rule evaln.Super)
   5.266 @@ -1414,7 +1527,7 @@
   5.267      have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
   5.268      have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
   5.269      have hyp_methd: "PROP ?EqEval s3' s4 
   5.270 -                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
   5.271 +             (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
   5.272      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   5.273      have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   5.274                      \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
   5.275 @@ -1475,7 +1588,7 @@
   5.276        moreover
   5.277        from eq_s3'_s3 False keep_abrupt eval_methd init_lvars
   5.278        obtain "s4=s3'"
   5.279 -	 "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.280 +      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.281  	by auto
   5.282        moreover note False evaln.Abrupt
   5.283        ultimately obtain m where 
   5.284 @@ -1514,7 +1627,7 @@
   5.285  	moreover
   5.286  	from eq_s3'_s3 np eval_methd init_lvars
   5.287  	obtain "s4=s3'"
   5.288 -	  "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.289 +      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   5.290  	  by auto
   5.291  	moreover note np
   5.292  	ultimately obtain m where 
   5.293 @@ -1600,7 +1713,7 @@
   5.294  	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
   5.295              \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" 
   5.296  	  by - (drule wf_mdecl_bodyD,
   5.297 -                simp cong add: lname.case_cong ename.case_cong)
   5.298 +                auto simp: cong add: lname.case_cong ename.case_cong)
   5.299  	with dynM' iscls_invDeclC invDeclC'
   5.300  	have
   5.301  	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
     6.1 --- a/src/HOL/Bali/ROOT.ML	Wed Jul 10 14:51:18 2002 +0200
     6.2 +++ b/src/HOL/Bali/ROOT.ML	Wed Jul 10 15:07:02 2002 +0200
     6.3 @@ -1,3 +1,5 @@
     6.4 -use_thy "AxExample";
     6.5 -use_thy "AxSound";
     6.6 -use_thy "AxCompl";
     6.7 +
     6.8 +update_thy "AxExample";
     6.9 +update_thy "AxSound";
    6.10 +update_thy "AxCompl";
    6.11 +update_thy "Trans";
     7.1 --- a/src/HOL/Bali/State.thy	Wed Jul 10 14:51:18 2002 +0200
     7.2 +++ b/src/HOL/Bali/State.thy	Wed Jul 10 15:07:02 2002 +0200
     7.3 @@ -223,13 +223,13 @@
     7.4  	= "(oref , obj) table"
     7.5  	heap
     7.6  	= "(loc  , obj) table"
     7.7 -	locals
     7.8 -	= "(lname, val) table" (* local variables *)
     7.9 +(*	locals                   
    7.10 +	= "(lname, val) table" *) (* defined in Value.thy local variables *)
    7.11  
    7.12  translations
    7.13   "globs"  <= (type) "(oref , obj) table"
    7.14   "heap"   <= (type) "(loc  , obj) table"
    7.15 - "locals" <= (type) "(lname, val) table"
    7.16 +(*  "locals" <= (type) "(lname, val) table" *)
    7.17  
    7.18  datatype st = (* pure state, i.e. contents of all variables *)
    7.19  	 st globs locals
    7.20 @@ -487,18 +487,7 @@
    7.21  section "abrupt completion"
    7.22  
    7.23  
    7.24 -datatype xcpt        (* exception *)
    7.25 -	= Loc loc    (* location of allocated execption object *)
    7.26 -	| Std xname  (* intermediate standard exception, see Eval.thy *)
    7.27  
    7.28 -datatype error
    7.29 -       = AccessViolation (* Access to a member that isn't permitted *)
    7.30 -
    7.31 -datatype abrupt      (* abrupt completion *) 
    7.32 -        = Xcpt xcpt  (* exception *)
    7.33 -        | Jump jump  (* break, continue, return *)
    7.34 -        | Error error (* runtime errors, we wan't to detect and proof absent
    7.35 -                         in welltyped programms *)
    7.36  consts
    7.37  
    7.38    the_Xcpt :: "abrupt \<Rightarrow> xcpt"
    7.39 @@ -511,8 +500,7 @@
    7.40  primrec "the_Loc (Loc a) = a"
    7.41  primrec "the_Std (Std x) = x"
    7.42  
    7.43 -types
    7.44 -  abopt  = "abrupt option"
    7.45 +
    7.46  	
    7.47  
    7.48  constdefs
     8.1 --- a/src/HOL/Bali/Table.thy	Wed Jul 10 14:51:18 2002 +0200
     8.2 +++ b/src/HOL/Bali/Table.thy	Wed Jul 10 15:07:02 2002 +0200
     8.3 @@ -41,7 +41,7 @@
     8.4  
     8.5  syntax
     8.6    table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"    (* concrete table *)
     8.7 -
     8.8 +  
     8.9  translations
    8.10    "table_of" == "map_of"
    8.11    
     9.1 --- a/src/HOL/Bali/Term.thy	Wed Jul 10 14:51:18 2002 +0200
     9.2 +++ b/src/HOL/Bali/Term.thy	Wed Jul 10 15:07:02 2002 +0200
     9.3 @@ -6,7 +6,7 @@
     9.4  
     9.5  header {* Java expressions and statements *}
     9.6  
     9.7 -theory Term = Value:
     9.8 +theory Term = Value + Table:
     9.9  
    9.10  text {*
    9.11  design issues:
    9.12 @@ -58,6 +58,40 @@
    9.13  \end{itemize}
    9.14  *}
    9.15  
    9.16 +
    9.17 +
    9.18 +types locals = "(lname, val) table"  (* local variables *)
    9.19 +
    9.20 +
    9.21 +datatype jump
    9.22 +        = Break label (* break *)
    9.23 +        | Cont label  (* continue *)
    9.24 +        | Ret         (* return from method *)
    9.25 +
    9.26 +datatype xcpt        (* exception *)
    9.27 +	= Loc loc    (* location of allocated execption object *)
    9.28 +	| Std xname  (* intermediate standard exception, see Eval.thy *)
    9.29 +
    9.30 +datatype error
    9.31 +       = AccessViolation (* Access to a member that isn't permitted *)
    9.32 +
    9.33 +datatype abrupt      (* abrupt completion *) 
    9.34 +        = Xcpt xcpt  (* exception *)
    9.35 +        | Jump jump  (* break, continue, return *)
    9.36 +        | Error error (* runtime errors, we wan't to detect and proof absent
    9.37 +                         in welltyped programms *)
    9.38 +types
    9.39 +  abopt  = "abrupt option"
    9.40 +
    9.41 +text {* Local variable store and exception. 
    9.42 +Anticipation of State.thy used by smallstep semantics. For a method call, 
    9.43 +we save the local variables of the caller in the term Callee to restore them 
    9.44 +after method return. Also an exception must be restored after the finally
    9.45 +statement *}
    9.46 +
    9.47 +translations
    9.48 + "locals" <= (type) "(lname, val) table"
    9.49 +
    9.50  datatype inv_mode                  (* invocation mode for method calls *)
    9.51  	= Static                   (* static *)
    9.52  	| SuperM                   (* super  *)
    9.53 @@ -71,71 +105,112 @@
    9.54    "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
    9.55    "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
    9.56  
    9.57 -datatype jump
    9.58 -        = Break label (* break *)
    9.59 -        | Cont label  (* continue *)
    9.60 -        | Ret         (* return from method *)
    9.61 +-- "function codes for unary operations"
    9.62 +datatype unop =  UPlus    -- "+ unary plus" 
    9.63 +               | UMinus   -- "- unary minus"
    9.64 +               | UBitNot  -- "~ bitwise NOT"
    9.65 +               | UNot     -- "! logical complement"
    9.66 +
    9.67 +-- "function codes for binary operations"
    9.68 +datatype binop = Mul     -- "*   multiplication"
    9.69 +               | Div     -- "/   division"
    9.70 +               | Mod     -- "%   remainder"
    9.71 +               | Plus    -- "+   addition"
    9.72 +               | Minus   -- "-   subtraction"
    9.73 +               | LShift  -- "<<  left shift"
    9.74 +               | RShift  -- ">>  signed right shift"
    9.75 +               | RShiftU -- ">>> unsigned right shift"
    9.76 +               | Less    -- "<   less than"
    9.77 +               | Le      -- "<=  less than or equal"
    9.78 +               | Greater -- ">   greater than"
    9.79 +               | Ge      -- ">=  greater than or equal"
    9.80 +               | Eq      -- "==  equal"
    9.81 +               | Neq     -- "!=  not equal"
    9.82 +               | BitAnd  -- "&   bitwise AND"
    9.83 +               | And     -- "&   boolean AND"
    9.84 +               | BitXor  -- "^   bitwise Xor"
    9.85 +               | Xor     -- "^   boolean Xor"
    9.86 +               | BitOr   -- "|   bitwise Or"
    9.87 +               | Or      -- "|   boolean Or"
    9.88  
    9.89  datatype var
    9.90  	= LVar                  lname(* local variable (incl. parameters) *)
    9.91          | FVar qtname qtname bool expr vname
    9.92                                  (*class field*)("{_,_,_}_.._"[10,10,10,85,99]90)
    9.93 -	| AVar        expr expr      (* array component *) ("_.[_]"[90,10   ]90)
    9.94 +	| AVar expr expr    (* array component *) ("_.[_]"[90,10   ]90)
    9.95 +        | InsInitV stmt var (* insertion of initialization before
    9.96 +                                   evaluation of var (for smallstep sem.) *)
    9.97  
    9.98  and expr
    9.99 -	= NewC qtname              (* class instance creation *)
   9.100 -	| NewA ty expr             (* array creation *) ("New _[_]"[99,10   ]85)
   9.101 -	| Cast ty expr             (* type cast  *)
   9.102 -	| Inst expr ref_ty         (* instanceof *)     ("_ InstOf _"[85,99] 85)
   9.103 -	| Lit  val                 (* literal value, references not allowed *)
   9.104 -	| Super                    (* special Super keyword *)
   9.105 -	| Acc  var                 (* variable access *)
   9.106 -	| Ass  var expr            (* variable assign *) ("_:=_"   [90,85   ]85)
   9.107 -	| Cond expr expr expr      (* conditional *)  ("_ ? _ : _" [85,85,80]80)
   9.108 -        | Call qtname ref_ty inv_mode expr mname "(ty list)" (* method call *)
   9.109 -                  "(expr list)" ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
   9.110 -        | Methd qtname sig          (*   (folded) method (see below) *)
   9.111 -        | Body qtname stmt          (* (unfolded) method body *)
   9.112 +	= NewC qtname         (* class instance creation *)
   9.113 +	| NewA ty expr        (* array creation *) ("New _[_]"[99,10   ]85)
   9.114 +	| Cast ty expr        (* type cast  *)
   9.115 +	| Inst expr ref_ty    (* instanceof *)     ("_ InstOf _"[85,99] 85)
   9.116 +	| Lit  val            (* literal value, references not allowed *)
   9.117 +        | UnOp unop expr        (* unary operation *)
   9.118 +        | BinOp binop expr expr (* binary operation *)
   9.119 +        
   9.120 +	| Super               (* special Super keyword *)
   9.121 +	| Acc  var            (* variable access *)
   9.122 +	| Ass  var expr       (* variable assign *) ("_:=_"   [90,85   ]85)
   9.123 +	| Cond expr expr expr (* conditional *)  ("_ ? _ : _" [85,85,80]80)
   9.124 +        | Call qtname ref_ty inv_mode expr mname "(ty list)" 
   9.125 +               "(expr list)"  (* method call *) 
   9.126 +                              ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85)
   9.127 +        | Methd qtname sig    (*   (folded) method (see below) *)
   9.128 +        | Body qtname stmt    (* (unfolded) method body *)
   9.129 +        | InsInitE stmt expr      (* insertion of initialization before
   9.130 +                                   evaluation of expr (for smallstep sem.) *)
   9.131 +        | Callee locals expr      (* save Callers locals in Callee-Frame
   9.132 +                                     (for smallstep semantics) *)
   9.133  and  stmt
   9.134 -	= Skip                     (* empty      statement *)
   9.135 -	| Expr  expr               (* expression statement *)
   9.136 -        | Lab   label stmt         ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   9.137 -                                   (* handles break *)
   9.138 -	| Comp  stmt stmt          ("_;; _"                     [      66,65]65)
   9.139 -	| If_   expr stmt stmt     ("If'(_') _ Else _"          [   80,79,79]70)
   9.140 -	| Loop  label expr stmt    ("_\<bullet> While'(_') _"           [   99,80,79]70)
   9.141 -        | Do jump                  (* break, continue, return *)
   9.142 +	= Skip                  (* empty      statement *)
   9.143 +	| Expr  expr            (* expression statement *)
   9.144 +        | Lab   jump stmt       ("_\<bullet> _"(* labeled statement*)[      99,66]66)
   9.145 +                                (* handles break *)
   9.146 +	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
   9.147 +	| If_   expr stmt stmt  ("If'(_') _ Else _"          [   80,79,79]70)
   9.148 +	| Loop  label expr stmt ("_\<bullet> While'(_') _"           [   99,80,79]70)
   9.149 +        | Do jump               (* break, continue, return *)
   9.150  	| Throw expr
   9.151          | TryC  stmt
   9.152 -	        qtname vname stmt   ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   9.153 -	| Fin   stmt stmt          ("_ Finally _"               [      79,79]70)
   9.154 +	     qtname vname stmt ("Try _ Catch'(_ _') _"     [79,99,80,79]70)
   9.155 +	| Fin  stmt  stmt        ("_ Finally _"               [      79,79]70)
   9.156 +        | FinA abopt stmt        (* Save abruption of first statement 
   9.157 +                                    (for smallstep sem.) *)
   9.158  	| Init  qtname              (* class initialization *)
   9.159  
   9.160  
   9.161  text {*
   9.162  The expressions Methd and Body are artificial program constructs, in the
   9.163  sense that they are not used to define a concrete Bali program. In the 
   9.164 -evaluation semantic definition they are "generated on the fly" to decompose 
   9.165 -the task to define the behaviour of the Call expression. They are crucial 
   9.166 -for the axiomatic semantics to give a syntactic hook to insert 
   9.167 -some assertions (cf. AxSem.thy, Eval.thy).
   9.168 -Also the Init statement (to initialize a class on its first use) is inserted 
   9.169 -in various places by the evaluation semantics.   
   9.170 +operational semantic's they are "generated on the fly" 
   9.171 +to decompose the task to define the behaviour of the Call expression. 
   9.172 +They are crucial for the axiomatic semantics to give a syntactic hook to insert 
   9.173 +some assertions (cf. AxSem.thy, Eval.thy). 
   9.174 +The Init statement (to initialize a class on its first use) is 
   9.175 +inserted in various places by the semantics. 
   9.176 +Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the
   9.177 +smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the 
   9.178 +local variables of the caller for method return. So ve avoid modelling a 
   9.179 +frame stack.
   9.180 +The InsInitV/E terms are only used by the smallstep semantics to model the
   9.181 +intermediate steps of class-initialisation.
   9.182  *}
   9.183   
   9.184 -types "term" = "(expr+stmt, var, expr list) sum3"
   9.185 +types "term" = "(expr+stmt,var,expr list) sum3"
   9.186  translations
   9.187    "sig"   <= (type) "mname \<times> ty list"
   9.188    "var"   <= (type) "Term.var"
   9.189    "expr"  <= (type) "Term.expr"
   9.190    "stmt"  <= (type) "Term.stmt"
   9.191 -  "term"  <= (type) "(expr+stmt, var, expr list) sum3"
   9.192 +  "term"  <= (type) "(expr+stmt,var,expr list) sum3"
   9.193  
   9.194  syntax
   9.195    
   9.196    this    :: expr
   9.197 -  LAcc    :: "vname \<Rightarrow>         expr" ("!!")
   9.198 -  LAss    :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
   9.199 +  LAcc    :: "vname \<Rightarrow> expr" ("!!")
   9.200 +  LAss    :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85)
   9.201    Return  :: "expr \<Rightarrow> stmt"
   9.202    StatRef :: "ref_ty \<Rightarrow> expr"
   9.203  
    10.1 --- a/src/HOL/Bali/Trans.thy	Wed Jul 10 14:51:18 2002 +0200
    10.2 +++ b/src/HOL/Bali/Trans.thy	Wed Jul 10 15:07:02 2002 +0200
    10.3 @@ -7,175 +7,434 @@
    10.4  execution of Java expressions and statements
    10.5  
    10.6  PRELIMINARY!!!!!!!!
    10.7 -
    10.8 -improvements over Java Specification 1.0 (cf. 15.11.4.4):
    10.9 -* dynamic method lookup does not need to check the return type
   10.10 -* throw raises a NullPointer exception if a null reference is given, and each
   10.11 -  throw of a system exception yield a fresh exception object (was not specified)
   10.12 -* if there is not enough memory even to allocate an OutOfMemory exception,
   10.13 -  evaluation/execution fails, i.e. simply stops (was not specified)
   10.14 -
   10.15 -design issues:
   10.16 -* Lit expressions and Skip statements are considered completely evaluated.
   10.17 -* the expr entry in rules is redundant in case of exceptions, but its full
   10.18 -  inclusion helps to make the rule structure independent of exception occurence.
   10.19 -* the rule format is such that the start state may contain an exception.
   10.20 -  ++ faciliates exception handling (to be added later)
   10.21 -  +  symmetry
   10.22 -* the rules are defined carefully in order to be applicable even in not
   10.23 -  type-correct situations (yielding undefined values),
   10.24 -  e.g. the_Adr (Val (Bool b)) = arbitrary.
   10.25 -  ++ fewer rules 
   10.26 -  -  less readable because of auxiliary functions like the_Adr
   10.27 -  Alternative: "defensive" evaluation throwing some InternalError exception
   10.28 -               in case of (impossible, for correct programs) type mismatches
   10.29 -
   10.30 -simplifications:
   10.31 -* just simple handling (i.e. propagation) of exceptions so far
   10.32 -* dynamic method lookup does not check return type (should not be necessary)
   10.33  *)
   10.34  
   10.35 -Trans = Eval +
   10.36 +theory Trans = Evaln:
   10.37 +(*
   10.38 +constdefs inj_stmt:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 83)
   10.39 +    "\<langle>s\<rangle>\<^sub>s \<equiv> In1r s"
   10.40 +
   10.41 +constdefs inj_expr:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 83)
   10.42 +    "\<langle>e\<rangle>\<^sub>e \<equiv> In1l e"
   10.43 +*)
   10.44 +axclass inj_term < "type"
   10.45 +consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
   10.46 +
   10.47 +instance stmt::inj_term ..
   10.48 +
   10.49 +defs (overloaded)
   10.50 +stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
   10.51 +
   10.52 +lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
   10.53 +by (simp add: stmt_inj_term_def)
   10.54 +
   10.55 +instance expr::inj_term ..
   10.56 +
   10.57 +defs (overloaded)
   10.58 +expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
   10.59 +
   10.60 +lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
   10.61 +by (simp add: expr_inj_term_def)
   10.62 +
   10.63 +instance var::inj_term ..
   10.64 +
   10.65 +defs (overloaded)
   10.66 +var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
   10.67 +
   10.68 +lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
   10.69 +by (simp add: var_inj_term_def)
   10.70 +
   10.71 +instance "list":: (type) inj_term ..
   10.72 +
   10.73 +defs (overloaded)
   10.74 +expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   10.75 +
   10.76 +lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   10.77 +by (simp add: expr_list_inj_term_def)
   10.78 +
   10.79 +constdefs groundVar:: "var \<Rightarrow> bool"
   10.80 +"groundVar v \<equiv> (case v of
   10.81 +                   LVar ln \<Rightarrow> True
   10.82 +                 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
   10.83 +                 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
   10.84 +                 | InsInitV c v \<Rightarrow> False)"
   10.85 +
   10.86 +lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
   10.87 +  assumes ground: "groundVar v" and
   10.88 +          LVar: "\<And> ln. \<lbrakk>v=LVar ln\<rbrakk> \<Longrightarrow> P" and
   10.89 +          FVar: "\<And> accC statDeclC stat a fn. 
   10.90 +                    \<lbrakk>v={accC,statDeclC,stat}(Lit a)..fn\<rbrakk> \<Longrightarrow> P" and
   10.91 +          AVar: "\<And> a i. \<lbrakk>v=(Lit a).[Lit i]\<rbrakk> \<Longrightarrow> P"
   10.92 +  shows "P"
   10.93 +proof -
   10.94 +  from ground LVar FVar AVar
   10.95 +  show ?thesis
   10.96 +    apply (cases v)
   10.97 +    apply (simp add: groundVar_def)
   10.98 +    apply (simp add: groundVar_def,blast)
   10.99 +    apply (simp add: groundVar_def,blast)
  10.100 +    apply (simp add: groundVar_def)
  10.101 +    done
  10.102 +qed
  10.103 +
  10.104 +constdefs groundExprs:: "expr list \<Rightarrow> bool"
  10.105 +"groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
  10.106 +  
  10.107 +consts the_val:: "expr \<Rightarrow> val"
  10.108 +primrec
  10.109 +"the_val (Lit v) = v"
  10.110 +
  10.111 +consts the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)"
  10.112 +primrec
  10.113 +"the_var G s (LVar ln)                    =(lvar ln (store s),s)"
  10.114 +the_var_FVar_def:
  10.115 +"the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
  10.116 +the_var_AVar_def:
  10.117 +"the_var G s(a.[i])                       =avar G (the_val i) (the_val a) s"
  10.118 +
  10.119 +lemma the_var_FVar_simp[simp]:
  10.120 +"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
  10.121 +by (simp)
  10.122 +declare the_var_FVar_def [simp del]
  10.123 +
  10.124 +lemma the_var_AVar_simp:
  10.125 +"the_var G s ((Lit a).[Lit i]) = avar G i a s"
  10.126 +by (simp)
  10.127 +declare the_var_AVar_def [simp del]
  10.128  
  10.129  consts
  10.130 -  texpr_tstmt	:: "prog  (((expr  state)  (expr  state)) +
  10.131 -		            ((stmt  state)  (stmt  state))) set"
  10.132 +  step	:: "prog \<Rightarrow> ((term \<times> state) \<times> (term \<times> state)) set"
  10.133  
  10.134  syntax (symbols)
  10.135 -  texpr :: "[prog, expr  state, expr  state]  bool "("__ 1 _"[61,82,82] 81)
  10.136 -  tstmt :: "[prog, stmt  state, stmt  state]  bool "("__ 1 _"[61,82,82] 81)
  10.137 -  Ref   :: "loc  expr"
  10.138 +  step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
  10.139 +  stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" 
  10.140 +                                                  ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81)
  10.141 +"step*":: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81)
  10.142 +  Ref  :: "loc \<Rightarrow> expr"
  10.143 +  SKIP :: "expr"
  10.144  
  10.145  translations
  10.146 -
  10.147 -  "Ge_s 1 ex_s'" == "Inl (e_s, ex_s')  texpr_tstmt G"
  10.148 -  "Gs_s 1 s'_s'" == "Inr (s_s, s'_s')  texpr_tstmt G"
  10.149 +  "G\<turnstile>p \<mapsto>1 p' " == "(p,p') \<in> step G"
  10.150 +  "G\<turnstile>p \<mapsto>n p' " == "(p,p') \<in> (step G)^n"
  10.151 +  "G\<turnstile>p \<mapsto>* p' " == "(p,p') \<in> (step G)\<^sup>*"
  10.152    "Ref a" == "Lit (Addr a)"
  10.153 +  "SKIP"  == "Lit Unit"
  10.154  
  10.155 -constdefs
  10.156 -  
  10.157 -  sub_expr_expr :: "(expr  expr)  prop"
  10.158 -  "sub_expr_expr ef  (G e s e' s'. G(   e,s) 1 (   e',s') 
  10.159 -				     G(ef e,s) 1 (ef e',s'))"
  10.160 -
  10.161 -inductive "texpr_tstmt G" intrs 
  10.162 +inductive "step G" intros 
  10.163  
  10.164  (* evaluation of expression *)
  10.165    (* cf. 15.5 *)
  10.166 -  XcptE	"v. e  Lit v 
  10.167 -				  G(e,Some xc,s) 1 (Lit arbitrary,Some xc,s)"
  10.168 -
  10.169 - CastXX "PROP sub_expr_expr (Cast T)"
  10.170 -
  10.171 -(*
  10.172 -  (* cf. 15.8.1 *)
  10.173 -  NewC	"new_Addr (heap s) = Some (a,x);
  10.174 -	  s' = assign (hupd[ainit_Obj G C]s) (x,s) 
  10.175 -				G(NewC C,None,s) 1 (Ref a,s')"
  10.176 -
  10.177 -  (* cf. 15.9.1 *)
  10.178 -(*NewA1	"sub_expr_expr (NewA T)"*)
  10.179 -  NewA1	"G(e,None,s) 1 (e',s') 
  10.180 -			      G(New T[e],None,s) 1 (New T[e'],s')"
  10.181 -  NewA	"i = the_Intg i'; new_Addr (heap s) = Some (a, x);
  10.182 -	  s' = assign (hupd[ainit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s) 
  10.183 -			G(New T[Lit i'],None,s) 1 (Ref a,s')"
  10.184 -  (* cf. 15.15 *)
  10.185 -  Cast1	"G(e,None,s) 1 (e',s') 
  10.186 -			      G(Cast T e,None,s) 1 (Cast T e',s')"
  10.187 -  Cast	"x'= raise_if (\<questiondown>G,sv fits T) ClassCast None 
  10.188 -		        G(Cast T (Lit v),None,s) 1 (Lit v,x',s)"
  10.189 +Abrupt:	         "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>;
  10.190 +                  \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
  10.191 +                  \<forall> C vn c.  t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
  10.192 +                  \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
  10.193 +                  \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
  10.194 +                \<Longrightarrow> 
  10.195 +                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
  10.196  
  10.197 -  (* cf. 15.7.1 *)
  10.198 -(*Lit				"G(Lit v,None,s) 1 (Lit v,None,s)"*)
  10.199 -
  10.200 -  (* cf. 15.13.1, 15.2 *)
  10.201 -  LAcc	"v = the (locals s vn) 
  10.202 -			       G(LAcc vn,None,s) 1 (Lit v,None,s)"
  10.203 -
  10.204 -  (* cf. 15.25.1 *)
  10.205 -  LAss1	"G(e,None,s) 1 (e',s') 
  10.206 -				 G(f vn:=e,None,s) 1 (vn:=e',s')"
  10.207 -  LAss			    "G(f vn:=Lit v,None,s) 1 (Lit v,None,lupd[vnv]s)"
  10.208 +InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
  10.209 +           \<Longrightarrow> 
  10.210 +           G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
  10.211  
  10.212 -  (* cf. 15.10.1, 15.2 *)
  10.213 -  FAcc1	"G(e,None,s) 1 (e',s') 
  10.214 -			       G({T}e..fn,None,s) 1 ({T}e'..fn,s')"
  10.215 -  FAcc	"v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T)) 
  10.216 -			  G({T}Lit a'..fn,None,s) 1 (Lit v,np a' None,s)"
  10.217 -
  10.218 -  (* cf. 15.25.1 *)
  10.219 -  FAss1	"G(e1,None,s) 1 (e1',s') 
  10.220 -			  G(f ({T}e1..fn):=e2,None,s) 1 (f({T}e1'..fn):=e2,s')"
  10.221 -  FAss2	"G(e2,np a' None,s) 1 (e2',s') 
  10.222 -		      G(f({T}Lit a'..fn):=e2,None,s) 1 (f({T}Lit a'..fn):=e2',s')"
  10.223 -  FAss	"a = the_Addr a'; (c,fs) = the_Obj (heap s a);
  10.224 -	  s'= assign (hupd[aObj c (fs[(fn,T)v])]s) (None,s) 
  10.225 -		   G(f({T}Lit a'..fn):=Lit v,None,s) 1 (Lit v,s')"
  10.226 -
  10.227 -
  10.228 +(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
  10.229 +(* Specialised rules to evaluate: 
  10.230 +   InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
  10.231 + 
  10.232 +  (* cf. 15.8.1 *)
  10.233 +NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)"
  10.234 +NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
  10.235 +             \<Longrightarrow> 
  10.236 +             G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
  10.237  
  10.238  
  10.239  
  10.240 -  (* cf. 15.12.1 *)
  10.241 -  AAcc1	"G(e1,None,s) 1 (e1',s') 
  10.242 -				G(e1[e2],None,s) 1 (e1'[e2],s')"
  10.243 -  AAcc2	"G(e2,None,s) 1 (e2',s') 
  10.244 -			    G(Lit a'[e2],None,s) 1 (Lit a'[e2'],s')"
  10.245 -  AAcc	"vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
  10.246 -	  x' = raise_if (vo = None) IndOutBound (np a' None) 
  10.247 -			G(Lit a'[Lit i'],None,s) 1 (Lit (the vo),x',s)"
  10.248 +(* Alternative when rule SeqE is present 
  10.249 +NewCInited: "\<lbrakk>inited C (globs s); 
  10.250 +              G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
  10.251 +             \<Longrightarrow> 
  10.252 +              G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
  10.253 +
  10.254 +NewC:
  10.255 +     "\<lbrakk>\<not> inited C (globs s)\<rbrakk> 
  10.256 +     \<Longrightarrow> 
  10.257 +      G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
  10.258 +
  10.259 +*)
  10.260 +  (* cf. 15.9.1 *)
  10.261 +NewA: 
  10.262 +   "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)"
  10.263 +InsInitNewAIdx: 
  10.264 +   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk>
  10.265 +    \<Longrightarrow>  
  10.266 +    G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
  10.267 +InsInitNewA: 
  10.268 +   "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk>
  10.269 +    \<Longrightarrow>
  10.270 +    G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
  10.271 + 
  10.272 +  (* cf. 15.15 *)
  10.273 +CastE:	
  10.274 +   "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
  10.275 +    \<Longrightarrow>
  10.276 +    G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
  10.277 +Cast:	
  10.278 +   "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T)  ClassCast) (Norm s)\<rbrakk> 
  10.279 +    \<Longrightarrow> 
  10.280 +    G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
  10.281 +  (* can be written without abupd, since we know Norm s *)
  10.282  
  10.283  
  10.284 -  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
  10.285 -  Call1	"G(e,None,s) 1 (e',s') 
  10.286 -			  G(e..mn({pT}p),None,s) 1 (e'..mn({pT}p),s')"
  10.287 -  Call2	"G(p,None,s) 1 (p',s') 
  10.288 -		     G(Lit a'..mn({pT}p),None,s) 1 (Lit a'..mn({pT}p'),s')"
  10.289 -  Call	"a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
  10.290 - 			   the (cmethd G (fst (the_Obj (h a))) (mn,pT)) 
  10.291 -	    G(Lit a'..mn({pT}Lit pv),None,(h,l)) 1 
  10.292 -      (Body blk res l,np a' x,(h,init_vals lvars[Thisa'][Supera'][pnpv]))"
  10.293 -  Body1	"G(s0,None,s) 1 (s0',s') 
  10.294 -		   G(Body s0    e      l,None,s) 1 (Body s0'  e  l,s')"
  10.295 -  Body2	"G(e ,None,s) 1 (e',s') 
  10.296 -		   G(Body Skip  e      l,None,s) 1 (Body Skip e' l,s')"
  10.297 -  Body		  "G(Body Skip (Lit v) l,None,s) 1 (Lit v,None,(heap s,l))"
  10.298 +InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
  10.299 +        \<Longrightarrow> 
  10.300 +        G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
  10.301 +Inst:  "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
  10.302 +        \<Longrightarrow> 
  10.303 +        G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
  10.304 +
  10.305 +  (* cf. 15.7.1 *)
  10.306 +(*Lit				"G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
  10.307 +
  10.308 +UnOpE:  "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk>
  10.309 +         \<Longrightarrow> 
  10.310 +         G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
  10.311 +UnOp:   "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)"
  10.312 +
  10.313 +BinOpE1:  "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk>
  10.314 +           \<Longrightarrow> 
  10.315 +           G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
  10.316 +BinOpE2:  "\<lbrakk>G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk>
  10.317 +           \<Longrightarrow> 
  10.318 +           G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 
  10.319 +            \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
  10.320 +BinOp:    "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 
  10.321 +            \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
  10.322 +
  10.323 +Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)"
  10.324 +
  10.325 +AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk>
  10.326 +        \<Longrightarrow> 
  10.327 +        G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
  10.328 +Acc:  "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk>
  10.329 +       \<Longrightarrow>  
  10.330 +       G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
  10.331 +
  10.332 +(*
  10.333 +AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
  10.334 +AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
  10.335 +          \<Longrightarrow>  
  10.336 +          G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 
  10.337 +           \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
  10.338 +AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
  10.339 +          \<Longrightarrow>  
  10.340 +          G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
  10.341 +*) 
  10.342 +AssVA:  "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
  10.343 +         \<Longrightarrow> 
  10.344 +         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
  10.345 +AssE:   "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
  10.346 +         \<Longrightarrow> 
  10.347 +         G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
  10.348 +Ass:    "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 
  10.349 +         \<Longrightarrow> 
  10.350 +         G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
  10.351 +
  10.352 +CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
  10.353 +        \<Longrightarrow> 
  10.354 +        G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
  10.355 +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)"
  10.356 +
  10.357 +
  10.358 +CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
  10.359 +             \<Longrightarrow>
  10.360 +	     G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 
  10.361 +              \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
  10.362 +CallArgs:   "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 
  10.363 +             \<Longrightarrow>
  10.364 +	     G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
  10.365 +              \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
  10.366 +Call:       "\<lbrakk>groundExprs args; vs = map the_val args;
  10.367 +              D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
  10.368 +              s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 
  10.369 +             \<Longrightarrow> 
  10.370 +             G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 
  10.371 +              \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
  10.372 +           
  10.373 +Callee:     "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk>
  10.374 +             \<Longrightarrow> 
  10.375 +             G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
  10.376 +
  10.377 +CalleeRet:   "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
  10.378 +               \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
  10.379 +
  10.380 +Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)"
  10.381 +
  10.382 +Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)"
  10.383 +
  10.384 +InsInitBody: 
  10.385 +    "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
  10.386 +     \<Longrightarrow> 
  10.387 +     G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
  10.388 +InsInitBodyRet: 
  10.389 +     "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s)
  10.390 +       \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
  10.391 +
  10.392 +(*   LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
  10.393 +  
  10.394 +FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk>
  10.395 +       \<Longrightarrow> 
  10.396 +       G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 
  10.397 +        \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
  10.398 +InsInitFVarE:
  10.399 +      "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk>
  10.400 +       \<Longrightarrow>
  10.401 +       G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
  10.402 +        \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
  10.403 +InsInitFVar:
  10.404 +      "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
  10.405 +        \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
  10.406 +--  {* Notice, that we do not have literal values for @{text vars}. 
  10.407 +The rules for accessing variables (@{text Acc}) and assigning to variables 
  10.408 +(@{text Ass}), test this with the predicate @{text groundVar}.  After 
  10.409 +initialisation is done and the @{text FVar} is evaluated, we can't just 
  10.410 +throw away the @{text InsInitFVar} term and return a literal value, as in the 
  10.411 +cases of @{text New}  or @{text NewC}. Instead we just return the evaluated 
  10.412 +@{text FVar} and test for initialisation in the rule @{text FVar}. 
  10.413 +*}
  10.414 +
  10.415 +
  10.416 +AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
  10.417 +         \<Longrightarrow> 
  10.418 +         G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
  10.419 +
  10.420 +AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
  10.421 +         \<Longrightarrow> 
  10.422 +         G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
  10.423 +
  10.424 +(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
  10.425 +
  10.426 +(* evaluation of expression lists *)
  10.427 +
  10.428 +  -- {* @{text Nil}  is fully evaluated *}
  10.429 +
  10.430 +ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
  10.431 +         \<Longrightarrow>
  10.432 +         G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
  10.433 +  
  10.434 +ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
  10.435 +         \<Longrightarrow>
  10.436 +         G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
  10.437  
  10.438  (* execution of statements *)
  10.439  
  10.440 -  (* cf. 14.1 *)
  10.441 -  XcptS	"s0  Skip 
  10.442 -				 G(s0,Some xc,s) 1 (Skip,Some xc,s)"
  10.443 -
  10.444    (* cf. 14.5 *)
  10.445 -(*Skip	 			 "G(Skip,None,s) 1 (Skip,None,s)"*)
  10.446 +Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
  10.447  
  10.448 -  (* cf. 14.2 *)
  10.449 -  Comp1	"G(s1,None,s) 1 (s1',s') 
  10.450 -			       G(s1;; s2,None,s) 1 (s1';; s2,s')"
  10.451 -  Comp			    "G(Skip;; s2,None,s) 1 (s2,None,s)"
  10.452 -
  10.453 -
  10.454 -
  10.455 -
  10.456 +ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
  10.457 +        \<Longrightarrow> 
  10.458 +        G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
  10.459 +Expr:  "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
  10.460  
  10.461  
  10.462 -  (* cf. 14.7 *)
  10.463 -  Expr1	"G(e ,None,s) 1 (e',s') 
  10.464 -				G(Expr e,None,s) 1 (Expr e',s')"
  10.465 -  Expr			 "G(Expr (Lit v),None,s) 1 (Skip,None,s)"
  10.466 +LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
  10.467 +       \<Longrightarrow>  
  10.468 +       G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
  10.469 +Lab:  "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)"
  10.470 +
  10.471 +  (* cf. 14.2 *)
  10.472 +CompC1:	"\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
  10.473 +         \<Longrightarrow> 
  10.474 +         G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
  10.475 +
  10.476 +Comp:   "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)"
  10.477  
  10.478    (* cf. 14.8.2 *)
  10.479 -  If1	"G(e ,None,s) 1 (e',s') 
  10.480 -		      G(If(e) s1 Else s2,None,s) 1 (If(e') s1 Else s2,s')"
  10.481 -  If		 "G(If(Lit v) s1 Else s2,None,s) 1 
  10.482 -		    (if the_Bool v then s1 else s2,None,s)"
  10.483 +IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
  10.484 +      \<Longrightarrow>
  10.485 +      G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
  10.486 +If:  "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 
  10.487 +       \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
  10.488  
  10.489    (* cf. 14.10, 14.10.1 *)
  10.490 -  Loop			  "G(While(e) s0,None,s) 1 
  10.491 -			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
  10.492 +Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
  10.493 +        \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
  10.494 +
  10.495 +Do: "G\<turnstile>(\<langle>Do j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))"
  10.496 +
  10.497 +ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
  10.498 +         \<Longrightarrow>
  10.499 +         G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
  10.500 +Throw:  "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))"
  10.501 +
  10.502 +TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
  10.503 +        \<Longrightarrow>
  10.504 +        G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
  10.505 +Try:   "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk>
  10.506 +        \<Longrightarrow>
  10.507 +        G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 
  10.508 +         \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
  10.509 +                              else (\<langle>Skip\<rangle>,s'))"
  10.510 +
  10.511 +FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
  10.512 +        \<Longrightarrow>
  10.513 +        G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
  10.514 +
  10.515 +Fin:    "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)"
  10.516 +
  10.517 +FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk>
  10.518 +        \<Longrightarrow>
  10.519 +        G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
  10.520 +FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)"
  10.521 +
  10.522 +
  10.523 +Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
  10.524 +        \<Longrightarrow> 
  10.525 +        G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
  10.526 +Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk>  
  10.527 +       \<Longrightarrow> 
  10.528 +       G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 
  10.529 +        \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
  10.530 +              Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
  10.531 +             ,Norm (init_class_obj G C s))"
  10.532 +-- {* @{text InsInitE} is just used as trick to embed the statement 
  10.533 +@{text "init c"} into an expression*} 
  10.534 +InsInitESKIP:
  10.535 +  "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
  10.536 +         
  10.537 +(* Equivalenzen:
  10.538 +  Bigstep zu Smallstep komplett.
  10.539 +  Smallstep zu Bigstep, nur wenn nicht die Ausdrcke Callee, FinA ,\<dots>
  10.540  *)
  10.541 -  con_defs "[sub_expr_expr_def]"
  10.542  
  10.543 -end
  10.544 +lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
  10.545 +proof -
  10.546 +  assume "p \<in> R\<^sup>*"
  10.547 +  moreover obtain x y where p: "p = (x,y)" by (cases p)
  10.548 +  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
  10.549 +  hence "\<exists>n. (x,y) \<in> R^n"
  10.550 +  proof induct
  10.551 +    fix a have "(a,a) \<in> R^0" by simp
  10.552 +    thus "\<exists>n. (a,a) \<in> R ^ n" ..
  10.553 +  next
  10.554 +    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
  10.555 +    then obtain n where "(a,b) \<in> R^n" ..
  10.556 +    moreover assume "(b,c) \<in> R"
  10.557 +    ultimately have "(a,c) \<in> R^(Suc n)" by auto
  10.558 +    thus "\<exists>n. (a,c) \<in> R^n" ..
  10.559 +  qed
  10.560 +  with p show ?thesis by hypsubst
  10.561 +qed  
  10.562 +
  10.563 +(*
  10.564 +lemma imp_eval_trans:
  10.565 +  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  10.566 +    shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
  10.567 +*)
  10.568 +(* Jetzt muss man bei trans natrlich wieder unterscheiden: Stmt, Expr, Var!
  10.569 +   Sowas bldes:
  10.570 +   Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
  10.571 +   the_vals definieren\<dots>
  10.572 +  G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
  10.573 +*)
  10.574 +
  10.575 +
  10.576 +end
  10.577 \ No newline at end of file
    11.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed Jul 10 14:51:18 2002 +0200
    11.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Jul 10 15:07:02 2002 +0200
    11.3 @@ -173,7 +173,7 @@
    11.4    | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
    11.5    | In3 vs \<Rightarrow> True)"
    11.6  apply (erule eval_induct)
    11.7 -prefer 24 
    11.8 +prefer 26 
    11.9    apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
   11.10  apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
   11.11   simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
   11.12 @@ -1257,13 +1257,13 @@
   11.13      obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
   11.14             error_free_s1: "error_free s1" 
   11.15        by (blast)
   11.16 -    from conf_s1 have "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L)"
   11.17 +    from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
   11.18        by (cases s1) (auto intro: conforms_absorb)
   11.19      with wt error_free_s1
   11.20 -    show "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L) \<and>
   11.21 -          (normal (abupd (absorb (Break l)) s1)
   11.22 -           \<longrightarrow> G,L,store (abupd (absorb (Break l)) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
   11.23 -          (error_free (Norm s0) = error_free (abupd (absorb (Break l)) s1))"
   11.24 +    show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
   11.25 +          (normal (abupd (absorb l) s1)
   11.26 +           \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
   11.27 +          (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
   11.28        by (simp)
   11.29    next
   11.30      case (Comp c1 c2 s0 s1 s2 L accC T)
   11.31 @@ -1463,9 +1463,12 @@
   11.32        qed
   11.33      qed
   11.34    next
   11.35 -    case (Fin c1 c2 s0 s1 s2 x1 L accC T)
   11.36 +    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
   11.37      have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
   11.38      have c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
   11.39 +    have s3: "s3= (if \<exists>err. x1 = Some (Error err) 
   11.40 +                     then (x1, s1)
   11.41 +                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
   11.42      have  hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
   11.43      have  hyp_c2: "PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>" .
   11.44      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   11.45 @@ -1482,14 +1485,14 @@
   11.46      with wt_c2 hyp_c2
   11.47      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
   11.48        by blast
   11.49 -    show "abupd (abrupt_if (x1 \<noteq> None) x1) s2\<Colon>\<preceq>(G, L) \<and>
   11.50 -          (normal (abupd (abrupt_if (x1 \<noteq> None) x1) s2) 
   11.51 -           \<longrightarrow> G,L,store (abupd (abrupt_if (x1 \<noteq> None) x1) s2)
   11.52 -               \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
   11.53 -          (error_free (Norm s0) =
   11.54 -              error_free (abupd (abrupt_if (x1 \<noteq> None) x1) s2))"
   11.55 +    from error_free_s1 s3 
   11.56 +    have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
   11.57 +      by simp
   11.58 +    show "s3\<Colon>\<preceq>(G, L) \<and>
   11.59 +          (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
   11.60 +          (error_free (Norm s0) = error_free s3)"
   11.61      proof (cases x1)
   11.62 -      case None with conf_s2 wt show ?thesis by auto
   11.63 +      case None with conf_s2 s3' wt show ?thesis by auto
   11.64      next
   11.65        case (Some x) 
   11.66        with c2 wf conf_s1 conf_s2
   11.67 @@ -1501,7 +1504,7 @@
   11.68        with error_free_s2
   11.69        have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
   11.70  	by (cases s2) simp
   11.71 -      with Some wt conf show ?thesis
   11.72 +      with Some wt conf s3' show ?thesis
   11.73  	by (cases s2) auto
   11.74      qed
   11.75    next
   11.76 @@ -1679,6 +1682,60 @@
   11.77        by (auto elim!: wt_elim_cases 
   11.78                 intro: conf_litval simp add: empty_dt_def)
   11.79    next
   11.80 +    case (UnOp e s0 s1 unop v L accC T)
   11.81 +    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
   11.82 +    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   11.83 +    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
   11.84 +    then obtain eT
   11.85 +      where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
   11.86 +            wt_unop: "wt_unop unop eT" and
   11.87 +                  T: "T=Inl (PrimT (unop_type unop))" 
   11.88 +      by (auto elim!: wt_elim_cases)
   11.89 +    from conf_s0 wt_e 
   11.90 +    obtain     conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
   11.91 +                  wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
   11.92 +         error_free_s1: "error_free s1"
   11.93 +      by (auto dest!: hyp)
   11.94 +    from wt_v T wt_unop
   11.95 +    have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
   11.96 +      by (cases unop) auto
   11.97 +    with conf_s1 error_free_s1
   11.98 +    show "s1\<Colon>\<preceq>(G, L) \<and>
   11.99 +     (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T) \<and>
  11.100 +     error_free (Norm s0) = error_free s1"
  11.101 +      by simp
  11.102 +  next
  11.103 +    case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
  11.104 +    have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
  11.105 +    have hyp_e2: "PROP ?TypeSafe       s1  s2 (In1l e2) (In1 v2)" .
  11.106 +    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  11.107 +    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
  11.108 +    then obtain e1T e2T where
  11.109 +         wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
  11.110 +         wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
  11.111 +      wt_binop: "wt_binop G binop e1T e2T" and
  11.112 +             T: "T=Inl (PrimT (binop_type binop))"
  11.113 +      by (auto elim!: wt_elim_cases)
  11.114 +    from conf_s0 wt_e1 
  11.115 +    obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  11.116 +                  wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
  11.117 +          error_free_s1: "error_free s1"
  11.118 +      by (auto dest!: hyp_e1)
  11.119 +    from conf_s1 wt_e2 error_free_s1
  11.120 +    obtain      conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
  11.121 +                  wt_v2: "normal s2 \<longrightarrow> G,store s2\<turnstile>v2\<Colon>\<preceq>e2T" and
  11.122 +          error_free_s2: "error_free s2"
  11.123 +      by (auto dest!: hyp_e2)
  11.124 +    from wt_v1 wt_v2 wt_binop T
  11.125 +    have "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
  11.126 +      by (cases binop) auto
  11.127 +    with conf_s2 error_free_s2
  11.128 +    show "s2\<Colon>\<preceq>(G, L) \<and>
  11.129 +          (normal s2 \<longrightarrow>
  11.130 +        G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
  11.131 +          error_free (Norm s0) = error_free s2"
  11.132 +      by simp
  11.133 +  next
  11.134      case (Super s L accC T)
  11.135      have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
  11.136      have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
  11.137 @@ -1818,7 +1875,7 @@
  11.138      have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a')" .
  11.139      have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
  11.140      have hyp_methd: "PROP ?TypeSafe s3' s4 
  11.141 -                     (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  11.142 +               (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  11.143      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  11.144      have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  11.145                      \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
  11.146 @@ -1995,7 +2052,7 @@
  11.147              \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  11.148  	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  11.149  	  by - (drule wf_mdecl_bodyD,
  11.150 -                simp cong add: lname.case_cong ename.case_cong)
  11.151 +                auto simp: cong add: lname.case_cong ename.case_cong)
  11.152  	with dynM' iscls_invDeclC invDeclC'
  11.153  	have
  11.154  	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  11.155 @@ -2031,14 +2088,14 @@
  11.156    next
  11.157      case (Methd D s0 s1 sig v L accC T)
  11.158      have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
  11.159 -    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
  11.160 +    have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
  11.161      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  11.162      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
  11.163      then obtain m bodyT where
  11.164        D: "is_class G D" and
  11.165        m: "methd G D sig = Some m" and
  11.166        wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  11.167 -                   \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  11.168 +                  \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  11.169        T: "T=Inl bodyT"
  11.170        by (rule wt_elim_cases) auto
  11.171      with hyp [of _ _ "(Inl bodyT)"] conf_s0 
  11.172 @@ -2079,7 +2136,7 @@
  11.173      show "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L) \<and>
  11.174             (normal (abupd (absorb Ret) s2) \<longrightarrow>
  11.175               G,L,store (abupd (absorb Ret) s2)
  11.176 -              \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  11.177 +             \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  11.178            (error_free (Norm s0) = error_free (abupd (absorb Ret) s2)) "
  11.179        by (cases s2) (auto intro: conforms_locals)
  11.180    next
    12.1 --- a/src/HOL/Bali/WellType.thy	Wed Jul 10 14:51:18 2002 +0200
    12.2 +++ b/src/HOL/Bali/WellType.thy	Wed Jul 10 15:07:02 2002 +0200
    12.3 @@ -180,7 +180,67 @@
    12.4  apply (clarsimp simp add: invmode_IntVir_eq)
    12.5  done
    12.6  
    12.7 +consts unop_type :: "unop \<Rightarrow> prim_ty"
    12.8 +primrec 
    12.9 +"unop_type UPlus   = Integer"
   12.10 +"unop_type UMinus  = Integer"
   12.11 +"unop_type UBitNot = Integer"
   12.12 +"unop_type UNot    = Boolean"    
   12.13  
   12.14 +consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
   12.15 +primrec
   12.16 +"wt_unop UPlus   t = (t = PrimT Integer)"
   12.17 +"wt_unop UMinus  t = (t = PrimT Integer)"
   12.18 +"wt_unop UBitNot t = (t = PrimT Integer)"
   12.19 +"wt_unop UNot    t = (t = PrimT Boolean)"
   12.20 +
   12.21 +consts binop_type :: "binop \<Rightarrow> prim_ty"
   12.22 +primrec
   12.23 +"binop_type Mul      = Integer"     
   12.24 +"binop_type Div      = Integer"
   12.25 +"binop_type Mod      = Integer"
   12.26 +"binop_type Plus     = Integer"
   12.27 +"binop_type Minus    = Integer"
   12.28 +"binop_type LShift   = Integer"
   12.29 +"binop_type RShift   = Integer"
   12.30 +"binop_type RShiftU  = Integer"
   12.31 +"binop_type Less     = Boolean"
   12.32 +"binop_type Le       = Boolean"
   12.33 +"binop_type Greater  = Boolean"
   12.34 +"binop_type Ge       = Boolean"
   12.35 +"binop_type Eq       = Boolean"
   12.36 +"binop_type Neq      = Boolean"
   12.37 +"binop_type BitAnd   = Integer"
   12.38 +"binop_type And      = Boolean"
   12.39 +"binop_type BitXor   = Integer"
   12.40 +"binop_type Xor      = Boolean"
   12.41 +"binop_type BitOr    = Integer"
   12.42 +"binop_type Or       = Boolean"
   12.43 +
   12.44 +consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   12.45 +primrec
   12.46 +"wt_binop G Mul     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.47 +"wt_binop G Div     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.48 +"wt_binop G Mod     t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.49 +"wt_binop G Plus    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.50 +"wt_binop G Minus   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.51 +"wt_binop G LShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.52 +"wt_binop G RShift  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.53 +"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.54 +"wt_binop G Less    t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.55 +"wt_binop G Le      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.56 +"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.57 +"wt_binop G Ge      t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.58 +"wt_binop G Eq      t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 
   12.59 +"wt_binop G Neq     t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
   12.60 +"wt_binop G BitAnd  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.61 +"wt_binop G And     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   12.62 +"wt_binop G BitXor  t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.63 +"wt_binop G Xor     t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   12.64 +"wt_binop G BitOr   t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
   12.65 +"wt_binop G Or      t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
   12.66 +
   12.67 +      
   12.68  types tys  =        "ty + ty list"
   12.69  translations
   12.70    "tys"   <= (type) "ty + ty list"
   12.71 @@ -237,6 +297,7 @@
   12.72  	"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
   12.73  
   12.74  
   12.75 +
   12.76  inductive wt intros 
   12.77  
   12.78  
   12.79 @@ -312,6 +373,15 @@
   12.80    Lit:	"\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   12.81  					 E,dt\<Turnstile>Lit x\<Colon>-T"
   12.82  
   12.83 +  UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 
   12.84 +          \<Longrightarrow>
   12.85 +	  E,dt\<Turnstile>UnOp unop e\<Colon>-T"
   12.86 +  
   12.87 +  BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 
   12.88 +           T=PrimT (binop_type binop)\<rbrakk> 
   12.89 +           \<Longrightarrow>
   12.90 +	   E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   12.91 +  
   12.92    (* cf. 15.10.2, 15.11.1 *)
   12.93    Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   12.94  	  class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   12.95 @@ -348,6 +418,9 @@
   12.96   (* The class C is the dynamic class of the method call (cf. Eval.thy). 
   12.97    * It hasn't got to be directly accessible from the current package (pkg E). 
   12.98    * Only the static class must be accessible (enshured indirectly by Call). 
   12.99 +  * Note that l is just a dummy value. It is only used in the smallstep 
  12.100 +  * semantics. To proof typesafety directly for the smallstep semantics 
  12.101 +  * we would have to assume conformance of l here!
  12.102    *)
  12.103  
  12.104    Body:	"\<lbrakk>is_class (prg E) D;
  12.105 @@ -359,7 +432,8 @@
  12.106     * from the current package (pkg E), but can also be indirectly accessible 
  12.107     * due to inheritance (enshured in Call)
  12.108     * The result type hasn't got to be accessible in Java! (If it is not 
  12.109 -   * accessible you can only assign it to Object) 
  12.110 +   * accessible you can only assign it to Object).
  12.111 +   * For dummy value l see rule Methd. 
  12.112     *)
  12.113  
  12.114  (* well-typed variables *)
  12.115 @@ -404,6 +478,8 @@
  12.116  	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T"
  12.117  	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T"
  12.118  	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T"
  12.119 +        "E,dt\<Turnstile>In1l (UnOp unop e)           \<Colon>T"
  12.120 +        "E,dt\<Turnstile>In1l (BinOp binop e1 e2)     \<Colon>T"
  12.121  	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T"
  12.122  	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T"
  12.123  	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T"
  12.124 @@ -566,11 +642,11 @@
  12.125  apply (simp_all (no_asm_use) split del: split_if_asm)
  12.126  apply (safe del: disjE)
  12.127  (* 17 subgoals *)
  12.128 -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) *})
  12.129 +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) *})
  12.130  (*apply (safe del: disjE elim!: wt_elim_cases)*)
  12.131  apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
  12.132  apply (simp_all (no_asm_use) split del: split_if_asm)
  12.133 -apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
  12.134 +apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *)
  12.135  apply ((blast del: equalityCE dest: sym [THEN trans])+)
  12.136  done
  12.137