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