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