src/HOL/Bali/DefiniteAssignmentCorrect.thy
author haftmann
Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407 61dd8c145da7
parent 35069 09154b995ed8
child 44890 22f665a2e91c
permissions -rw-r--r--
declare lex_prod_def [code del]
schirmer@13688
     1
header {* Correctness of Definite Assignment *}
schirmer@13688
     2
haftmann@16417
     3
theory DefiniteAssignmentCorrect imports WellForm Eval begin
schirmer@13688
     4
wenzelm@24019
     5
declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
schirmer@13688
     6
schirmer@13688
     7
lemma sxalloc_no_jump:
schirmer@13688
     8
  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
schirmer@13688
     9
           no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
schirmer@13688
    10
   shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
    11
using sxalloc no_jmp
schirmer@13688
    12
by cases simp_all
schirmer@13688
    13
schirmer@13688
    14
lemma sxalloc_no_jump':
schirmer@13688
    15
  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
schirmer@13688
    16
          jump:  "abrupt s1 = Some (Jump j)"
schirmer@13688
    17
 shows "abrupt s0 = Some (Jump j)"
schirmer@13688
    18
using sxalloc jump
schirmer@13688
    19
by cases simp_all
schirmer@13688
    20
schirmer@13688
    21
lemma halloc_no_jump:
schirmer@13688
    22
  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
schirmer@13688
    23
           no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
schirmer@13688
    24
   shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
    25
using halloc no_jmp
schirmer@13688
    26
by cases simp_all
schirmer@13688
    27
schirmer@13688
    28
lemma halloc_no_jump':
schirmer@13688
    29
  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
schirmer@13688
    30
          jump:  "abrupt s1 = Some (Jump j)"
schirmer@13688
    31
  shows "abrupt s0 = Some (Jump j)"
schirmer@13688
    32
using halloc jump
schirmer@13688
    33
by cases simp_all
schirmer@13688
    34
schirmer@13688
    35
lemma Body_no_jump: 
schirmer@13688
    36
   assumes eval: "G\<turnstile>s0 \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and
schirmer@13688
    37
           jump: "abrupt s0 \<noteq> Some (Jump j)"
schirmer@13688
    38
   shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
    39
proof (cases "normal s0")
schirmer@13688
    40
  case True
schirmer@13688
    41
  with eval obtain s0' where eval': "G\<turnstile>Norm s0' \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and
schirmer@13688
    42
                             s0: "s0 = Norm s0'"
schirmer@13688
    43
    by (cases s0) simp
schirmer@13688
    44
  from eval' obtain s2 where
schirmer@13688
    45
     s1: "s1 = abupd (absorb Ret)
schirmer@13688
    46
             (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
schirmer@13688
    47
                     abrupt s2 = Some (Jump (Cont l))
schirmer@13688
    48
              then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)"
schirmer@13688
    49
    by cases simp
schirmer@13688
    50
  show ?thesis
