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