src/HOL/Bali/TypeSafe.thy
changeset 62042 6c6ccf573479
parent 60751 83f04804696c
child 62390 842917225d56
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Sat Jan 02 18:46:36 2016 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Sat Jan 02 18:48:45 2016 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Bali/TypeSafe.thy
     1.5      Author:     David von Oheimb and Norbert Schirmer
     1.6  *)
     1.7 -subsection {* The type soundness proof for Java *}
     1.8 +subsection \<open>The type soundness proof for Java\<close>
     1.9  
    1.10  theory TypeSafe
    1.11  imports DefiniteAssignmentCorrect Conform
    1.12 @@ -114,7 +114,7 @@
    1.13                  else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
    1.14      | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts)"
    1.15  
    1.16 -text {*
    1.17 +text \<open>
    1.18   With @{term rconf} we describe the conformance of the result value of a term.
    1.19   This definition gets rather complicated because of the relations between the
    1.20   injections of the different terms, types and values. The main case distinction
    1.21 @@ -132,7 +132,7 @@
    1.22   local variables are allowed to be @{term None}, since the definedness is not 
    1.23   ensured by conformance but by definite assignment. Field and array variables 
    1.24   must contain a value. 
    1.25 -*}
    1.26 +\<close>
    1.27   
    1.28  
    1.29  
    1.30 @@ -588,8 +588,8 @@
    1.31  qed
    1.32  
    1.33  corollary DynT_mheadsE [consumes 7]: 
    1.34 ---{* Same as @{text DynT_mheadsD} but better suited for application in 
    1.35 -typesafety proof   *}
    1.36 +\<comment>\<open>Same as \<open>DynT_mheadsD\<close> but better suited for application in 
    1.37 +typesafety proof\<close>
    1.38   assumes invC_compatible: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT" 
    1.39       and wf: "wf_prog G" 
    1.40       and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
    1.41 @@ -726,8 +726,8 @@
    1.42  declare split_paired_All [simp del] split_paired_Ex [simp del] 
    1.43  declare split_if     [split del] split_if_asm     [split del] 
    1.44          option.split [split del] option.split_asm [split del]
    1.45 -setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
    1.46 -setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    1.47 +setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
    1.48 +setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
    1.49  
    1.50  lemma FVar_lemma: 
    1.51  "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
    1.52 @@ -755,8 +755,8 @@
    1.53  declare split_paired_All [simp] split_paired_Ex [simp] 
    1.54  declare split_if     [split] split_if_asm     [split] 
    1.55          option.split [split] option.split_asm [split]
    1.56 -setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    1.57 -setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
    1.58 +setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
    1.59 +setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
    1.60  
    1.61  
    1.62  lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
    1.63 @@ -871,8 +871,8 @@
    1.64  declare split_paired_All [simp del] split_paired_Ex [simp del] 
    1.65  declare split_if     [split del] split_if_asm     [split del] 
    1.66          option.split [split del] option.split_asm [split del]
    1.67 -setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
    1.68 -setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    1.69 +setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
    1.70 +setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
    1.71  
    1.72  lemma conforms_init_lvars: 
    1.73  "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
    1.74 @@ -924,8 +924,8 @@
    1.75  declare split_paired_All [simp] split_paired_Ex [simp] 
    1.76  declare split_if     [split] split_if_asm     [split] 
    1.77          option.split [split] option.split_asm [split]
    1.78 -setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    1.79 -setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
    1.80 +setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
    1.81 +setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
    1.82  
    1.83  
    1.84  subsection "accessibility"
    1.85 @@ -1169,7 +1169,7 @@
    1.86    case Nil thus ?case by simp
    1.87  next
    1.88    case (Cons p ps tab qs)
    1.89 -  from `length (p#ps) = length qs`
    1.90 +  from \<open>length (p#ps) = length qs\<close>
    1.91    obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
    1.92      by (cases qs) auto
    1.93    from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
    1.94 @@ -1185,7 +1185,7 @@
    1.95    case Nil thus ?case by simp
    1.96  next
    1.97    case (Cons p ps tab qs x y)
    1.98 -  from `length (p#ps) = length qs`
    1.99 +  from \<open>length (p#ps) = length qs\<close>
   1.100    obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
   1.101      by (cases qs) auto
   1.102    from eq_length 
   1.103 @@ -1278,14 +1278,14 @@
   1.104    case Nil thus ?case by simp
   1.105  next
   1.106    case (Cons x xs tab ys z)
   1.107 -  note z = `tab vn = Some z`
   1.108 +  note z = \<open>tab vn = Some z\<close>
   1.109    show ?case
   1.110    proof (cases ys)
   1.111      case Nil
   1.112      with z show ?thesis by simp
   1.113    next
   1.114      case (Cons y ys')
   1.115 -    note ys = `ys = y#ys'`
   1.116 +    note ys = \<open>ys = y#ys'\<close>
   1.117      from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
   1.118        by (rule map_upd_Some_expand [of tab,elim_format]) blast
   1.119      hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
   1.120 @@ -1320,14 +1320,14 @@
   1.121    case Nil thus ?case by simp
   1.122  next
   1.123    case (Cons x xs tab tab' ys z)
   1.124 -  note some = `(tab(x # xs[\<mapsto>]ys)) vn = Some z`
   1.125 -  note tab_not_z = `tab vn \<noteq> Some z`
   1.126 +  note some = \<open>(tab(x # xs[\<mapsto>]ys)) vn = Some z\<close>
   1.127 +  note tab_not_z = \<open>tab vn \<noteq> Some z\<close>
   1.128    show ?case
   1.129    proof (cases ys)
   1.130      case Nil with some tab_not_z show ?thesis by simp
   1.131    next
   1.132      case (Cons y tl)
   1.133 -    note ys = `ys = y#tl`
   1.134 +    note ys = \<open>ys = y#tl\<close>
   1.135      show ?thesis
   1.136      proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
   1.137        case True
   1.138 @@ -1412,15 +1412,15 @@
   1.139    case Nil thus ?case by simp
   1.140  next
   1.141    case (Cons x xs tab tab' ys)
   1.142 -  note tab_vn = `(tab(x # xs[\<mapsto>]ys)) vn = Some el`
   1.143 -  note tab'_vn = `(tab'(x # xs[\<mapsto>]ys)) vn = None`
   1.144 +  note tab_vn = \<open>(tab(x # xs[\<mapsto>]ys)) vn = Some el\<close>
   1.145 +  note tab'_vn = \<open>(tab'(x # xs[\<mapsto>]ys)) vn = None\<close>
   1.146    show ?case
   1.147    proof (cases ys)
   1.148      case Nil
   1.149      with tab_vn show ?thesis by simp
   1.150    next
   1.151      case (Cons y tl)
   1.152 -    note ys = `ys=y#tl`
   1.153 +    note ys = \<open>ys=y#tl\<close>
   1.154      with tab_vn tab'_vn 
   1.155      have "(tab(x\<mapsto>y)) vn = Some el"
   1.156        by - (rule Cons.hyps,auto)
   1.157 @@ -1497,7 +1497,7 @@
   1.158  next
   1.159    case (Cons x xs tab ys)
   1.160    note Hyp = Cons.hyps
   1.161 -  note len = `length (x#xs)=length ys`
   1.162 +  note len = \<open>length (x#xs)=length ys\<close>
   1.163    show ?case
   1.164    proof (cases ys)
   1.165      case Nil with len show ?thesis by simp
   1.166 @@ -1728,7 +1728,7 @@
   1.167                       ?ErrorFree s0 s1")
   1.168    proof (induct)
   1.169      case (Abrupt xc s t L accC T A) 
   1.170 -    from `(Some xc, s)\<Colon>\<preceq>(G,L)`
   1.171 +    from \<open>(Some xc, s)\<Colon>\<preceq>(G,L)\<close>
   1.172      show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
   1.173        (normal (Some xc, s) 
   1.174        \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>undefined3 t\<Colon>\<preceq>T) \<and> 
   1.175 @@ -1736,19 +1736,19 @@
   1.176        by simp
   1.177    next
   1.178      case (Skip s L accC T A)
   1.179 -    from `Norm s\<Colon>\<preceq>(G, L)` and
   1.180 -      `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T`
   1.181 +    from \<open>Norm s\<Colon>\<preceq>(G, L)\<close> and
   1.182 +      \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T\<close>
   1.183      show "Norm s\<Colon>\<preceq>(G, L) \<and>
   1.184                (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
   1.185                (error_free (Norm s) = error_free (Norm s))"
   1.186        by simp
   1.187    next
   1.188      case (Expr s0 e v s1 L accC T A)
   1.189 -    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
   1.190 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
   1.191 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.192 +    note \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>
   1.193 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)\<close>
   1.194 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.195      moreover
   1.196 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T`
   1.197 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T\<close>
   1.198      then obtain eT 
   1.199        where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
   1.200        by (rule wt_elim_cases) blast
   1.201 @@ -1766,10 +1766,10 @@
   1.202        by (simp)
   1.203    next
   1.204      case (Lab s0 c s1 l L accC T A)
   1.205 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>`
   1.206 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.207 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>\<close>
   1.208 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.209      moreover
   1.210 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T`
   1.211 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T\<close>
   1.212      then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
   1.213        by (rule wt_elim_cases) blast
   1.214      moreover from Lab.prems obtain C where
   1.215 @@ -1789,12 +1789,12 @@
   1.216        by (simp)
   1.217    next
   1.218      case (Comp s0 c1 s1 c2 s2 L accC T A)
   1.219 -    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   1.220 -    note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
   1.221 -    note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
   1.222 -    note hyp_c2 = `PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>`
   1.223 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.224 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T`
   1.225 +    note eval_c1 = \<open>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1\<close>
   1.226 +    note eval_c2 = \<open>G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<close>
   1.227 +    note hyp_c1 = \<open>PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>\<close>
   1.228 +    note hyp_c2 = \<open>PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>\<close>
   1.229 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.230 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T\<close>
   1.231      then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   1.232                  wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
   1.233        by (rule wt_elim_cases) blast
   1.234 @@ -1835,13 +1835,13 @@
   1.235      qed
   1.236    next
   1.237      case (If s0 e b s1 c1 c2 s2 L accC T A)
   1.238 -    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
   1.239 -    note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
   1.240 -    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
   1.241 +    note eval_e = \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1\<close>
   1.242 +    note eval_then_else = \<open>G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<close>
   1.243 +    note hyp_e = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)\<close>
   1.244      note hyp_then_else =
   1.245 -      `PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>`
   1.246 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.247 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T`
   1.248 +      \<open>PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>\<close>
   1.249 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.250 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T\<close>
   1.251      then obtain 
   1.252                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
   1.253        wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
   1.254 @@ -1899,7 +1899,7 @@
   1.255        with wt show ?thesis
   1.256          by simp
   1.257      qed
   1.258 -    -- {* Note that we don't have to show that @{term b} really is a boolean 
   1.259 +    \<comment> \<open>Note that we don't have to show that @{term b} really is a boolean 
   1.260            value. With @{term the_Bool} we enforce to get a value of boolean 
   1.261            type. So execution will be type safe, even if b would be
   1.262            a string, for example. We might not expect such a behaviour to be
   1.263 @@ -1907,18 +1907,18 @@
   1.264            the evaulation rule, so that it only has a type safe evaluation if
   1.265            we actually get a boolean value for the condition. That b is actually
   1.266            a boolean value is part of @{term hyp_e}. See also Loop 
   1.267 -       *}
   1.268 +\<close>
   1.269    next
   1.270      case (Loop s0 e b s1 c s2 l s3 L accC T A)
   1.271 -    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
   1.272 -    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
   1.273 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.274 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
   1.275 +    note eval_e = \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1\<close>
   1.276 +    note hyp_e = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)\<close>
   1.277 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.278 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T\<close>
   1.279      then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
   1.280                  wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
   1.281        by (rule wt_elim_cases) blast
   1.282 -    note da = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   1.283 -            \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A`
   1.284 +    note da = \<open>\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   1.285 +            \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A\<close>
   1.286      then
   1.287      obtain E C where
   1.288        da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   1.289 @@ -2041,7 +2041,7 @@
   1.290      qed
   1.291    next
   1.292      case (Jmp s j L accC T A)
   1.293 -    note `Norm s\<Colon>\<preceq>(G, L)`
   1.294 +    note \<open>Norm s\<Colon>\<preceq>(G, L)\<close>
   1.295      moreover
   1.296      from Jmp.prems 
   1.297      have "j=Ret \<longrightarrow> Result \<in> dom (locals (store ((Norm s)::state)))"
   1.298 @@ -2055,10 +2055,10 @@
   1.299        by simp
   1.300    next
   1.301      case (Throw s0 e a s1 L accC T A)
   1.302 -    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
   1.303 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
   1.304 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.305 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T`
   1.306 +    note \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1\<close>
   1.307 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)\<close>
   1.308 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.309 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T\<close>
   1.310      then obtain tn 
   1.311        where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
   1.312              throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
   1.313 @@ -2083,11 +2083,11 @@
   1.314        by simp
   1.315    next
   1.316      case (Try s0 c1 s1 s2 catchC vn c2 s3 L accC T A)
   1.317 -    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   1.318 -    note sx_alloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
   1.319 -    note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
   1.320 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.321 -    note wt = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T`
   1.322 +    note eval_c1 = \<open>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1\<close>
   1.323 +    note sx_alloc = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
   1.324 +    note hyp_c1 = \<open>PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>\<close>
   1.325 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.326 +    note wt = \<open>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T\<close>
   1.327      then obtain 
   1.328        wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   1.329        wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
   1.330 @@ -2165,7 +2165,7 @@
   1.331            have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
   1.332                    \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
   1.333            proof -
   1.334 -            from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   1.335 +            from \<open>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1\<close>
   1.336              have "dom (locals (store ((Norm s0)::state))) 
   1.337                      \<subseteq> dom (locals (store s1))"
   1.338                by (rule dom_locals_eval_mono_elim)
   1.339 @@ -2200,15 +2200,15 @@
   1.340      qed
   1.341    next
   1.342      case (Fin s0 c1 x1 s1 c2 s2 s3 L accC T A)
   1.343 -    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)`
   1.344 -    note eval_c2 = `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`
   1.345 -    note s3 = `s3 = (if \<exists>err. x1 = Some (Error err)
   1.346 +    note eval_c1 = \<open>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)\<close>
   1.347 +    note eval_c2 = \<open>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<close>
   1.348 +    note s3 = \<open>s3 = (if \<exists>err. x1 = Some (Error err)
   1.349                       then (x1, s1)
   1.350 -                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
   1.351 -    note hyp_c1 = `PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>`
   1.352 -    note hyp_c2 = `PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>`
   1.353 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.354 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T`
   1.355 +                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>
   1.356 +    note hyp_c1 = \<open>PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>\<close>
   1.357 +    note hyp_c2 = \<open>PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>\<close>
   1.358 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.359 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T\<close>
   1.360      then obtain
   1.361        wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   1.362        wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
   1.363 @@ -2270,9 +2270,9 @@
   1.364      qed
   1.365    next
   1.366      case (Init C c s0 s3 s1 s2 L accC T A)
   1.367 -    note cls = `the (class G C) = c`
   1.368 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.369 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T`
   1.370 +    note cls = \<open>the (class G C) = c\<close>
   1.371 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.372 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T\<close>
   1.373      with cls
   1.374      have cls_C: "class G C = Some c"
   1.375        by - (erule wt_elim_cases, auto)
   1.376 @@ -2376,12 +2376,12 @@
   1.377      qed
   1.378    next
   1.379      case (NewC s0 C s1 a s2 L accC T A)
   1.380 -    note `G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1`
   1.381 -    note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
   1.382 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>`
   1.383 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.384 +    note \<open>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1\<close>
   1.385 +    note halloc = \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close>
   1.386 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>\<close>
   1.387 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.388      moreover
   1.389 -    note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T`
   1.390 +    note wt = \<open>\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T\<close>
   1.391      then obtain is_cls_C: "is_class G C" and
   1.392                         T: "T=Inl (Class C)"
   1.393        by (rule wt_elim_cases) (auto dest: is_acc_classD)
   1.394 @@ -2408,13 +2408,13 @@
   1.395        by auto
   1.396    next
   1.397      case (NewA s0 elT s1 e i s2 a s3 L accC T A)
   1.398 -    note eval_init = `G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1`
   1.399 -    note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2`
   1.400 -    note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
   1.401 -    note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>`
   1.402 -    note hyp_size = `PROP ?TypeSafe s1 s2 (In1l e) (In1 i)`
   1.403 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.404 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T`
   1.405 +    note eval_init = \<open>G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1\<close>
   1.406 +    note eval_e = \<open>G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2\<close>
   1.407 +    note halloc = \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3\<close>
   1.408 +    note hyp_init = \<open>PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>\<close>
   1.409 +    note hyp_size = \<open>PROP ?TypeSafe s1 s2 (In1l e) (In1 i)\<close>
   1.410 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.411 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T\<close>
   1.412      then obtain
   1.413        wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
   1.414        wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
   1.415 @@ -2479,11 +2479,11 @@
   1.416        by simp
   1.417    next
   1.418      case (Cast s0 e v s1 s2 castT L accC T A)
   1.419 -    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
   1.420 -    note s2 = `s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1`
   1.421 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
   1.422 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.423 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T`
   1.424 +    note \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>
   1.425 +    note s2 = \<open>s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1\<close>
   1.426 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)\<close>
   1.427 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.428 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T\<close>
   1.429      then obtain eT
   1.430        where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
   1.431                eT: "G\<turnstile>eT\<preceq>? castT" and 
   1.432 @@ -2525,8 +2525,8 @@
   1.433        by blast
   1.434    next
   1.435      case (Inst s0 e v s1 b instT L accC T A)
   1.436 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
   1.437 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.438 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)\<close>
   1.439 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.440      from Inst.prems obtain eT
   1.441      where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-RefT eT"  and
   1.442               T: "T=Inl (PrimT Boolean)" 
   1.443 @@ -2549,9 +2549,9 @@
   1.444                 intro: conf_litval simp add: empty_dt_def)
   1.445    next
   1.446      case (UnOp s0 e v s1 unop L accC T A)
   1.447 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
   1.448 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.449 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T`
   1.450 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)\<close>
   1.451 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.452 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T\<close>
   1.453      then obtain eT
   1.454        where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
   1.455              wt_unop: "wt_unop unop eT" and
   1.456 @@ -2576,15 +2576,15 @@
   1.457        by simp
   1.458    next
   1.459      case (BinOp s0 e1 v1 s1 binop e2 v2 s2 L accC T A)
   1.460 -    note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1`
   1.461 -    note eval_e2 = `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   1.462 -                             else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
   1.463 -    note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)`
   1.464 -    note hyp_e2 = `PROP ?TypeSafe       s1  s2 
   1.465 +    note eval_e1 = \<open>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1\<close>
   1.466 +    note eval_e2 = \<open>G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   1.467 +                             else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)\<close>
   1.468 +    note hyp_e1 = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)\<close>
   1.469 +    note hyp_e2 = \<open>PROP ?TypeSafe       s1  s2 
   1.470                     (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
   1.471 -                   (In1 v2)`
   1.472 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.473 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T`
   1.474 +                   (In1 v2)\<close>
   1.475 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.476 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T\<close>
   1.477      then obtain e1T e2T where
   1.478           wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
   1.479           wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
   1.480 @@ -2597,8 +2597,8 @@
   1.481        daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.482                    \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
   1.483        by (auto intro: da_Skip [simplified] assigned.select_convs)
   1.484 -    note da = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
   1.485 -                  \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A`
   1.486 +    note da = \<open>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
   1.487 +                  \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A\<close>
   1.488      then obtain E1 where
   1.489        da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.490                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e1\<guillemotright> E1"
   1.491 @@ -2612,20 +2612,20 @@
   1.492      have conf_v:
   1.493        "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
   1.494        by (cases binop) auto
   1.495 -    -- {* Note that we don't use the information that v1 really is compatible 
   1.496 +    \<comment> \<open>Note that we don't use the information that v1 really is compatible 
   1.497            with the expected type e1T and v2 is compatible with e2T, 
   1.498 -          because @{text eval_binop} will anyway produce an output of 
   1.499 +          because \<open>eval_binop\<close> will anyway produce an output of 
   1.500            the right type.
   1.501            So evaluating the addition of an integer with a string is type
   1.502            safe. This is a little bit annoying since we may regard such a
   1.503            behaviour as not type safe.
   1.504 -          If we want to avoid this we can redefine @{text eval_binop} so that
   1.505 +          If we want to avoid this we can redefine \<open>eval_binop\<close> so that
   1.506            it only produces a output of proper type if it is assigned to 
   1.507            values of the expected types, and arbitrary if the inputs have 
   1.508            unexpected types. The proof can easily be adapted since we
   1.509            have the hypothesis that the values have a proper type.
   1.510            This also applies to unary operations.
   1.511 -       *}
   1.512 +\<close>
   1.513      from eval_e1 have 
   1.514        s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
   1.515        by (rule dom_locals_eval_mono_elim)
   1.516 @@ -2667,8 +2667,8 @@
   1.517      qed
   1.518    next
   1.519      case (Super s L accC T A)
   1.520 -    note conf_s = `Norm s\<Colon>\<preceq>(G, L)`
   1.521 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T`
   1.522 +    note conf_s = \<open>Norm s\<Colon>\<preceq>(G, L)\<close>
   1.523 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T\<close>
   1.524      then obtain C c where
   1.525               C: "L This = Some (Class C)" and
   1.526         neq_Obj: "C\<noteq>Object" and
   1.527 @@ -2692,8 +2692,8 @@
   1.528        by simp
   1.529    next
   1.530      case (Acc s0 v w upd s1 L accC T A)
   1.531 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))`
   1.532 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.533 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))\<close>
   1.534 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.535      from Acc.prems obtain vT where
   1.536        wt_v: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>v\<Colon>=vT" and
   1.537           T: "T=Inl vT"
   1.538 @@ -2712,7 +2712,7 @@
   1.539          also
   1.540          have "dom (locals s0) \<subseteq> dom (locals (store s1))"
   1.541          proof -
   1.542 -          from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
   1.543 +          from \<open>G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1\<close>
   1.544            show ?thesis
   1.545              by (rule dom_locals_eval_mono_elim) simp
   1.546          qed
   1.547 @@ -2732,12 +2732,12 @@
   1.548        by simp
   1.549    next
   1.550      case (Ass s0 var w upd s1 e v s2 L accC T A)
   1.551 -    note eval_var = `G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1`
   1.552 -    note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
   1.553 -    note hyp_var = `PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))`
   1.554 -    note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 v)`
   1.555 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.556 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T`
   1.557 +    note eval_var = \<open>G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1\<close>
   1.558 +    note eval_e = \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close>
   1.559 +    note hyp_var = \<open>PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))\<close>
   1.560 +    note hyp_e = \<open>PROP ?TypeSafe s1 s2 (In1l e) (In1 v)\<close>
   1.561 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.562 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T\<close>
   1.563      then obtain varT eT where
   1.564           wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
   1.565             wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
   1.566 @@ -2889,13 +2889,13 @@
   1.567      qed
   1.568    next
   1.569      case (Cond s0 e0 b s1 e1 e2 v s2 L accC T A)
   1.570 -    note eval_e0 = `G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
   1.571 -    note eval_e1_e2 = `G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2`
   1.572 -    note hyp_e0 = `PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)`
   1.573 -    note hyp_if = `PROP ?TypeSafe s1 s2
   1.574 -                       (In1l (if the_Bool b then e1 else e2)) (In1 v)`
   1.575 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.576 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T`
   1.577 +    note eval_e0 = \<open>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1\<close>
   1.578 +    note eval_e1_e2 = \<open>G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<close>
   1.579 +    note hyp_e0 = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)\<close>
   1.580 +    note hyp_if = \<open>PROP ?TypeSafe s1 s2
   1.581 +                       (In1l (if the_Bool b then e1 else e2)) (In1 v)\<close>
   1.582 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.583 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T\<close>
   1.584      then obtain T1 T2 statT where
   1.585        wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
   1.586        wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
   1.587 @@ -2983,24 +2983,24 @@
   1.588    next
   1.589      case (Call s0 e a s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC'
   1.590             v s4 L accC T A)
   1.591 -    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
   1.592 -    note eval_args = `G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2`
   1.593 -    note invDeclC = `invDeclC 
   1.594 +    note eval_e = \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1\<close>
   1.595 +    note eval_args = \<open>G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2\<close>
   1.596 +    note invDeclC = \<open>invDeclC 
   1.597                        = invocation_declclass G mode (store s2) a statT 
   1.598 -                           \<lparr>name = mn, parTs = pTs'\<rparr>`
   1.599 +                           \<lparr>name = mn, parTs = pTs'\<rparr>\<close>
   1.600      note init_lvars =
   1.601 -      `s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2`
   1.602 -    note check = `s3' =
   1.603 -        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3`
   1.604 +      \<open>s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2\<close>
   1.605 +    note check = \<open>s3' =
   1.606 +        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3\<close>
   1.607      note eval_methd =
   1.608 -      `G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4`
   1.609 -    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
   1.610 -    note hyp_args = `PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)`
   1.611 -    note hyp_methd = `PROP ?TypeSafe s3' s4 
   1.612 -        (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)`
   1.613 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.614 -    note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   1.615 -        \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T`
   1.616 +      \<open>G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4\<close>
   1.617 +    note hyp_e = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)\<close>
   1.618 +    note hyp_args = \<open>PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)\<close>
   1.619 +    note hyp_methd = \<open>PROP ?TypeSafe s3' s4 
   1.620 +        (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)\<close>
   1.621 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.622 +    note wt = \<open>\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   1.623 +        \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T\<close>
   1.624      from wt obtain pTs statDeclT statM where
   1.625                   wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
   1.626                wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
   1.627 @@ -3325,10 +3325,10 @@
   1.628      qed
   1.629    next
   1.630      case (Methd s0 D sig v s1 L accC T A)
   1.631 -    note `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
   1.632 -    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)`
   1.633 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.634 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T`
   1.635 +    note \<open>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<close>
   1.636 +    note hyp = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)\<close>
   1.637 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.638 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T\<close>
   1.639      then obtain m bodyT where
   1.640        D: "is_class G D" and
   1.641        m: "methd G D sig = Some m" and
   1.642 @@ -3350,12 +3350,12 @@
   1.643        by (auto simp add: Let_def body_def)
   1.644    next
   1.645      case (Body s0 D s1 c s2 s3 L accC T A)
   1.646 -    note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1`
   1.647 -    note eval_c = `G\<turnstile>s1 \<midarrow>c\<rightarrow> s2`
   1.648 -    note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>`
   1.649 -    note hyp_c = `PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>`
   1.650 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.651 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T`
   1.652 +    note eval_init = \<open>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1\<close>
   1.653 +    note eval_c = \<open>G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<close>
   1.654 +    note hyp_init = \<open>PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>\<close>
   1.655 +    note hyp_c = \<open>PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>\<close>
   1.656 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.657 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T\<close>
   1.658      then obtain bodyT where
   1.659           iscls_D: "is_class G D" and
   1.660              wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
   1.661 @@ -3413,10 +3413,10 @@
   1.662        have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
   1.663          by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
   1.664        moreover 
   1.665 -      note `s3 =
   1.666 +      note \<open>s3 =
   1.667                  (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
   1.668                          abrupt s2 = Some (Jump (Cont l))
   1.669 -                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
   1.670 +                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)\<close>
   1.671        ultimately show ?thesis
   1.672          by force
   1.673      qed
   1.674 @@ -3451,8 +3451,8 @@
   1.675        by (cases s2) (auto intro: conforms_locals)
   1.676    next
   1.677      case (LVar s vn L accC T)
   1.678 -    note conf_s = `Norm s\<Colon>\<preceq>(G, L)` and
   1.679 -      wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T`
   1.680 +    note conf_s = \<open>Norm s\<Colon>\<preceq>(G, L)\<close> and
   1.681 +      wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T\<close>
   1.682      then obtain vnT where
   1.683        vnT: "L vn = Some vnT" and
   1.684          T: "T=Inl vnT"
   1.685 @@ -3474,14 +3474,14 @@
   1.686        by (simp add: lvar_def) 
   1.687    next
   1.688      case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC L accC' T A)
   1.689 -    note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1`
   1.690 -    note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2`
   1.691 -    note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
   1.692 -    note check = `s3 = check_field_access G accC statDeclC fn stat a s2'`
   1.693 -    note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>`
   1.694 -    note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 a)`
   1.695 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.696 -    note wt = `\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T`
   1.697 +    note eval_init = \<open>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1\<close>
   1.698 +    note eval_e = \<open>G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2\<close>
   1.699 +    note fvar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>
   1.700 +    note check = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
   1.701 +    note hyp_init = \<open>PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>\<close>
   1.702 +    note hyp_e = \<open>PROP ?TypeSafe s1 s2 (In1l e) (In1 a)\<close>
   1.703 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.704 +    note wt = \<open>\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T\<close>
   1.705      then obtain statC f where
   1.706                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   1.707              accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
   1.708 @@ -3590,13 +3590,13 @@
   1.709        by auto
   1.710    next
   1.711      case (AVar s0 e1 a s1 e2 i s2 v s2' L accC T A)
   1.712 -    note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1`
   1.713 -    note eval_e2 = `G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2`
   1.714 -    note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)`
   1.715 -    note hyp_e2 = `PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)`
   1.716 -    note avar = `(v, s2') = avar G i a s2`
   1.717 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.718 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T`
   1.719 +    note eval_e1 = \<open>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1\<close>
   1.720 +    note eval_e2 = \<open>G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2\<close>
   1.721 +    note hyp_e1 = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)\<close>
   1.722 +    note hyp_e2 = \<open>PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)\<close>
   1.723 +    note avar = \<open>(v, s2') = avar G i a s2\<close>
   1.724 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.725 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T\<close>
   1.726      then obtain elemT
   1.727         where wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
   1.728               wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
   1.729 @@ -3690,12 +3690,12 @@
   1.730        by (auto elim!: wt_elim_cases)
   1.731    next
   1.732      case (Cons s0 e v s1 es vs s2 L accC T A)
   1.733 -    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
   1.734 -    note eval_es = `G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2`
   1.735 -    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
   1.736 -    note hyp_es = `PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)`
   1.737 -    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
   1.738 -    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T`
   1.739 +    note eval_e = \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>
   1.740 +    note eval_es = \<open>G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<close>
   1.741 +    note hyp_e = \<open>PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)\<close>
   1.742 +    note hyp_es = \<open>PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)\<close>
   1.743 +    note conf_s0 = \<open>Norm s0\<Colon>\<preceq>(G, L)\<close>
   1.744 +    note wt = \<open>\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T\<close>
   1.745      then obtain eT esT where
   1.746         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
   1.747         wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
   1.748 @@ -3749,10 +3749,10 @@
   1.749    from this and conf_s0 wt da show ?thesis .
   1.750  qed
   1.751  
   1.752 -text {* 
   1.753 +text \<open>
   1.754  
   1.755  
   1.756 -*} (* dummy text command to break paragraph for latex;
   1.757 +\<close> (* dummy text command to break paragraph for latex;
   1.758                large paragraphs exhaust memory of debian pdflatex *)
   1.759  
   1.760  corollary eval_type_soundE [consumes 5]:
   1.761 @@ -3823,7 +3823,7 @@
   1.762  
   1.763  subsection "Ideas for the future"
   1.764  
   1.765 -text {* In the type soundness proof and the correctness proof of 
   1.766 +text \<open>In the type soundness proof and the correctness proof of 
   1.767  definite assignment we perform induction on the evaluation relation with the 
   1.768  further preconditions that the term is welltyped and definitely assigned. During
   1.769  the proofs we have to establish the welltypedness and definite assignment of 
   1.770 @@ -3833,7 +3833,7 @@
   1.771  evaluation of a wellformed term, were these propagations is already done, once
   1.772  and forever. 
   1.773  Then we can do the proofs with this rule and can enjoy the time we have saved.
   1.774 -Here is a first and incomplete sketch of such a rule.*}
   1.775 +Here is a first and incomplete sketch of such a rule.\<close>
   1.776  theorem wellformed_eval_induct [consumes 4, case_names Abrupt Skip Expr Lab 
   1.777                                  Comp If]:
   1.778    assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
   1.779 @@ -3926,8 +3926,8 @@
   1.780        by (rule lab)
   1.781    next
   1.782      case (Comp s0 c1 s1 c2 s2 L accC T A) 
   1.783 -    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   1.784 -    note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
   1.785 +    note eval_c1 = \<open>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1\<close>
   1.786 +    note eval_c2 = \<open>G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<close>
   1.787      from Comp.prems obtain 
   1.788        wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   1.789        wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
   1.790 @@ -3969,8 +3969,8 @@
   1.791        by (rule comp) iprover+
   1.792    next
   1.793      case (If s0 e b s1 c1 c2 s2 L accC T A)
   1.794 -    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
   1.795 -    note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
   1.796 +    note eval_e = \<open>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1\<close>
   1.797 +    note eval_then_else = \<open>G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<close>
   1.798      from If.prems
   1.799      obtain 
   1.800                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and