schirmer@13688
    51
  proof (cases "\<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
schirmer@13688
    52
                   abrupt s2 = Some (Jump (Cont l))")
schirmer@13688
    53
    case True
schirmer@13688
    54
    with s1 have "abrupt s1 = Some (Error CrossMethodJump)"
schirmer@13688
    55
      by (cases s2) simp
schirmer@13688
    56
    thus ?thesis by simp
schirmer@13688
    57
  next
schirmer@13688
    58
    case False
schirmer@13688
    59
    with s1 have "s1=abupd (absorb Ret) s2"
schirmer@13688
    60
      by simp
schirmer@13688
    61
    with False show ?thesis
schirmer@13688
    62
      by (cases s2,cases j) (auto simp add: absorb_def)
schirmer@13688
    63
  qed
schirmer@13688
    64
next
schirmer@13688
    65
  case False
schirmer@13688
    66
  with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Body D c-\<succ>v\<rightarrow>s1"
schirmer@13688
    67
                                 "s0 = (Some abr, s0')"
schirmer@13688
    68
    by (cases s0) fastsimp
schirmer@13688
    69
  with this jump
schirmer@13688
    70
  show ?thesis
schirmer@13688
    71
    by (cases) (simp)
schirmer@13688
    72
qed
schirmer@13688
    73
schirmer@13688
    74
lemma Methd_no_jump: 
schirmer@13688
    75
   assumes eval: "G\<turnstile>s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1" and
schirmer@13688
    76
           jump: "abrupt s0 \<noteq> Some (Jump j)"
schirmer@13688
    77
   shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
    78
proof (cases "normal s0")
schirmer@13688
    79
  case True
schirmer@13688
    80
   with eval obtain s0' where "G\<turnstile>Norm s0' \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1" 
schirmer@13688
    81
                              "s0 = Norm s0'"
schirmer@13688
    82
    by (cases s0) simp
schirmer@13688
    83
  then obtain D' body where "G\<turnstile>s0 \<midarrow>Body D' body-\<succ>v\<rightarrow>s1"
schirmer@13688
    84
    by (cases) (simp add: body_def2)
schirmer@13688
    85
  from this jump
schirmer@13688
    86
  show ?thesis
schirmer@13688
    87
    by (rule Body_no_jump)
schirmer@13688
    88
next
schirmer@13688
    89
  case False
schirmer@13688
    90
  with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1"
schirmer@13688
    91
                                 "s0 = (Some abr, s0')"
schirmer@13688
    92
    by (cases s0) fastsimp
schirmer@13688
    93
  with this jump
schirmer@13688
    94
  show ?thesis
schirmer@13688
    95
    by (cases) (simp)
schirmer@13688
    96
qed
schirmer@13688
    97
schirmer@13688
    98
lemma jumpNestingOkS_mono: 
schirmer@13688
    99
  assumes jumpNestingOk_l': "jumpNestingOkS jmps' c" 
schirmer@13688
   100
      and      subset: "jmps' \<subseteq> jmps"
schirmer@13688
   101
 shows "jumpNestingOkS jmps c"
schirmer@13688
   102
proof -
schirmer@13688
   103
    have True and True and 
schirmer@13688
   104
       "\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c" 
schirmer@13688
   105
       and True
wenzelm@18459
   106
  proof (induct rule: var_expr_stmt.inducts)
schirmer@13688
   107
    case (Lab j c jmps' jmps)
wenzelm@23350
   108
    note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
wenzelm@23350
   109
    note jmps = `jmps' \<subseteq> jmps`
schirmer@13688
   110
    with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp
schirmer@13688
   111
    moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto
schirmer@13688
   112
    ultimately
schirmer@13688
   113
    have "jumpNestingOkS ({j} \<union> jmps) c"
schirmer@13688
   114
      by (rule Lab.hyps)
schirmer@13688
   115
    thus ?case 
schirmer@13688
   116
      by simp
schirmer@13688
   117
  next
schirmer@13688
   118
    case (Jmp j jmps' jmps) 
schirmer@13688
   119
    thus ?case 
schirmer@13688
   120
      by (cases j) auto
schirmer@13688
   121
  next
schirmer@13688
   122
    case (Comp c1 c2 jmps' jmps)
schirmer@13688
   123
    from Comp.prems 
schirmer@13688
   124
    have "jumpNestingOkS jmps c1" by - (rule Comp.hyps,auto)
schirmer@13688
   125
    moreover from Comp.prems
schirmer@13688
   126
    have "jumpNestingOkS jmps c2" by - (rule Comp.hyps,auto)
schirmer@13688
   127
    ultimately show ?case
schirmer@13688
   128
      by simp
schirmer@13688
   129
  next
wenzelm@24783
   130
    case (If' e c1 c2 jmps' jmps)
wenzelm@24783
   131
    from If'.prems 
wenzelm@24783
   132
    have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto)
wenzelm@24783
   133
    moreover from If'.prems 
wenzelm@24783
   134
    have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto)
schirmer@13688
   135
    ultimately show ?case
schirmer@13688
   136
      by simp
schirmer@13688
   137
  next
schirmer@13688
   138
    case (Loop l e c jmps' jmps)
wenzelm@23350
   139
    from `jumpNestingOkS jmps' (l\<bullet> While(e) c)`
wenzelm@23350
   140
    have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
wenzelm@23350
   141
    moreover
wenzelm@23350
   142
    from `jmps' \<subseteq> jmps`
wenzelm@23350
   143
    have "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps" by auto
schirmer@13688
   144
    ultimately
schirmer@13688
   145
    have "jumpNestingOkS ({Cont l} \<union> jmps) c"
schirmer@13688
   146
      by (rule Loop.hyps)
schirmer@13688
   147
    thus ?case by simp
schirmer@13688
   148
  next
schirmer@13688
   149
    case (TryC c1 C vn c2 jmps' jmps)
schirmer@13688
   150
    from TryC.prems 
schirmer@13688
   151
    have "jumpNestingOkS jmps c1" by - (rule TryC.hyps,auto)
schirmer@13688
   152
    moreover from TryC.prems 
schirmer@13688
   153
    have "jumpNestingOkS jmps c2" by - (rule TryC.hyps,auto)
schirmer@13688
   154
    ultimately show ?case
schirmer@13688
   155
      by simp
schirmer@13688
   156
  next
schirmer@13688
   157
    case (Fin c1 c2 jmps' jmps)
schirmer@13688
   158
    from Fin.prems 
schirmer@13688
   159
    have "jumpNestingOkS jmps c1" by - (rule Fin.hyps,auto)
schirmer@13688
   160
    moreover from Fin.prems 
schirmer@13688
   161
    have "jumpNestingOkS jmps c2" by - (rule Fin.hyps,auto)
schirmer@13688
   162
    ultimately show ?case
schirmer@13688
   163
      by simp
schirmer@13688
   164
  qed (simp_all)
schirmer@13688
   165
  with jumpNestingOk_l' subset
schirmer@13688
   166
  show ?thesis
nipkow@17589
   167
    by iprover
schirmer@13688
   168
qed
schirmer@13688
   169
   
schirmer@13688
   170
corollary jumpNestingOk_mono: 
schirmer@13688
   171
  assumes jmpOk: "jumpNestingOk jmps' t" 
schirmer@13688
   172
     and subset: "jmps' \<subseteq> jmps"
schirmer@13688
   173
  shows  "jumpNestingOk jmps t"
schirmer@13688
   174
proof (cases t)
schirmer@13688
   175
  case (In1 expr_stmt)
schirmer@13688
   176
  show ?thesis
schirmer@13688
   177
  proof (cases expr_stmt)
schirmer@13688
   178
    case (Inl e)
schirmer@13688
   179
    with In1 show ?thesis by simp
schirmer@13688
   180
  next
schirmer@13688
   181
    case (Inr s)
schirmer@13688
   182
    with In1 jmpOk subset show ?thesis by (auto intro: jumpNestingOkS_mono)
schirmer@13688
   183
  qed
schirmer@13688
   184
qed (simp_all)
schirmer@13688
   185
schirmer@13688
   186
lemma assign_abrupt_propagation: 
schirmer@13688
   187
 assumes f_ok: "abrupt (f n s) \<noteq> x"
schirmer@13688
   188
   and    ass: "abrupt (assign f n s) = x"
schirmer@13688
   189
  shows "abrupt s = x"
schirmer@13688
   190
proof (cases x)
schirmer@13688
   191
  case None
schirmer@13688
   192
  with ass show ?thesis
schirmer@13688
   193
    by (cases s) (simp add: assign_def Let_def)
schirmer@13688
   194
next
schirmer@13688
   195
  case (Some xcpt)
schirmer@13688
   196
  from f_ok
schirmer@13688
   197
  obtain xf sf where "f n s = (xf,sf)"
schirmer@13688
   198
    by (cases "f n s")
schirmer@13688
   199
  with Some ass f_ok show ?thesis
schirmer@13688
   200
    by (cases s) (simp add: assign_def Let_def)
schirmer@13688
   201
qed
schirmer@13688
   202
 
schirmer@13688
   203
lemma wt_init_comp_ty': 
schirmer@13688
   204
"is_acc_type (prg Env) (pid (cls Env)) T \<Longrightarrow> Env\<turnstile>init_comp_ty T\<Colon>\<surd>"
schirmer@13688
   205
apply (unfold init_comp_ty_def)
schirmer@13688
   206
apply (clarsimp simp add: accessible_in_RefT_simp 
schirmer@13688
   207
                          is_acc_type_def is_acc_class_def)
schirmer@13688
   208
done
schirmer@13688
   209
schirmer@13688
   210
lemma fvar_upd_no_jump: 
schirmer@13688
   211
      assumes upd: "upd = snd (fst (fvar statDeclC stat fn a s'))"
schirmer@13688
   212
        and noJmp: "abrupt s \<noteq> Some (Jump j)"
schirmer@13688
   213
        shows "abrupt (upd val s) \<noteq> Some (Jump j)"
schirmer@13688
   214
proof (cases "stat")
schirmer@13688
   215
  case True
schirmer@13688
   216
  with noJmp upd
schirmer@13688
   217
  show ?thesis
schirmer@13688
   218
    by (cases s) (simp add: fvar_def2)
schirmer@13688
   219
next
schirmer@13688
   220
  case False
schirmer@13688
   221
  with noJmp upd
schirmer@13688
   222
  show ?thesis
schirmer@13688
   223
    by (cases s) (simp add: fvar_def2)
schirmer@13688
   224
qed
schirmer@13688
   225
schirmer@13688
   226
schirmer@13688
   227
lemma avar_state_no_jump: 
schirmer@13688
   228
  assumes jmp: "abrupt (snd (avar G i a s)) = Some (Jump j)"
schirmer@13688
   229
  shows "abrupt s = Some (Jump j)"
schirmer@13688
   230
proof (cases "normal s")
schirmer@13688
   231
  case True with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)
schirmer@13688
   232
next
schirmer@13688
   233
  case False with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)
schirmer@13688
   234
qed
schirmer@13688
   235
schirmer@13688
   236
lemma avar_upd_no_jump: 
schirmer@13688
   237
      assumes upd: "upd = snd (fst (avar G i a s'))"
schirmer@13688
   238
        and noJmp: "abrupt s \<noteq> Some (Jump j)"
schirmer@13688
   239
        shows "abrupt (upd val s) \<noteq> Some (Jump j)"
schirmer@13688
   240
using upd noJmp
schirmer@13688
   241
by (cases s) (simp add: avar_def2 abrupt_if_def)
schirmer@13688
   242
schirmer@13688
   243
schirmer@13688
   244
text {* 
schirmer@13688
   245
The next theorem expresses: If jumps (breaks, continues, returns) are nested
schirmer@13688
   246
correctly, we won't find an unexpected jump in the result state of the 
schirmer@13688
   247
evaluation. For exeample, a break can't leave its enclosing loop, an return
schirmer@13688
   248
cant leave its enclosing method.
schirmer@13688
   249
To proove this, the method call is critical. Allthough the
schirmer@13688
   250
wellformedness of the whole program guarantees that the jumps (breaks,continues
schirmer@13688
   251
and returns) are nested
schirmer@13688
   252
correctly in all method bodies, the call rule alone does not guarantee that I
schirmer@13688
   253
will call a method or even a class that is part of the program due to dynamic
schirmer@13688
   254
binding! To be able to enshure this we need a kind of conformance of the
schirmer@13688
   255
state, like in the typesafety proof. But then we will redo the typesafty
schirmer@13688
   256
proof here. It would be nice if we could find an easy precondition that will
schirmer@13688
   257
guarantee that all calls will actually call classes and methods of the current
schirmer@13688
   258
program, which can be instantiated in the typesafty proof later on.
schirmer@13688
   259
To fix this problem, I have instrumented the semantic definition of a call
schirmer@13688
   260
to filter out any breaks in the state and to throw an error instead. 
schirmer@13688
   261
schirmer@13688
   262
To get an induction hypothesis which is strong enough to perform the
schirmer@13688
   263
proof, we can't just 
schirmer@13688
   264
assume @{term jumpNestingOk} for the empty set and conlcude, that no jump at 
schirmer@13688
   265
all will be in the resulting state,  because the set is altered by 
schirmer@13688
   266
the statements @{term Lab} and @{term While}. 
schirmer@13688
   267
schirmer@13688
   268
The wellformedness of the program is used to enshure that for all
schirmer@13688
   269
classinitialisations and methods the nesting of jumps is wellformed, too.
schirmer@13688
   270
*}  
schirmer@13688
   271
theorem jumpNestingOk_eval:
schirmer@13688
   272
  assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
schirmer@13688
   273
     and jmpOk: "jumpNestingOk jmps t" 
schirmer@13688
   274
     and wt: "Env\<turnstile>t\<Colon>T" 
schirmer@13688
   275
     and wf: "wf_prog G"
schirmer@13688
   276
     and  G: "prg Env = G"
wenzelm@19859
   277
     and no_jmp: "\<forall>j. abrupt s0 = Some (Jump j) \<longrightarrow> j \<in> jmps"
schirmer@13688
   278
                    (is "?Jmp jmps s0")
wenzelm@19859
   279
  shows  "(\<forall>j. fst s1 = Some (Jump j) \<longrightarrow> j \<in> jmps) \<and>
schirmer@13688
   280
                 (normal s1 \<longrightarrow>
wenzelm@19859
   281
                  (\<forall> w upd. v=In2 (w,upd)
wenzelm@19859
   282
                   \<longrightarrow>   (\<forall> s j val.
schirmer@13688
   283
                          abrupt s \<noteq> Some (Jump j) \<longrightarrow>
schirmer@13688
   284
                          abrupt (upd val s) \<noteq> Some (Jump j))))"
schirmer@13688
   285
        (is "?Jmp jmps s1 \<and> ?Upd v s1")  
schirmer@13688
   286
proof -
schirmer@13688
   287
  let ?HypObj = "\<lambda> t s0 s1 v.
schirmer@13688
   288
       (\<forall> jmps T Env. 
schirmer@13688
   289
          ?Jmp jmps s0 \<longrightarrow> jumpNestingOk jmps t \<longrightarrow> Env\<turnstile>t\<Colon>T \<longrightarrow> prg Env=G\<longrightarrow>
schirmer@13688
   290
          ?Jmp jmps s1 \<and> ?Upd v s1)"
schirmer@13688
   291
  -- {* Variable @{text ?HypObj} is the following goal spelled in terms of
schirmer@13688
   292
        the object logic, instead of the meta logic. It is needed in some
schirmer@13688
   293
        cases of the induction were, the atomize-rulify process of induct 
schirmer@13688
   294
        does not work fine, because the eval rules mix up object and meta
schirmer@13688
   295
        logic. See for example the case for the loop. *} 
schirmer@13688
   296
  from eval 
schirmer@13688
   297
  have "\<And> jmps T Env. \<lbrakk>?Jmp jmps s0; jumpNestingOk jmps t; Env\<turnstile>t\<Colon>T;prg Env=G\<rbrakk>
schirmer@13688
   298
            \<Longrightarrow> ?Jmp jmps s1 \<and> ?Upd v s1" 
schirmer@13688
   299
        (is "PROP ?Hyp t s0 s1 v")
schirmer@13688
   300
  -- {* We need to abstract over @{term jmps} since @{term jmps} are extended
schirmer@13688
   301
        during analysis of @{term Lab}. Also we need to abstract over 
schirmer@13688
   302
        @{term T} and @{term Env} since they are altered in various
schirmer@13688
   303
        typing judgements. *}    
schirmer@13688
   304
  proof (induct)   
schirmer@13688
   305
    case Abrupt thus ?case by simp 
schirmer@13688
   306
  next
schirmer@13688
   307
    case Skip thus ?case by simp
schirmer@13688
   308
  next
schirmer@13688
   309
    case Expr thus ?case by (elim wt_elim_cases) simp
schirmer@13688
   310
  next
berghofe@21765
   311
    case (Lab s0 c s1 jmp jmps T Env) 
wenzelm@23350
   312
    note jmpOK = `jumpNestingOk jmps (In1r (jmp\<bullet> c))`
wenzelm@23350
   313
    note G = `prg Env = G`
schirmer@13688
   314
    have wt_c: "Env\<turnstile>c\<Colon>\<surd>" 
schirmer@13688
   315
      using Lab.prems by (elim wt_elim_cases)
schirmer@13688
   316
    { 
schirmer@13688
   317
      fix j
schirmer@13688
   318
      assume ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)"
schirmer@13688
   319
      have "j\<in>jmps"          
schirmer@13688
   320
      proof -
schirmer@13688
   321
        from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
schirmer@13688
   322
          by (cases s1) (simp add: absorb_def)
wenzelm@23350
   323
        note hyp_c = `PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>`
schirmer@13688
   324
        from ab_s1 have "j \<noteq> jmp" 
schirmer@13688
   325
          by (cases s1) (simp add: absorb_def)
schirmer@13688
   326
        moreover have "j \<in> {jmp} \<union> jmps"
schirmer@13688
   327
        proof -
schirmer@13688
   328
          from jmpOK 
schirmer@13688
   329
          have "jumpNestingOk ({jmp} \<union> jmps) (In1r c)" by simp
schirmer@13688
   330
          with wt_c jmp_s1 G hyp_c
schirmer@13688
   331
          show ?thesis
schirmer@13688
   332
            by - (rule hyp_c [THEN conjunct1,rule_format],simp)
schirmer@13688
   333
        qed
schirmer@13688
   334
        ultimately show ?thesis
schirmer@13688
   335
          by simp
schirmer@13688
   336
      qed
schirmer@13688
   337
    }
schirmer@13688
   338
    thus ?case by simp
schirmer@13688
   339
  next
berghofe@21765
   340
    case (Comp s0 c1 s1 c2 s2 jmps T Env)
wenzelm@23350
   341
    note jmpOk = `jumpNestingOk jmps (In1r (c1;; c2))`
wenzelm@23350
   342
    note G = `prg Env = G`
wenzelm@23350
   343
    from Comp.prems obtain
schirmer@13688
   344
      wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
schirmer@13688
   345
      by (elim wt_elim_cases)
schirmer@13688
   346
    {
schirmer@13688
   347
      fix j
schirmer@13688
   348
      assume abr_s2: "abrupt s2 = Some (Jump j)"
schirmer@13688
   349
      have "j\<in>jmps"
schirmer@13688
   350
      proof -
schirmer@13688
   351
        have jmp: "?Jmp jmps s1"
schirmer@13688
   352
        proof -
wenzelm@23350
   353
          note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>`
schirmer@13688
   354
          with wt_c1 jmpOk G 
schirmer@13688
   355
          show ?thesis by simp
schirmer@13688
   356
        qed
wenzelm@23350
   357
        moreover note hyp_c2 = `PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)`
schirmer@13688
   358
        have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
schirmer@13688
   359
        moreover note wt_c2 G abr_s2
schirmer@13688
   360
        ultimately show "j \<in> jmps"
schirmer@13688
   361
          by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
schirmer@13688
   362
      qed
schirmer@13688
   363
    } thus ?case by simp
schirmer@13688
   364
  next
berghofe@21765
   365
    case (If s0 e b s1 c1 c2 s2 jmps T Env)
wenzelm@23350
   366
    note jmpOk = `jumpNestingOk jmps (In1r (If(e) c1 Else c2))`
wenzelm@23350
   367
    note G = `prg Env = G`
schirmer@13688
   368
    from If.prems obtain 
schirmer@13688
   369
              wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
schirmer@13688
   370
      wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
schirmer@13688
   371
      by (elim wt_elim_cases) simp
schirmer@13688
   372
    { 
schirmer@13688
   373
      fix j
schirmer@13688
   374
      assume jmp: "abrupt s2 = Some (Jump j)"
schirmer@13688
   375
      have "j\<in>jmps"
schirmer@13688
   376
      proof -
wenzelm@23350
   377
        note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
schirmer@13688
   378
        with wt_e G have "?Jmp jmps s1" 
schirmer@13688
   379
          by simp
wenzelm@23350
   380
        moreover note hyp_then_else =
wenzelm@23350
   381
          `PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>`
schirmer@13688
   382
        have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
schirmer@13688
   383
          using jmpOk by (cases "the_Bool b") simp_all
schirmer@13688
   384
        moreover note wt_then_else G jmp
schirmer@13688
   385
        ultimately show "j\<in> jmps" 
schirmer@13688
   386
          by (rule hyp_then_else [THEN conjunct1,rule_format (no_asm)])
schirmer@13688
   387
      qed
schirmer@13688
   388
    }
schirmer@13688
   389
    thus ?case by simp
schirmer@13688
   390
  next
berghofe@21765
   391
    case (Loop s0 e b s1 c s2 l s3 jmps T Env)
wenzelm@23350
   392
    note jmpOk = `jumpNestingOk jmps (In1r (l\<bullet> While(e) c))`
wenzelm@23350
   393
    note G = `prg Env = G`
wenzelm@23350
   394
    note wt = `Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
schirmer@13688
   395
    then obtain 
schirmer@13688
   396
              wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
schirmer@13688
   397
              wt_c: "Env\<turnstile>c\<Colon>\<surd>"
schirmer@13688
   398
      by (elim wt_elim_cases)
schirmer@13688
   399
    {
schirmer@13688
   400
      fix j
schirmer@13688
   401
      assume jmp: "abrupt s3 = Some (Jump j)" 
schirmer@13688
   402
      have "j\<in>jmps"
schirmer@13688
   403
      proof -
wenzelm@23350
   404
        note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
schirmer@13688
   405
        with wt_e G have jmp_s1: "?Jmp jmps s1" 
schirmer@13688
   406
          by simp
schirmer@13688
   407
        show ?thesis
wenzelm@32960
   408
        proof (cases "the_Bool b")
schirmer@13688
   409
          case False
schirmer@13688
   410
          from Loop.hyps
schirmer@13688
   411
          have "s3=s1"
schirmer@13688
   412
            by (simp (no_asm_use) only: if_False False) 
schirmer@13688
   413
          with jmp_s1 jmp have "j \<in> jmps" by simp
schirmer@13688
   414
          thus ?thesis by simp
schirmer@13688
   415
        next
schirmer@13688
   416
          case True
schirmer@13688
   417
          from Loop.hyps 
schirmer@13688
   418
            (* Because of the mixture of object and pure logic in the rule 
schirmer@13688
   419
               eval.If the atomization-rulification of the induct method 
schirmer@13688
   420
               leaves the hypothesis in object logic *)
schirmer@13688
   421
          have "?HypObj (In1r c) s1 s2 (\<diamondsuit>::vals)"
schirmer@13688
   422
            apply (simp (no_asm_use) only: True if_True )
schirmer@13688
   423
            apply (erule conjE)+
schirmer@13688
   424
            apply assumption
schirmer@13688
   425
            done
schirmer@13688
   426
          note hyp_c = this [rule_format (no_asm)]
schirmer@13688
   427
          moreover from jmpOk have "jumpNestingOk ({Cont l} \<union> jmps) (In1r c)"
schirmer@13688
   428
            by simp
schirmer@13688
   429
          moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
schirmer@13688
   430
          ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2" 
nipkow@17589
   431
            using wt_c G by iprover
schirmer@13688
   432
          have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
schirmer@13688
   433
          proof -
schirmer@13688
   434
            {
wenzelm@32960
   435
              fix j'
wenzelm@32960
   436
              assume abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')"
wenzelm@32960
   437
              have "j' \<in> jmps"
wenzelm@32960
   438
              proof (cases "j' = Cont l")
wenzelm@32960
   439
                case True
wenzelm@32960
   440
                with abs show ?thesis
wenzelm@32960
   441
                  by (cases s2) (simp add: absorb_def)
wenzelm@32960
   442
              next
wenzelm@32960
   443
                case False 
wenzelm@32960
   444
                with abs have "abrupt s2 = Some (Jump j')"
wenzelm@32960
   445
                  by (cases s2) (simp add: absorb_def) 
wenzelm@32960
   446
                with jmp_s2 False show ?thesis
wenzelm@32960
   447
                  by simp
wenzelm@32960
   448
              qed
schirmer@13688
   449
            }
schirmer@13688
   450
            thus ?thesis by simp
schirmer@13688
   451
          qed
schirmer@13688
   452
          moreover
schirmer@13688
   453
          from Loop.hyps
schirmer@13688
   454
          have "?HypObj (In1r (l\<bullet> While(e) c)) 
schirmer@13688
   455
                        (abupd (absorb (Cont l)) s2) s3 (\<diamondsuit>::vals)"
schirmer@13688
   456
            apply (simp (no_asm_use) only: True if_True)
schirmer@13688
   457
            apply (erule conjE)+
schirmer@13688
   458
            apply assumption
schirmer@13688
   459
            done
schirmer@13688
   460
          note hyp_w = this [rule_format (no_asm)]
schirmer@13688
   461
          note jmpOk wt G jmp 
schirmer@13688
   462
          ultimately show "j\<in> jmps" 
schirmer@13688
   463
            by (rule hyp_w [THEN conjunct1,rule_format (no_asm)])
schirmer@13688
   464
        qed
schirmer@13688
   465
      qed
schirmer@13688
   466
    }
schirmer@13688
   467
    thus ?case by simp
schirmer@13688
   468
  next
berghofe@21765
   469
    case (Jmp s j jmps T Env) thus ?case by simp
schirmer@13688
   470
  next
berghofe@21765
   471
    case (Throw s0 e a s1 jmps T Env)
wenzelm@23350
   472
    note jmpOk = `jumpNestingOk jmps (In1r (Throw e))`
wenzelm@23350
   473
    note G = `prg Env = G`
schirmer@13688
   474
    from Throw.prems obtain Te where 
schirmer@13688
   475
      wt_e: "Env\<turnstile>e\<Colon>-Te" 
schirmer@13688
   476
      by (elim wt_elim_cases)
schirmer@13688
   477
    {
schirmer@13688
   478
      fix j
schirmer@13688
   479
      assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
schirmer@13688
   480
      have "j\<in>jmps"
schirmer@13688
   481
      proof -
wenzelm@23350
   482
        from `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
wenzelm@23350
   483
        have "?Jmp jmps s1" using wt_e G by simp
schirmer@13688
   484
        moreover
schirmer@13688
   485
        from jmp 
schirmer@13688
   486
        have "abrupt s1 = Some (Jump j)"
schirmer@13688
   487
          by (cases s1) (simp add: throw_def abrupt_if_def)
schirmer@13688
   488
        ultimately show "j \<in> jmps" by simp
schirmer@13688
   489
      qed
schirmer@13688
   490
    }
schirmer@13688
   491
    thus ?case by simp
schirmer@13688
   492
  next
berghofe@21765
   493
    case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
wenzelm@23350
   494
    note jmpOk = `jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))`
wenzelm@23350
   495
    note G = `prg Env = G`
schirmer@13688
   496
    from Try.prems obtain 
schirmer@13688
   497
      wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and  
schirmer@13688
   498
      wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
schirmer@13688
   499
      by (elim wt_elim_cases)
schirmer@13688
   500
    {
schirmer@13688
   501
      fix j
schirmer@13688
   502
      assume jmp: "abrupt s3 = Some (Jump j)"
schirmer@13688
   503
      have "j\<in>jmps"
schirmer@13688
   504
      proof -
wenzelm@23350
   505
        note `PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)`
schirmer@13688
   506
        with jmpOk wt_c1 G
schirmer@13688
   507
        have jmp_s1: "?Jmp jmps s1" by simp
wenzelm@23350
   508
        note s2 = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
schirmer@13688
   509
        show "j \<in> jmps"
schirmer@13688
   510
        proof (cases "G,s2\<turnstile>catch C")
schirmer@13688
   511
          case False
schirmer@13688
   512
          from Try.hyps have "s3=s2" 
wenzelm@32960
   513
            by (simp (no_asm_use) only: False if_False)
schirmer@13688
   514
          with jmp have "abrupt s1 = Some (Jump j)"
schirmer@13688
   515
            using sxalloc_no_jump' [OF s2] by simp
schirmer@13688
   516
          with jmp_s1 
schirmer@13688
   517
          show ?thesis by simp
schirmer@13688
   518
        next
schirmer@13688
   519
          case True
schirmer@13688
   520
          with Try.hyps 
schirmer@13688
   521
          have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3 (\<diamondsuit>::vals)"
schirmer@13688
   522
            apply (simp (no_asm_use) only: True if_True simp_thms)
schirmer@13688
   523
            apply (erule conjE)+
schirmer@13688
   524
            apply assumption
schirmer@13688
   525
            done
schirmer@13688
   526
          note hyp_c2 = this [rule_format (no_asm)]
schirmer@13688
   527
          from jmp_s1 sxalloc_no_jump' [OF s2] 
schirmer@13688
   528
          have "?Jmp jmps s2"
schirmer@13688
   529
            by simp
schirmer@13688
   530
          hence "?Jmp jmps (new_xcpt_var vn s2)"
schirmer@13688
   531
            by (cases s2) simp
schirmer@13688
   532
          moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
schirmer@13688
   533
          moreover note wt_c2
schirmer@13688
   534
          moreover from G 
schirmer@13688
   535
          have "prg (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) = G"
schirmer@13688
   536
            by simp
schirmer@13688
   537
          moreover note jmp
schirmer@13688
   538
          ultimately show ?thesis 
schirmer@13688
   539
            by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
schirmer@13688
   540
        qed
schirmer@13688
   541
      qed
schirmer@13688
   542
    }
schirmer@13688
   543
    thus ?case by simp
schirmer@13688
   544
  next
berghofe@21765
   545
    case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
wenzelm@23350
   546
    note jmpOk = `jumpNestingOk jmps (In1r (c1 Finally c2))`
wenzelm@23350
   547
    note G = `prg Env = G`
schirmer@13688
   548
    from Fin.prems obtain 
schirmer@13688
   549
      wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
schirmer@13688
   550
      by (elim wt_elim_cases)
schirmer@13688
   551
    {
schirmer@13688
   552
      fix j
schirmer@13688
   553
      assume jmp: "abrupt s3 = Some (Jump j)" 
schirmer@13688
   554
      have "j \<in> jmps"
schirmer@13688
   555
      proof (cases "x1=Some (Jump j)")
schirmer@13688
   556
        case True
wenzelm@23350
   557
        note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>`
schirmer@13688
   558
        with True jmpOk wt_c1 G show ?thesis 
schirmer@13688
   559
          by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
schirmer@13688
   560
      next
schirmer@13688
   561
        case False
wenzelm@23350
   562
        note hyp_c2 = `PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>`
wenzelm@23350
   563
        note `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
wenzelm@23350
   564
                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
schirmer@13688
   565
        with False jmp have "abrupt s2 = Some (Jump j)"
wenzelm@23350
   566
          by (cases s2) (simp add: abrupt_if_def)
schirmer@13688
   567
        with jmpOk wt_c2 G show ?thesis 
schirmer@13688
   568
          by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)
schirmer@13688
   569
      qed
schirmer@13688
   570
    }
schirmer@13688
   571
    thus ?case by simp
schirmer@13688
   572
  next
berghofe@21765
   573
    case (Init C c s0 s3 s1 s2 jmps T Env)
wenzelm@23350
   574
    note `jumpNestingOk jmps (In1r (Init C))`
wenzelm@23350
   575
    note G = `prg Env = G`
wenzelm@23350
   576
    note `the (class G C) = c`
schirmer@13688
   577
    with Init.prems have c: "class G C = Some c"
schirmer@13688
   578
      by (elim wt_elim_cases) auto
schirmer@13688
   579
    {
schirmer@13688
   580
      fix j
schirmer@13688
   581
      assume jmp: "abrupt s3 = (Some (Jump j))" 
schirmer@13688
   582
      have "j\<in>jmps"
schirmer@13688
   583
      proof (cases "inited C (globs s0)") 
schirmer@13688
   584
        case True
schirmer@13688
   585
        with Init.hyps have "s3=Norm s0"
schirmer@13688
   586
          by simp
schirmer@13688
   587
        with jmp
schirmer@13688
   588
        have "False" by simp thus ?thesis ..
schirmer@13688
   589
      next
schirmer@13688
   590
        case False
schirmer@13688
   591
        from wf c G
schirmer@13688
   592
        have wf_cdecl: "wf_cdecl G (C,c)"
schirmer@13688
   593
          by (simp add: wf_prog_cdecl)
schirmer@13688
   594
        from Init.hyps
schirmer@13688
   595
        have "?HypObj (In1r (if C = Object then Skip else Init (super c))) 
schirmer@13688
   596
                            (Norm ((init_class_obj G C) s0)) s1 (\<diamondsuit>::vals)"
schirmer@13688
   597
          apply (simp (no_asm_use) only: False if_False simp_thms)
schirmer@13688
   598
          apply (erule conjE)+
schirmer@13688
   599
          apply assumption
schirmer@13688
   600
          done
schirmer@13688
   601
        note hyp_s1 = this [rule_format (no_asm)]
schirmer@13688
   602
        from wf_cdecl G have
schirmer@13688
   603
          wt_super: "Env\<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
schirmer@13688
   604
          by (cases "C=Object")
schirmer@13688
   605
             (auto dest: wf_cdecl_supD is_acc_classD) 
schirmer@13688
   606
        from hyp_s1 [OF _ _ wt_super G]
schirmer@13688
   607
        have "?Jmp jmps s1" 
schirmer@13688
   608
          by simp
schirmer@13688
   609
        hence jmp_s1: "?Jmp jmps ((set_lvars empty) s1)" by (cases s1) simp
schirmer@13688
   610
        from False Init.hyps
schirmer@13688
   611
        have "?HypObj (In1r (init c)) ((set_lvars empty) s1) s2 (\<diamondsuit>::vals)" 
schirmer@13688
   612
          apply (simp (no_asm_use) only: False if_False simp_thms)
schirmer@13688
   613
          apply (erule conjE)+
schirmer@13688
   614
          apply assumption
schirmer@13688
   615
          done
schirmer@13688
   616
        note hyp_init_c = this [rule_format (no_asm)] 
schirmer@13688
   617
        from wf_cdecl 
schirmer@13688
   618
        have wt_init_c: "\<lparr>prg = G, cls = C, lcl = empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
schirmer@13688
   619
          by (rule wf_cdecl_wt_init)
schirmer@13688
   620
        from wf_cdecl have "jumpNestingOkS {} (init c)" 
schirmer@13688
   621
          by (cases rule: wf_cdeclE)
schirmer@13688
   622
        hence "jumpNestingOkS jmps (init c)"
schirmer@13688
   623
          by (rule jumpNestingOkS_mono) simp
schirmer@13688
   624
        moreover 
schirmer@13688
   625
        have "abrupt s2 = Some (Jump j)"
schirmer@13688
   626
        proof -
schirmer@13688
   627
          from False Init.hyps 
schirmer@13688
   628
          have "s3 = (set_lvars (locals (store s1))) s2"  by simp
schirmer@13688
   629
          with jmp show ?thesis by (cases s2) simp
schirmer@13688
   630
        qed
schirmer@13688
   631
        ultimately show ?thesis
schirmer@13688
   632
          using hyp_init_c [OF jmp_s1 _ wt_init_c]
schirmer@13688
   633
          by simp
schirmer@13688
   634
      qed
schirmer@13688
   635
    }
schirmer@13688
   636
    thus ?case by simp
schirmer@13688
   637
  next
berghofe@21765
   638
    case (NewC s0 C s1 a s2 jmps T Env)
schirmer@13688
   639
    {
schirmer@13688
   640
      fix j
schirmer@13688
   641
      assume jmp: "abrupt s2 = Some (Jump j)"
schirmer@13688
   642
      have "j\<in>jmps"
schirmer@13688
   643
      proof - 
wenzelm@23350
   644
        note `prg Env = G`
wenzelm@23350
   645
        moreover note hyp_init = `PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>`
schirmer@13688
   646
        moreover from wf NewC.prems 
schirmer@13688
   647
        have "Env\<turnstile>(Init C)\<Colon>\<surd>"
schirmer@13688
   648
          by (elim wt_elim_cases) (drule is_acc_classD,simp)
schirmer@13688
   649
        moreover 
schirmer@13688
   650
        have "abrupt s1 = Some (Jump j)"
schirmer@13688
   651
        proof -
wenzelm@23350
   652
          from `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2` and jmp show ?thesis
schirmer@13688
   653
            by (rule halloc_no_jump')
schirmer@13688
   654
        qed
schirmer@13688
   655
        ultimately show "j \<in> jmps" 
schirmer@13688
   656
          by - (rule hyp_init [THEN conjunct1,rule_format (no_asm)],auto)
schirmer@13688
   657
      qed
schirmer@13688
   658
    }
schirmer@13688
   659
    thus ?case by simp
schirmer@13688
   660
  next
berghofe@21765
   661
    case (NewA s0 elT s1 e i s2 a s3 jmps T Env)
schirmer@13688
   662
    {
schirmer@13688
   663
      fix j
schirmer@13688
   664
      assume jmp: "abrupt s3 = Some (Jump j)"
schirmer@13688
   665
      have "j\<in>jmps"
schirmer@13688
   666
      proof -
wenzelm@32960
   667
        note G = `prg Env = G`
schirmer@13688
   668
        from NewA.prems 
schirmer@13688
   669
        obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
schirmer@13688
   670
               wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
schirmer@13688
   671
          by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
wenzelm@23350
   672
        note `PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>`
schirmer@13688
   673
        with wt_init G 
schirmer@13688
   674
        have "?Jmp jmps s1" 
schirmer@13688
   675
          by (simp add: init_comp_ty_def)
schirmer@13688
   676
        moreover
wenzelm@23350
   677
        note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 i)`
schirmer@13688
   678
        have "abrupt s2 = Some (Jump j)"
schirmer@13688
   679
        proof -
wenzelm@23350
   680
          note `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
schirmer@13688
   681
          moreover note jmp
schirmer@13688
   682
          ultimately 
schirmer@13688
   683
          have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
schirmer@13688
   684
            by (rule halloc_no_jump')
schirmer@13688
   685
          thus ?thesis by (cases s2) auto
schirmer@13688
   686
        qed
schirmer@13688
   687
        ultimately show "j\<in>jmps" using wt_size G 
schirmer@13688
   688
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)
schirmer@13688
   689
      qed
schirmer@13688
   690
    }
schirmer@13688
   691
    thus ?case by simp
schirmer@13688
   692
  next
berghofe@21765
   693
    case (Cast s0 e v s1 s2 cT jmps T Env)
schirmer@13688
   694
    {
schirmer@13688
   695
      fix j
schirmer@13688
   696
      assume jmp: "abrupt s2 = Some (Jump j)"
schirmer@13688
   697
      have "j\<in>jmps"
schirmer@13688
   698
      proof -
wenzelm@23350
   699
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
wenzelm@23350
   700
        note `prg Env = G`
schirmer@13688
   701
        moreover from Cast.prems
schirmer@13688
   702
        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
schirmer@13688
   703
        moreover 
schirmer@13688
   704
        have "abrupt s1 = Some (Jump j)"
schirmer@13688
   705
        proof -
wenzelm@23350
   706
          note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
schirmer@13688
   707
          moreover note jmp
schirmer@13688
   708
          ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
schirmer@13688
   709
        qed
schirmer@13688
   710
        ultimately show ?thesis 
schirmer@13688
   711
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
schirmer@13688
   712
      qed
schirmer@13688
   713
    }
schirmer@13688
   714
    thus ?case by simp
schirmer@13688
   715
  next
berghofe@21765
   716
    case (Inst s0 e v s1 b eT jmps T Env)
schirmer@13688
   717
    {
schirmer@13688
   718
      fix j
schirmer@13688
   719
      assume jmp: "abrupt s1 = Some (Jump j)"
schirmer@13688
   720
      have "j\<in>jmps"
schirmer@13688
   721
      proof -
wenzelm@23350
   722
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
wenzelm@23350
   723
        note `prg Env = G`
schirmer@13688
   724
        moreover from Inst.prems
schirmer@13688
   725
        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
schirmer@13688
   726
        moreover note jmp
schirmer@13688
   727
        ultimately show "j\<in>jmps" 
schirmer@13688
   728
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
schirmer@13688
   729
      qed
schirmer@13688
   730
    }
schirmer@13688
   731
    thus ?case by simp
schirmer@13688
   732
  next
schirmer@13688
   733
    case Lit thus ?case by simp
schirmer@13688
   734
  next
berghofe@21765
   735
    case (UnOp s0 e v s1 unop jmps T Env)
schirmer@13688
   736
    {
schirmer@13688
   737
      fix j
schirmer@13688
   738
      assume jmp: "abrupt s1 = Some (Jump j)"
schirmer@13688
   739
      have "j\<in>jmps"
schirmer@13688
   740
      proof -
wenzelm@23350
   741
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
wenzelm@23350
   742
        note `prg Env = G`
schirmer@13688
   743
        moreover from UnOp.prems
schirmer@13688
   744
        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
schirmer@13688
   745
        moreover note jmp
schirmer@13688
   746
        ultimately show  "j\<in>jmps" 
schirmer@13688
   747
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all) 
schirmer@13688
   748
      qed
schirmer@13688
   749
    }
schirmer@13688
   750
    thus ?case by simp
schirmer@13688
   751
  next
berghofe@21765
   752
    case (BinOp s0 e1 v1 s1 binop e2 v2 s2 jmps T Env)
schirmer@13688
   753
    {
schirmer@13688
   754
      fix j
schirmer@13688
   755
      assume jmp: "abrupt s2 = Some (Jump j)"
schirmer@13688
   756
      have "j\<in>jmps"
schirmer@13688
   757
      proof -
wenzelm@23350
   758
        note G = `prg Env = G`
schirmer@13688
   759
        from BinOp.prems
schirmer@13688
   760
        obtain e1T e2T where 
schirmer@13688
   761
          wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
schirmer@13688
   762
          wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
schirmer@13688
   763
          by (elim wt_elim_cases)
wenzelm@23350
   764
        note `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)`
schirmer@13688
   765
        with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
wenzelm@23350
   766
        note hyp_e2 =
wenzelm@23350
   767
          `PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
wenzelm@23350
   768
                     s1 s2 (In1 v2)`
schirmer@13688
   769
        show "j\<in>jmps"
schirmer@13688
   770
        proof (cases "need_second_arg binop v1")
schirmer@13688
   771
          case True with jmp_s1 wt_e2 jmp G
schirmer@13688
   772
          show ?thesis 
schirmer@13688
   773
            by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
schirmer@13688
   774
        next
schirmer@13688
   775
          case False with jmp_s1 jmp G
schirmer@13688
   776
          show ?thesis 
schirmer@13688
   777
            by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],auto)
schirmer@13688
   778
        qed
schirmer@13688
   779
      qed
schirmer@13688
   780
    }
schirmer@13688
   781
    thus ?case by simp
schirmer@13688
   782
  next
schirmer@13688
   783
    case Super thus ?case by simp
schirmer@13688
   784
  next
berghofe@21765
   785
    case (Acc s0 va v f s1 jmps T Env)
schirmer@13688
   786
    {
schirmer@13688
   787
      fix j
schirmer@13688
   788
      assume jmp: "abrupt s1 = Some (Jump j)"
schirmer@13688
   789
      have "j\<in>jmps"
schirmer@13688
   790
      proof -
wenzelm@23350
   791
        note hyp_va = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))`
wenzelm@23350
   792
        note `prg Env = G`
schirmer@13688
   793
        moreover from Acc.prems
schirmer@13688
   794
        obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
schirmer@13688
   795
        moreover note jmp
schirmer@13688
   796
        ultimately show "j\<in>jmps" 
schirmer@13688
   797
          by - (rule hyp_va [THEN conjunct1,rule_format (no_asm)], simp_all)
schirmer@13688
   798
      qed
schirmer@13688
   799
    }
schirmer@13688
   800
    thus ?case by simp
schirmer@13688
   801
  next
berghofe@21765
   802
    case (Ass s0 va w f s1 e v s2 jmps T Env)
wenzelm@23350
   803
    note G = `prg Env = G`
schirmer@13688
   804
    from Ass.prems
schirmer@13688
   805
    obtain vT eT where
schirmer@13688
   806
      wt_va: "Env\<turnstile>va\<Colon>=vT" and
schirmer@13688
   807
       wt_e: "Env\<turnstile>e\<Colon>-eT"
schirmer@13688
   808
      by (elim wt_elim_cases)
wenzelm@23350
   809
    note hyp_v = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))`
wenzelm@23350
   810
    note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 v)`
schirmer@13688
   811
    {
schirmer@13688
   812
      fix j
schirmer@13688
   813
      assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
schirmer@13688
   814
      have "j\<in>jmps"
schirmer@13688
   815
      proof -
schirmer@13688
   816
        have "abrupt s2 = Some (Jump j)"
schirmer@13688
   817
        proof (cases "normal s2")
schirmer@13688
   818
          case True
wenzelm@23350
   819
          from `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2` and True have nrm_s1: "normal s1" 
schirmer@13688
   820
            by (rule eval_no_abrupt_lemma [rule_format]) 
schirmer@13688
   821
          with nrm_s1 wt_va G True
schirmer@13688
   822
          have "abrupt (f v s2) \<noteq> Some (Jump j)"
schirmer@13688
   823
            using hyp_v [THEN conjunct2,rule_format (no_asm)]
schirmer@13688
   824
            by simp
schirmer@13688
   825
          from this jmp
schirmer@13688
   826
          show ?thesis
schirmer@13688
   827
            by (rule assign_abrupt_propagation)
schirmer@13688
   828
        next
schirmer@13688
   829
          case False with jmp 
schirmer@13688
   830
          show ?thesis by (cases s2) (simp add: assign_def Let_def)
schirmer@13688
   831
        qed
schirmer@13688
   832
        moreover from wt_va G
schirmer@13688
   833
        have "?Jmp jmps s1"
schirmer@13688
   834
          by - (rule hyp_v [THEN conjunct1],simp_all)
schirmer@13688
   835
        ultimately show ?thesis using G 
wenzelm@23350
   836
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)
schirmer@13688
   837
      qed
schirmer@13688
   838
    }
schirmer@13688
   839
    thus ?case by simp
schirmer@13688
   840
  next
berghofe@21765
   841
    case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)
wenzelm@23350
   842
    note G = `prg Env = G`
wenzelm@23350
   843
    note hyp_e0 = `PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)`
wenzelm@23350
   844
    note hyp_e1_e2 = `PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)`
schirmer@13688
   845
    from Cond.prems
schirmer@13688
   846
    obtain e1T e2T
schirmer@13688
   847
      where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"
schirmer@13688
   848
       and  wt_e1: "Env\<turnstile>e1\<Colon>-e1T"
schirmer@13688
   849
       and  wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
schirmer@13688
   850
      by (elim wt_elim_cases)
schirmer@13688
   851
    {
schirmer@13688
   852
      fix j
schirmer@13688
   853
      assume jmp: "abrupt s2 = Some (Jump j)"
schirmer@13688
   854
      have "j\<in>jmps" 
schirmer@13688
   855
      proof -
schirmer@13688
   856
        from wt_e0 G 
schirmer@13688
   857
        have jmp_s1: "?Jmp jmps s1"
schirmer@13688
   858
          by - (rule hyp_e0 [THEN conjunct1],simp_all)
schirmer@13688
   859
        show ?thesis
schirmer@13688
   860
        proof (cases "the_Bool b")
schirmer@13688
   861
          case True
schirmer@13688
   862
          with jmp_s1 wt_e1 G jmp
schirmer@13688
   863
          show ?thesis
schirmer@13688
   864
            by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
schirmer@13688
   865
        next
schirmer@13688
   866
          case False
schirmer@13688
   867
          with jmp_s1 wt_e2 G jmp
schirmer@13688
   868
          show ?thesis
schirmer@13688
   869
            by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
schirmer@13688
   870
        qed
schirmer@13688
   871
      qed
schirmer@13688
   872
    }
schirmer@13688
   873
    thus ?case by simp
schirmer@13688
   874
  next
berghofe@21765
   875
    case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
schirmer@13688
   876
               jmps T Env)
wenzelm@23350
   877
    note G = `prg Env = G`
schirmer@13688
   878
    from Call.prems
schirmer@13688
   879
    obtain eT argsT 
schirmer@13688
   880
      where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
schirmer@13688
   881
      by (elim wt_elim_cases)
schirmer@13688
   882
    {
schirmer@13688
   883
      fix j
schirmer@13688
   884
      assume jmp: "abrupt ((set_lvars (locals (store s2))) s4) 
schirmer@13688
   885
                     = Some (Jump j)"
schirmer@13688
   886
      have "j\<in>jmps"
schirmer@13688
   887
      proof -
wenzelm@23350
   888
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
schirmer@13688
   889
        from wt_e G 
schirmer@13688
   890
        have jmp_s1: "?Jmp jmps s1"
schirmer@13688
   891
          by - (rule hyp_e [THEN conjunct1],simp_all)
wenzelm@23350
   892
        note hyp_args = `PROP ?Hyp (In3 args) s1 s2 (In3 vs)`
schirmer@13688
   893
        have "abrupt s2 = Some (Jump j)"
schirmer@13688
   894
        proof -
wenzelm@23350
   895
          note `G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4`
schirmer@13688
   896
          moreover
schirmer@13688
   897
          from jmp have "abrupt s4 = Some (Jump j)"
schirmer@13688
   898
            by (cases s4) simp
schirmer@13688
   899
          ultimately have "abrupt s3' = Some (Jump j)"
schirmer@13688
   900
            by - (rule ccontr,drule (1) Methd_no_jump,simp)
wenzelm@23350
   901
          moreover note `s3' = check_method_access G accC statT mode 
wenzelm@23350
   902
                              \<lparr>name = mn, parTs = pTs\<rparr> a s3`
schirmer@13688
   903
          ultimately have "abrupt s3 = Some (Jump j)"
schirmer@13688
   904
            by (cases s3) 
schirmer@13688
   905
               (simp add: check_method_access_def abrupt_if_def Let_def)
schirmer@13688
   906
          moreover 
wenzelm@23350
   907
          note `s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2`
schirmer@13688
   908
          ultimately show ?thesis
schirmer@13688
   909
            by (cases s2) (auto simp add: init_lvars_def2)
schirmer@13688
   910
        qed
schirmer@13688
   911
        with jmp_s1 wt_args G
schirmer@13688
   912
        show ?thesis
schirmer@13688
   913
          by - (rule hyp_args [THEN conjunct1,rule_format (no_asm)], simp_all)
schirmer@13688
   914
      qed
schirmer@13688
   915
    }
schirmer@13688
   916
    thus ?case by simp
schirmer@13688
   917
  next
berghofe@21765
   918
    case (Methd s0 D sig v s1 jmps T Env)
wenzelm@23350
   919
    from `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
schirmer@13688
   920
    have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
schirmer@13688
   921
      by (rule eval.Methd)
schirmer@13688
   922
    hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
   923
      by (rule Methd_no_jump) simp
schirmer@13688
   924
    thus ?case by simp
schirmer@13688
   925
  next
berghofe@21765
   926
    case (Body s0 D s1 c s2 s3 jmps T Env)
schirmer@13688
   927
    have "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
schirmer@13688
   928
           \<rightarrow> abupd (absorb Ret) s3"
wenzelm@23350
   929
      by (rule eval.Body) (rule Body)+
schirmer@13688
   930
    hence "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
schirmer@13688
   931
      by (rule Body_no_jump) simp
schirmer@13688
   932
    thus ?case by simp
schirmer@13688
   933
  next
schirmer@13688
   934
    case LVar
schirmer@13688
   935
    thus ?case by (simp add: lvar_def Let_def)
schirmer@13688
   936
  next
berghofe@21765
   937
    case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)
wenzelm@23350
   938
    note G = `prg Env = G`
schirmer@13688
   939
    from wf FVar.prems 
schirmer@13688
   940
    obtain  statC f where
schirmer@13688
   941
      wt_e: "Env\<turnstile>e\<Colon>-Class statC" and
schirmer@13688
   942
      accfield: "accfield (prg Env) accC statC fn = Some (statDeclC,f)"
schirmer@13688
   943
      by  (elim wt_elim_cases) simp
schirmer@13688
   944
    have wt_init: "Env\<turnstile>Init statDeclC\<Colon>\<surd>"
schirmer@13688
   945
    proof -
schirmer@13688
   946
      from wf wt_e G 
schirmer@13688
   947
      have "is_class (prg Env) statC"
schirmer@13688
   948
        by (auto dest: ty_expr_is_type type_is_class)
schirmer@13688
   949
      with wf accfield G
schirmer@13688
   950
      have "is_class (prg Env) statDeclC"
schirmer@13688
   951
        by (auto dest!: accfield_fields dest: fields_declC)
schirmer@13688
   952
      thus ?thesis
schirmer@13688
   953
        by simp
schirmer@13688
   954
    qed
wenzelm@23350
   955
    note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
schirmer@13688
   956
    {
schirmer@13688
   957
      fix j
schirmer@13688
   958
      assume jmp: "abrupt s3 = Some (Jump j)"
schirmer@13688
   959
      have "j\<in>jmps"
schirmer@13688
   960
      proof -
wenzelm@23350
   961
        note hyp_init = `PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>`
schirmer@13688
   962
        from G wt_init 
schirmer@13688
   963
        have "?Jmp jmps s1"
schirmer@13688
   964
          by - (rule hyp_init [THEN conjunct1],auto)
schirmer@13688
   965
        moreover
wenzelm@23350
   966
        note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 a)`
schirmer@13688
   967
        have "abrupt s2 = Some (Jump j)"
schirmer@13688
   968
        proof -
wenzelm@23350
   969
          note `s3 = check_field_access G accC statDeclC fn stat a s2'`
schirmer@13688
   970
          with jmp have "abrupt s2' = Some (Jump j)"
schirmer@13688
   971
            by (cases s2') 
schirmer@13688
   972
               (simp add: check_field_access_def abrupt_if_def Let_def)
schirmer@13688
   973
         with fvar show "abrupt s2 =  Some (Jump j)"
schirmer@13688
   974
            by (cases s2) (simp add: fvar_def2 abrupt_if_def)
schirmer@13688
   975
        qed
schirmer@13688
   976
        ultimately show ?thesis
schirmer@13688
   977
          using G wt_e
schirmer@13688
   978
          by - (rule hyp_e [THEN conjunct1, rule_format (no_asm)],simp_all)
schirmer@13688
   979
      qed
schirmer@13688
   980
    }
schirmer@13688
   981
    moreover
schirmer@13688
   982
    from fvar obtain upd w
schirmer@13688
   983
      where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and
schirmer@13688
   984
              v: "v=(w,upd)"
schirmer@13688
   985
      by (cases "fvar statDeclC stat fn a s2") simp
schirmer@13688
   986
    {
schirmer@13688
   987
      fix j val fix s::state
schirmer@13688
   988
      assume "normal s3"
schirmer@13688
   989
      assume no_jmp: "abrupt s \<noteq> Some (Jump j)"
schirmer@13688
   990
      with upd
schirmer@13688
   991
      have "abrupt (upd val s) \<noteq> Some (Jump j)"
schirmer@13688
   992
        by (rule fvar_upd_no_jump)
schirmer@13688
   993
    }
schirmer@13688
   994
    ultimately show ?case using v by simp
schirmer@13688
   995
  next
berghofe@21765
   996
    case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
wenzelm@23350
   997
    note G = `prg Env = G`
schirmer@13688
   998
    from AVar.prems 
schirmer@13688
   999
    obtain  e1T e2T where
schirmer@13688
  1000
      wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
schirmer@13688
  1001
      by  (elim wt_elim_cases) simp
wenzelm@23350
  1002
    note avar = `(v, s2') = avar G i a s2`
schirmer@13688
  1003
    {
schirmer@13688
  1004
      fix j
schirmer@13688
  1005
      assume jmp: "abrupt s2' = Some (Jump j)"
schirmer@13688
  1006
      have "j\<in>jmps"
schirmer@13688
  1007
      proof -
wenzelm@23350
  1008
        note hyp_e1 = `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)`
schirmer@13688
  1009
        from G wt_e1
schirmer@13688
  1010
        have "?Jmp jmps s1"
wenzelm@23350
  1011
          by - (rule hyp_e1 [THEN conjunct1], auto)
schirmer@13688
  1012
        moreover
wenzelm@23350
  1013
        note hyp_e2 = `PROP ?Hyp (In1l e2) s1 s2 (In1 i)`
schirmer@13688
  1014
        have "abrupt s2 = Some (Jump j)"
schirmer@13688
  1015
        proof -
schirmer@13688
  1016
          from avar have "s2' = snd (avar G i a s2)"
schirmer@13688
  1017
            by (cases "avar G i a s2") simp
schirmer@13688
  1018
          with jmp show ?thesis by - (rule avar_state_no_jump,simp) 
schirmer@13688
  1019
        qed  
schirmer@13688
  1020
        ultimately show ?thesis
schirmer@13688
  1021
          using wt_e2 G
schirmer@13688
  1022
          by - (rule hyp_e2 [THEN conjunct1, rule_format (no_asm)],simp_all)
schirmer@13688
  1023
      qed
schirmer@13688
  1024
    }
schirmer@13688
  1025
    moreover
schirmer@13688
  1026
    from avar obtain upd w
schirmer@13688
  1027
      where upd: "upd = snd (fst (avar G i a s2))" and
schirmer@13688
  1028
              v: "v=(w,upd)"
schirmer@13688
  1029
      by (cases "avar G i a s2") simp
schirmer@13688
  1030
    {
schirmer@13688
  1031
      fix j val fix s::state
schirmer@13688
  1032
      assume "normal s2'"
schirmer@13688
  1033
      assume no_jmp: "abrupt s \<noteq> Some (Jump j)"
schirmer@13688
  1034
      with upd
schirmer@13688
  1035
      have "abrupt (upd val s) \<noteq> Some (Jump j)"
schirmer@13688
  1036
        by (rule avar_upd_no_jump)
schirmer@13688
  1037
    }
schirmer@13688
  1038
    ultimately show ?case using v by simp
schirmer@13688
  1039
  next
schirmer@13688
  1040
    case Nil thus ?case by simp
schirmer@13688
  1041
  next
berghofe@21765
  1042
    case (Cons s0 e v s1 es vs s2 jmps T Env)
wenzelm@23350
  1043
    note G = `prg Env = G`
schirmer@13688
  1044
    from Cons.prems obtain eT esT
schirmer@13688
  1045
      where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_e2: "Env\<turnstile>es\<Colon>\<doteq>esT"
schirmer@13688
  1046
      by  (elim wt_elim_cases) simp
schirmer@13688
  1047
    {
schirmer@13688
  1048
      fix j
schirmer@13688
  1049
      assume jmp: "abrupt s2 = Some (Jump j)"
schirmer@13688
  1050
      have "j\<in>jmps"
schirmer@13688
  1051
      proof -
wenzelm@23350
  1052
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
schirmer@13688
  1053
        from G wt_e
schirmer@13688
  1054
        have "?Jmp jmps s1"
schirmer@13688
  1055
          by - (rule hyp_e [THEN conjunct1],simp_all)
schirmer@13688
  1056
        moreover
wenzelm@23350
  1057
        note hyp_es = `PROP ?Hyp (In3 es) s1 s2 (In3 vs)`
schirmer@13688
  1058
        ultimately show ?thesis
schirmer@13688
  1059
          using wt_e2 G jmp
schirmer@13688
  1060
          by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
schirmer@13688
  1061
                (assumption|simp (no_asm_simp))+)
schirmer@13688
  1062
      qed
schirmer@13688
  1063
    }
schirmer@13688
  1064
    thus ?case by simp
schirmer@13688
  1065
  qed
schirmer@13688
  1066
  note generalized = this
schirmer@13688
  1067
  from no_jmp jmpOk wt G
schirmer@13688
  1068
  show ?thesis
schirmer@13688
  1069
    by (rule generalized)
schirmer@13688
  1070
qed
schirmer@13688
  1071
schirmer@13688
  1072
lemmas jumpNestingOk_evalE = jumpNestingOk_eval [THEN conjE,rule_format]
schirmer@13688
  1073
schirmer@13688
  1074
schirmer@13688
  1075
lemma jumpNestingOk_eval_no_jump:
schirmer@13688
  1076
 assumes    eval: "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
schirmer@13688
  1077
           jmpOk: "jumpNestingOk {} t" and
schirmer@13688
  1078
          no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
schirmer@13688
  1079
              wt: "Env\<turnstile>t\<Colon>T" and 
schirmer@13688
  1080
              wf: "wf_prog (prg Env)" 
schirmer@13688
  1081
 shows "abrupt s1 \<noteq> Some (Jump j) \<and>
schirmer@13688
  1082
        (normal s1 \<longrightarrow> v=In2 (w,upd)  
schirmer@13688
  1083
         \<longrightarrow> abrupt s \<noteq> Some (Jump j')
schirmer@13688
  1084
         \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j'))"
schirmer@13688
  1085
proof (cases "\<exists> j'. abrupt s0 = Some (Jump j')") 
schirmer@13688
  1086
  case True
schirmer@13688
  1087
  then obtain j' where jmp: "abrupt s0 = Some (Jump j')" ..
schirmer@13688
  1088
  with no_jmp have "j'\<noteq>j" by simp
schirmer@13688
  1089
  with eval jmp have "s1=s0" by auto
schirmer@13688
  1090
  with no_jmp jmp show ?thesis by simp
schirmer@13688
  1091
next
schirmer@13688
  1092
  case False
schirmer@13688
  1093
  obtain G where G: "prg Env = G"
schirmer@13688
  1094
    by (cases Env) simp
schirmer@13688
  1095
  from G eval have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by simp
schirmer@13688
  1096
  moreover note jmpOk wt
schirmer@13688
  1097
  moreover from G wf have "wf_prog G" by simp
schirmer@13688
  1098
  moreover note G 
schirmer@13688
  1099
  moreover from False have "\<And> j. abrupt s0 = Some (Jump j) \<Longrightarrow> j \<in> {}"
schirmer@13688
  1100
    by simp
schirmer@13688
  1101
  ultimately show ?thesis
schirmer@13688
  1102
    apply (rule jumpNestingOk_evalE)
schirmer@13688
  1103
    apply assumption
schirmer@13688
  1104
    apply simp
schirmer@13688
  1105
    apply fastsimp
schirmer@13688
  1106
    done
schirmer@13688
  1107
qed
schirmer@13688
  1108
schirmer@13688
  1109
lemmas jumpNestingOk_eval_no_jumpE 
schirmer@13688
  1110
       = jumpNestingOk_eval_no_jump [THEN conjE,rule_format]
schirmer@13688
  1111
schirmer@13688
  1112
corollary eval_expression_no_jump:
schirmer@13688
  1113
  assumes eval: "prg Env\<turnstile>s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and
schirmer@13688
  1114
        no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
schirmer@13688
  1115
        wt: "Env\<turnstile>e\<Colon>-T" and 
schirmer@13688
  1116
        wf: "wf_prog (prg Env)" 
schirmer@13688
  1117
  shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
  1118
using eval _ no_jmp wt wf
schirmer@13688
  1119
by (rule jumpNestingOk_eval_no_jumpE, simp_all)
schirmer@13688
  1120
schirmer@13688
  1121
corollary eval_var_no_jump:
schirmer@13688
  1122
  assumes eval: "prg Env\<turnstile>s0 \<midarrow>var=\<succ>(w,upd)\<rightarrow> s1" and
schirmer@13688
  1123
        no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
schirmer@13688
  1124
        wt: "Env\<turnstile>var\<Colon>=T" and 
schirmer@13688
  1125
        wf: "wf_prog (prg Env)" 
schirmer@13688
  1126
  shows "abrupt s1 \<noteq> Some (Jump j) \<and> 
schirmer@13688
  1127
         (normal s1 \<longrightarrow> 
schirmer@13688
  1128
          (abrupt s \<noteq> Some (Jump j') 
schirmer@13688
  1129
           \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j')))"
schirmer@13688
  1130
apply (rule_tac upd="upd" and val="val" and s="s" and w="w" and j'=j' 
schirmer@13688
  1131
         in jumpNestingOk_eval_no_jumpE [OF eval _ no_jmp wt wf])
schirmer@13688
  1132
by simp_all
schirmer@13688
  1133
schirmer@13688
  1134
lemmas eval_var_no_jumpE = eval_var_no_jump [THEN conjE,rule_format]
schirmer@13688
  1135
schirmer@13688
  1136
corollary eval_statement_no_jump:
schirmer@13688
  1137
  assumes eval: "prg Env\<turnstile>s0 \<midarrow>c\<rightarrow> s1" and
schirmer@13688
  1138
         jmpOk: "jumpNestingOkS {} c" and
schirmer@13688
  1139
        no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
schirmer@13688
  1140
        wt: "Env\<turnstile>c\<Colon>\<surd>" and 
schirmer@13688
  1141
        wf: "wf_prog (prg Env)" 
schirmer@13688
  1142
  shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
  1143
using eval _ no_jmp wt wf
schirmer@13688
  1144
by (rule jumpNestingOk_eval_no_jumpE) (simp_all add: jmpOk)
schirmer@13688
  1145
schirmer@13688
  1146
corollary eval_expression_list_no_jump:
schirmer@13688
  1147
  assumes eval: "prg Env\<turnstile>s0 \<midarrow>es\<doteq>\<succ>v\<rightarrow> s1" and
schirmer@13688
  1148
        no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
schirmer@13688
  1149
        wt: "Env\<turnstile>es\<Colon>\<doteq>T" and 
schirmer@13688
  1150
        wf: "wf_prog (prg Env)" 
schirmer@13688
  1151
  shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
  1152
using eval _ no_jmp wt wf
schirmer@13688
  1153
by (rule jumpNestingOk_eval_no_jumpE, simp_all)
schirmer@13688
  1154
schirmer@13688
  1155
(* ### FIXME: Do i need this *)
schirmer@13688
  1156
lemma union_subseteq_elim [elim]: "\<lbrakk>A \<union> B \<subseteq> C; \<lbrakk>A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
schirmer@13688
  1157
  by blast
schirmer@13688
  1158
schirmer@13688
  1159
lemma dom_locals_halloc_mono:
schirmer@13688
  1160
  assumes halloc: "G\<turnstile>s0\<midarrow>halloc oi\<succ>a\<rightarrow>s1"
schirmer@13688
  1161
  shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1162
proof -
schirmer@13688
  1163
  from halloc show ?thesis
schirmer@13688
  1164
    by cases simp_all
schirmer@13688
  1165
qed
schirmer@13688
  1166
 
schirmer@13688
  1167
lemma dom_locals_sxalloc_mono:
schirmer@13688
  1168
  assumes sxalloc: "G\<turnstile>s0\<midarrow>sxalloc\<rightarrow>s1"
schirmer@13688
  1169
  shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1170
proof -
schirmer@13688
  1171
  from sxalloc show ?thesis
schirmer@13688
  1172
  proof (cases)
schirmer@13688
  1173
    case Norm thus ?thesis by simp
schirmer@13688
  1174
  next
schirmer@13688
  1175
    case Jmp thus ?thesis by simp
schirmer@13688
  1176
  next
schirmer@13688
  1177
    case Error thus ?thesis by simp
schirmer@13688
  1178
  next
schirmer@13688
  1179
    case XcptL thus ?thesis by simp
schirmer@13688
  1180
  next
schirmer@13688
  1181
    case SXcpt thus ?thesis 
schirmer@13688
  1182
      by - (drule dom_locals_halloc_mono,simp)
schirmer@13688
  1183
  qed
schirmer@13688
  1184
qed
schirmer@13688
  1185
    
schirmer@13688
  1186
schirmer@13688
  1187
lemma dom_locals_assign_mono: 
schirmer@13688
  1188
 assumes f_ok: "dom (locals (store s)) \<subseteq> dom (locals (store (f n s)))"
schirmer@13688
  1189
   shows  "dom (locals (store s)) \<subseteq> dom (locals (store (assign f n s)))"
schirmer@13688
  1190
proof (cases "normal s")
schirmer@13688
  1191
  case False thus ?thesis
schirmer@13688
  1192
    by (cases s) (auto simp add: assign_def Let_def)
schirmer@13688
  1193
next
schirmer@13688
  1194
  case True
schirmer@13688
  1195
  then obtain s' where s': "s = (None,s')"
schirmer@13688
  1196
    by auto
schirmer@13688
  1197
  moreover
schirmer@13688
  1198
  obtain x1 s1 where "f n s = (x1,s1)"
wenzelm@23350
  1199
    by (cases "f n s")
schirmer@13688
  1200
  ultimately
schirmer@13688
  1201
  show ?thesis
schirmer@13688
  1202
    using f_ok
schirmer@13688
  1203
    by (simp add: assign_def Let_def)
schirmer@13688
  1204
qed
schirmer@13688
  1205
schirmer@13688
  1206
(*
schirmer@13688
  1207
lemma dom_locals_init_lvars_mono: 
schirmer@13688
  1208
 "dom (locals (store s)) 
schirmer@13688
  1209
   \<subseteq> dom (locals (store (init_lvars G D sig mode a vs s)))"
schirmer@13688
  1210
proof (cases "mode = Static")
schirmer@13688
  1211
  case True
schirmer@13688
  1212
  thus ?thesis
schirmer@13688
  1213
    apply (cases s)
schirmer@13688
  1214
    apply (simp add: init_lvars_def Let_def)
schirmer@13688
  1215
*)
schirmer@13688
  1216
schirmer@13688
  1217
lemma dom_locals_lvar_mono:
schirmer@13688
  1218
 "dom (locals (store s)) \<subseteq> dom (locals (store (snd (lvar vn s') val s)))"
schirmer@13688
  1219
by (simp add: lvar_def) blast
schirmer@13688
  1220
schirmer@13688
  1221
schirmer@13688
  1222
lemma dom_locals_fvar_vvar_mono:
schirmer@13688
  1223
"dom (locals (store s)) 
schirmer@13688
  1224
  \<subseteq> dom (locals (store (snd (fst (fvar statDeclC stat fn a s')) val s)))"
schirmer@13688
  1225
proof (cases stat) 
schirmer@13688
  1226
  case True
schirmer@13688
  1227
  thus ?thesis
schirmer@13688
  1228
    by (cases s) (simp add: fvar_def2)
schirmer@13688
  1229
next
schirmer@13688
  1230
  case False
schirmer@13688
  1231
  thus ?thesis
schirmer@13688
  1232
    by (cases s) (simp add: fvar_def2)
schirmer@13688
  1233
qed
schirmer@13688
  1234
schirmer@13688
  1235
lemma dom_locals_fvar_mono:
schirmer@13688
  1236
"dom (locals (store s)) 
schirmer@13688
  1237
  \<subseteq> dom (locals (store (snd (fvar statDeclC stat fn a s))))"
schirmer@13688
  1238
proof (cases stat) 
schirmer@13688
  1239
  case True
schirmer@13688
  1240
  thus ?thesis
schirmer@13688
  1241
    by (cases s) (simp add: fvar_def2)
schirmer@13688
  1242
next
schirmer@13688
  1243
  case False
schirmer@13688
  1244
  thus ?thesis
schirmer@13688
  1245
    by (cases s) (simp add: fvar_def2)
schirmer@13688
  1246
qed
schirmer@13688
  1247
schirmer@13688
  1248
schirmer@13688
  1249
lemma dom_locals_avar_vvar_mono:
schirmer@13688
  1250
"dom (locals (store s)) 
schirmer@13688
  1251
  \<subseteq> dom (locals (store (snd (fst (avar G i a s')) val s)))"
schirmer@13688
  1252
by (cases s, simp add: avar_def2)
schirmer@13688
  1253
schirmer@13688
  1254
lemma dom_locals_avar_mono:
schirmer@13688
  1255
"dom (locals (store s)) 
schirmer@13688
  1256
  \<subseteq> dom (locals (store (snd (avar G i a s))))"
schirmer@13688
  1257
by (cases s, simp add: avar_def2)
schirmer@13688
  1258
schirmer@13688
  1259
  text {* 
schirmer@13688
  1260
Since assignments are modelled as functions from states to states, we
schirmer@13688
  1261
  must take into account these functions. They  appear only in the assignment 
schirmer@13688
  1262
  rule and as result from evaluating a variable. Thats why we need the 
schirmer@13688
  1263
  complicated second part of the conjunction in the goal.
schirmer@13688
  1264
 The reason for the very generic way to treat assignments was the aim
schirmer@13688
  1265
to omit redundancy. There is only one evaluation rule for each kind of
schirmer@13688
  1266
variable (locals, fields, arrays). These rules are used for both accessing 
schirmer@13688
  1267
variables and updating variables. Thats why the evaluation rules for variables
schirmer@13688
  1268
result in a pair consisting of a value and an update function. Of course we
schirmer@13688
  1269
could also think of a pair of a value and a reference in the store, instead of
schirmer@13688
  1270
the generic update function. But as only array updates can cause a special
schirmer@13688
  1271
exception (if the types mismatch) and not array reads we then have to introduce
schirmer@13688
  1272
two different rules to handle array reads and updates *} 
schirmer@13688
  1273
lemma dom_locals_eval_mono: 
schirmer@13688
  1274
  assumes   eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
schirmer@13688
  1275
  shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1)) \<and>
schirmer@13688
  1276
         (\<forall> vv. v=In2 vv \<and> normal s1 
schirmer@13688
  1277
            \<longrightarrow> (\<forall> s val. dom (locals (store s)) 
schirmer@13688
  1278
                           \<subseteq> dom (locals (store ((snd vv) val s)))))"
schirmer@13688
  1279
proof -
schirmer@13688
  1280
  from eval show ?thesis
schirmer@13688
  1281
  proof (induct)
schirmer@13688
  1282
    case Abrupt thus ?case by simp 
schirmer@13688
  1283
  next
schirmer@13688
  1284
    case Skip thus ?case by simp
schirmer@13688
  1285
  next
schirmer@13688
  1286
    case Expr thus ?case by simp
schirmer@13688
  1287
  next
schirmer@13688
  1288
    case Lab thus ?case by simp
schirmer@13688
  1289
  next
berghofe@21765
  1290
    case (Comp s0 c1 s1 c2 s2) 
schirmer@13688
  1291
    from Comp.hyps 
schirmer@13688
  1292
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1293
      by simp
schirmer@13688
  1294
    also
schirmer@13688
  1295
    from Comp.hyps
schirmer@13688
  1296
    have "\<dots> \<subseteq> dom (locals (store s2))" 
schirmer@13688
  1297
      by simp
schirmer@13688
  1298
    finally show ?case by simp
schirmer@13688
  1299
  next
berghofe@21765
  1300
    case (If s0 e b s1 c1 c2 s2)
schirmer@13688
  1301
    from If.hyps 
schirmer@13688
  1302
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1303
      by simp
schirmer@13688
  1304
    also
schirmer@13688
  1305
    from If.hyps
schirmer@13688
  1306
    have "\<dots> \<subseteq> dom (locals (store s2))" 
schirmer@13688
  1307
      by simp
schirmer@13688
  1308
    finally show ?case by simp
schirmer@13688
  1309
  next
berghofe@21765
  1310
    case (Loop s0 e b s1 c s2 l s3) 
schirmer@13688
  1311
    show ?case
schirmer@13688
  1312
    proof (cases "the_Bool b")
schirmer@13688
  1313
      case True
schirmer@13688
  1314
      with Loop.hyps
schirmer@13688
  1315
      obtain
wenzelm@32960
  1316
        s0_s1: 
wenzelm@32960
  1317
        "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" and
wenzelm@32960
  1318
        s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" and
wenzelm@32960
  1319
        s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
wenzelm@32960
  1320
        by simp
schirmer@13688
  1321
      note s0_s1 also note s1_s2 also note s2_s3
schirmer@13688
  1322
      finally show ?thesis
wenzelm@32960
  1323
        by simp
schirmer@13688
  1324
    next
schirmer@13688
  1325
      case False
schirmer@13688
  1326
      with Loop.hyps show ?thesis
wenzelm@32960
  1327
        by simp
schirmer@13688
  1328
    qed
schirmer@13688
  1329
  next
schirmer@13688
  1330
    case Jmp thus ?case by simp
schirmer@13688
  1331
  next
schirmer@13688
  1332
    case Throw thus ?case by simp
schirmer@13688
  1333
  next
berghofe@21765
  1334
    case (Try s0 c1 s1 s2 C vn c2 s3)
schirmer@13688
  1335
    then
schirmer@13688
  1336
    have s0_s1: "dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1337
                  \<subseteq> dom (locals (store s1))" by simp
wenzelm@23350
  1338
    from `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
wenzelm@23350
  1339
    have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" 
schirmer@13688
  1340
      by (rule dom_locals_sxalloc_mono)
schirmer@13688
  1341
    thus ?case 
schirmer@13688
  1342
    proof (cases "G,s2\<turnstile>catch C")
schirmer@13688
  1343
      case True
schirmer@13688
  1344
      note s0_s1 also note s1_s2
schirmer@13688
  1345
      also
schirmer@13688
  1346
      from True Try.hyps 
schirmer@13688
  1347
      have "dom (locals (store (new_xcpt_var vn s2))) 
schirmer@13688
  1348
              \<subseteq> dom (locals (store s3))"
wenzelm@32960
  1349
        by simp
schirmer@13688
  1350
      hence "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
wenzelm@32960
  1351
        by (cases s2, simp )
schirmer@13688
  1352
      finally show ?thesis by simp
schirmer@13688
  1353
    next
schirmer@13688
  1354
      case False
schirmer@13688
  1355
      note s0_s1 also note s1_s2
schirmer@13688
  1356
      finally 
schirmer@13688
  1357
      show ?thesis 
wenzelm@32960
  1358
        using False Try.hyps by simp
schirmer@13688
  1359
    qed
schirmer@13688
  1360
  next
berghofe@21765
  1361
    case (Fin s0 c1 x1 s1 c2 s2 s3) 
schirmer@13688
  1362
    show ?case
schirmer@13688
  1363
    proof (cases "\<exists>err. x1 = Some (Error err)")
schirmer@13688
  1364
      case True
schirmer@13688
  1365
      with Fin.hyps show ?thesis
wenzelm@32960
  1366
        by simp
schirmer@13688
  1367
    next
schirmer@13688
  1368
      case False
schirmer@13688
  1369
      from Fin.hyps
schirmer@13688
  1370
      have "dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1371
             \<subseteq> dom (locals (store (x1, s1)))" 
wenzelm@32960
  1372
        by simp
schirmer@13688
  1373
      hence "dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1374
              \<subseteq> dom (locals (store ((Norm s1)::state)))"
wenzelm@32960
  1375
        by simp
schirmer@13688
  1376
      also
schirmer@13688
  1377
      from Fin.hyps
schirmer@13688
  1378
      have "\<dots> \<subseteq> dom (locals (store s2))"
wenzelm@32960
  1379
        by simp
schirmer@13688
  1380
      finally show ?thesis 
wenzelm@32960
  1381
        using Fin.hyps by simp
schirmer@13688
  1382
    qed
schirmer@13688
  1383
  next
berghofe@21765
  1384
    case (Init C c s0 s3 s1 s2)
schirmer@13688
  1385
    show ?case
schirmer@13688
  1386
    proof (cases "inited C (globs s0)")
schirmer@13688
  1387
      case True
schirmer@13688
  1388
      with Init.hyps show ?thesis by simp 
schirmer@13688
  1389
    next
schirmer@13688
  1390
      case False
schirmer@13688
  1391
      with Init.hyps 
schirmer@13688
  1392
      obtain s0_s1: "dom (locals (store (Norm ((init_class_obj G C) s0))))
schirmer@13688
  1393
                     \<subseteq> dom (locals (store s1))" and
wenzelm@32960
  1394
             s3: "s3 = (set_lvars (locals (snd s1))) s2"
wenzelm@32960
  1395
        by simp
schirmer@13688
  1396
      from s0_s1
schirmer@13688
  1397
      have "dom (locals (store (Norm s0))) \<subseteq> dom (locals (store s1))"
wenzelm@32960
  1398
        by (cases s0) simp
schirmer@13688
  1399
      with s3
schirmer@13688
  1400
      have "dom (locals (store (Norm s0))) \<subseteq> dom (locals (store s3))"
wenzelm@32960
  1401
        by (cases s2) simp
schirmer@13688
  1402
      thus ?thesis by simp
schirmer@13688
  1403
    qed
schirmer@13688
  1404
  next
berghofe@21765
  1405
    case (NewC s0 C s1 a s2)
wenzelm@23350
  1406
    note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
schirmer@13688
  1407
    from NewC.hyps
schirmer@13688
  1408
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
schirmer@13688
  1409
      by simp
schirmer@13688
  1410
    also
schirmer@13688
  1411
    from halloc
schirmer@13688
  1412
    have "\<dots>  \<subseteq> dom (locals (store s2))" by (rule dom_locals_halloc_mono)
schirmer@13688
  1413
    finally show ?case by simp
schirmer@13688
  1414
  next
berghofe@21765
  1415
    case (NewA s0 T s1 e i s2 a s3)
wenzelm@23350
  1416
    note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
schirmer@13688
  1417
    from NewA.hyps
schirmer@13688
  1418
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
schirmer@13688
  1419
      by simp
schirmer@13688
  1420
    also
schirmer@13688
  1421
    from NewA.hyps
schirmer@13688
  1422
    have "\<dots> \<subseteq> dom (locals (store s2))" by simp
schirmer@13688
  1423
    also
schirmer@13688
  1424
    from halloc 
schirmer@13688
  1425
    have "\<dots> \<subseteq>  dom (locals (store s3))"
schirmer@13688
  1426
      by (rule dom_locals_halloc_mono [elim_format]) simp
schirmer@13688
  1427
    finally show ?case by simp
schirmer@13688
  1428
  next
schirmer@13688
  1429
    case Cast thus ?case by simp
schirmer@13688
  1430
  next
schirmer@13688
  1431
    case Inst thus ?case by simp
schirmer@13688
  1432
  next
schirmer@13688
  1433
    case Lit thus ?case by simp
schirmer@13688
  1434
  next
schirmer@13688
  1435
    case UnOp thus ?case by simp
schirmer@13688
  1436
  next
berghofe@21765
  1437
    case (BinOp s0 e1 v1 s1 binop e2 v2 s2) 
schirmer@13688
  1438
    from BinOp.hyps
schirmer@13688
  1439
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
schirmer@13688
  1440
      by simp
schirmer@13688
  1441
    also
schirmer@13688
  1442
    from BinOp.hyps
schirmer@13688
  1443
    have "\<dots> \<subseteq> dom (locals (store s2))" by simp
schirmer@13688
  1444
    finally show ?case by simp
schirmer@13688
  1445
  next
schirmer@13688
  1446
    case Super thus ?case by simp
schirmer@13688
  1447
  next
schirmer@13688
  1448
    case Acc thus ?case by simp
schirmer@13688
  1449
  next
berghofe@21765
  1450
    case (Ass s0 va w f s1 e v s2)
schirmer@13688
  1451
    from Ass.hyps
schirmer@13688
  1452
    have s0_s1: 
schirmer@13688
  1453
      "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
schirmer@13688
  1454
      by simp
schirmer@13688
  1455
    show ?case
schirmer@13688
  1456
    proof (cases "normal s1")
schirmer@13688
  1457
      case True
schirmer@13688
  1458
      with Ass.hyps 
schirmer@13688
  1459
      have ass_ok:
schirmer@13688
  1460
        "\<And> s val. dom (locals (store s)) \<subseteq> dom (locals (store (f val s)))"
wenzelm@32960
  1461
        by simp
schirmer@13688
  1462
      note s0_s1
schirmer@13688
  1463
      also
schirmer@13688
  1464
      from Ass.hyps
schirmer@13688
  1465
      have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" 
wenzelm@32960
  1466
        by simp
schirmer@13688
  1467
      also
schirmer@13688
  1468
      from ass_ok
schirmer@13688
  1469
      have "\<dots> \<subseteq> dom (locals (store (assign f v s2)))"
wenzelm@32960
  1470
        by (rule dom_locals_assign_mono)
schirmer@13688
  1471
      finally show ?thesis by simp
schirmer@13688
  1472
    next
schirmer@13688
  1473
      case False
wenzelm@23350
  1474
      with `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
schirmer@13688
  1475
      have "s2=s1"
wenzelm@32960
  1476
        by auto
schirmer@13688
  1477
      with s0_s1 False
schirmer@13688
  1478
      have "dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1479
            \<subseteq> dom (locals (store (assign f v s2)))"
wenzelm@32960
  1480
        by simp
schirmer@13688
  1481
      thus ?thesis
wenzelm@32960
  1482
        by simp
schirmer@13688
  1483
    qed
schirmer@13688
  1484
  next
berghofe@21765
  1485
    case (Cond s0 e0 b s1 e1 e2 v s2)
schirmer@13688
  1486
    from Cond.hyps 
schirmer@13688
  1487
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1488
      by simp
schirmer@13688
  1489
    also
schirmer@13688
  1490
    from Cond.hyps
schirmer@13688
  1491
    have "\<dots> \<subseteq> dom (locals (store s2))" 
schirmer@13688
  1492
      by simp
schirmer@13688
  1493
    finally show ?case by simp
schirmer@13688
  1494
  next
berghofe@21765
  1495
    case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
wenzelm@23350
  1496
    note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
schirmer@13688
  1497
    from Call.hyps 
schirmer@13688
  1498
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1499
      by simp
schirmer@13688
  1500
    also
schirmer@13688
  1501
    from Call.hyps
schirmer@13688
  1502
    have "\<dots> \<subseteq> dom (locals (store s2))" 
schirmer@13688
  1503
      by simp
schirmer@13688
  1504
    also
schirmer@13688
  1505
    have "\<dots> \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"
schirmer@13688
  1506
      by (cases s4) simp
schirmer@13688
  1507
    finally show ?case by simp
schirmer@13688
  1508
  next
schirmer@13688
  1509
    case Methd thus ?case by simp
schirmer@13688
  1510
  next
berghofe@21765
  1511
    case (Body s0 D s1 c s2 s3)
schirmer@13688
  1512
    from Body.hyps 
schirmer@13688
  1513
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1514
      by simp
schirmer@13688
  1515
    also
schirmer@13688
  1516
    from Body.hyps
schirmer@13688
  1517
    have "\<dots> \<subseteq> dom (locals (store s2))" 
schirmer@13688
  1518
      by simp
schirmer@13688
  1519
    also
schirmer@13688
  1520
    have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s2)))"
schirmer@13688
  1521
      by simp
schirmer@13688
  1522
    also
schirmer@13688
  1523
    have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
schirmer@13688
  1524
    proof -
wenzelm@23350
  1525
      from `s3 =
schirmer@13688
  1526
         (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
schirmer@13688
  1527
                 abrupt s2 = Some (Jump (Cont l))
wenzelm@23350
  1528
             then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
wenzelm@23350
  1529
      show ?thesis
wenzelm@32960
  1530
        by simp
schirmer@13688
  1531
    qed
schirmer@13688
  1532
    finally show ?case by simp
schirmer@13688
  1533
  next
schirmer@13688
  1534
    case LVar
schirmer@13688
  1535
    thus ?case
schirmer@13688
  1536
      using dom_locals_lvar_mono
schirmer@13688
  1537
      by simp
schirmer@13688
  1538
  next
berghofe@21765
  1539
    case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
schirmer@13688
  1540
    from FVar.hyps
schirmer@13688
  1541
    obtain s2': "s2' = snd (fvar statDeclC stat fn a s2)" and
schirmer@13688
  1542
             v: "v = fst (fvar statDeclC stat fn a s2)"
schirmer@13688
  1543
      by (cases "fvar statDeclC stat fn a s2" ) simp
schirmer@13688
  1544
    from v 
schirmer@13688
  1545
    have "\<forall>s val. dom (locals (store s)) 
schirmer@13688
  1546
                          \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok")
schirmer@13688
  1547
      by (simp add: dom_locals_fvar_vvar_mono) 
schirmer@13688
  1548
    hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s3 \<longrightarrow> ?V_ok)"
schirmer@13688
  1549
      by - (intro strip, simp)
wenzelm@23350
  1550
    note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
schirmer@13688
  1551
    from FVar.hyps 
schirmer@13688
  1552
    have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1553
      by simp
schirmer@13688
  1554
    also
schirmer@13688
  1555
    from FVar.hyps
schirmer@13688
  1556
    have "\<dots> \<subseteq> dom (locals (store s2))" 
schirmer@13688
  1557
      by simp
schirmer@13688