src/HOL/MicroJava/BV/BVNoTypeError.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14981 e73f8140af78
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
kleing@13633
     1
(*  Title:      HOL/MicroJava/BV/BVNoTypeErrors.thy
kleing@13633
     2
    ID:         $Id$
kleing@13633
     3
    Author:     Gerwin Klein
kleing@13633
     4
*)
kleing@13633
     5
kleing@13633
     6
header {* \isaheader{Welltyped Programs produce no Type Errors} *}
kleing@13633
     7
kleing@13633
     8
theory BVNoTypeError = JVMDefensive + BVSpecTypeSafe:
kleing@13633
     9
kleing@13633
    10
text {*
kleing@13633
    11
  Some simple lemmas about the type testing functions of the
kleing@13633
    12
  defensive JVM:
kleing@13633
    13
*}
kleing@13633
    14
lemma typeof_NoneD [simp,dest]:
kleing@13633
    15
  "typeof (\<lambda>v. None) v = Some x \<Longrightarrow> \<not>isAddr v"
kleing@13633
    16
  by (cases v) auto
kleing@13633
    17
kleing@13633
    18
lemma isRef_def2:
kleing@13633
    19
  "isRef v = (v = Null \<or> (\<exists>loc. v = Addr loc))"
kleing@13633
    20
  by (cases v) (auto simp add: isRef_def)
kleing@13633
    21
kleing@13633
    22
lemma app'Store[simp]:
kleing@13633
    23
  "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST' \<and> idx < length LT)"
kleing@13633
    24
  by (cases ST, auto)
kleing@13633
    25
kleing@13633
    26
lemma app'GetField[simp]:
kleing@13633
    27
  "app' (Getfield F C, G, pc, maxs, rT, (ST,LT)) =  
kleing@13633
    28
  (\<exists>oT vT ST'. ST = oT#ST' \<and> is_class G C \<and>  
kleing@13633
    29
  field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> Class C)"
kleing@13633
    30
  by (cases ST, auto)
kleing@13633
    31
kleing@13633
    32
lemma app'PutField[simp]:
kleing@13633
    33
"app' (Putfield F C, G,  pc, maxs, rT, (ST,LT)) = 
kleing@13633
    34
 (\<exists>vT vT' oT ST'. ST = vT#oT#ST' \<and> is_class G C \<and> 
kleing@13633
    35
  field (G,C) F = Some (C, vT') \<and> 
kleing@13633
    36
  G \<turnstile> oT \<preceq> Class C \<and> G \<turnstile> vT \<preceq> vT')"
kleing@13633
    37
  apply rule
kleing@13633
    38
  defer
kleing@13633
    39
  apply clarsimp
kleing@13633
    40
  apply (cases ST)
kleing@13633
    41
  apply simp
kleing@13633
    42
  apply (cases "tl ST")
kleing@13633
    43
  apply auto
kleing@13633
    44
  done
kleing@13633
    45
kleing@13633
    46
lemma app'Checkcast[simp]:
kleing@13633
    47
"app' (Checkcast C, G, pc, maxs, rT, (ST,LT)) =
kleing@13633
    48
 (\<exists>rT ST'. ST = RefT rT#ST' \<and> is_class G C)"
kleing@13633
    49
apply rule
kleing@13633
    50
defer
kleing@13633
    51
apply clarsimp
kleing@13633
    52
apply (cases ST)
kleing@13633
    53
apply simp
kleing@13633
    54
apply (cases "hd ST")
kleing@13633
    55
defer 
kleing@13633
    56
apply simp
kleing@13633
    57
apply simp
kleing@13633
    58
done
kleing@13633
    59
kleing@13633
    60
kleing@13633
    61
lemma app'Pop[simp]: 
kleing@13633
    62
  "app' (Pop, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST')"
kleing@13633
    63
  by (cases ST, auto)
kleing@13633
    64
kleing@13633
    65
kleing@13633
    66
lemma app'Dup[simp]:
kleing@13633
    67
  "app' (Dup, G, pc, maxs, rT, (ST,LT)) =
kleing@13633
    68
  (\<exists>T ST'. ST = T#ST' \<and> length ST < maxs)"
kleing@13633
    69
  by (cases ST, auto)
kleing@13633
    70
 
kleing@13633
    71
kleing@13633
    72
lemma app'Dup_x1[simp]:
kleing@13633
    73
  "app' (Dup_x1, G, pc, maxs, rT, (ST,LT)) = 
kleing@13633
    74
  (\<exists>T1 T2 ST'. ST = T1#T2#ST' \<and> length ST < maxs)"
kleing@13633
    75
  by (cases ST, simp, cases "tl ST", auto)
kleing@13633
    76
kleing@13633
    77
  
kleing@13633
    78
lemma app'Dup_x2[simp]:
kleing@13633
    79
  "app' (Dup_x2, G, pc, maxs, rT, (ST,LT)) = 
kleing@13633
    80
  (\<exists>T1 T2 T3 ST'. ST = T1#T2#T3#ST' \<and> length ST < maxs)"
kleing@13633
    81
  by (cases ST, simp, cases "tl ST", simp, cases "tl (tl ST)", auto)
kleing@13633
    82
kleing@13633
    83
kleing@13633
    84
lemma app'Swap[simp]:
kleing@13633
    85
  "app' (Swap, G, pc, maxs, rT, (ST,LT)) = (\<exists>T1 T2 ST'. ST = T1#T2#ST')" 
kleing@13633
    86
  by (cases ST, simp, cases "tl ST", auto)
kleing@13633
    87
kleing@13633
    88
  
kleing@13633
    89
lemma app'IAdd[simp]:
kleing@13633
    90
  "app' (IAdd, G, pc, maxs, rT, (ST,LT)) = 
kleing@13633
    91
  (\<exists>ST'. ST = PrimT Integer#PrimT Integer#ST')"
kleing@13633
    92
  apply (cases ST)
kleing@13633
    93
  apply simp
kleing@13633
    94
  apply simp
kleing@13633
    95
  apply (case_tac a)
kleing@13633
    96
  apply auto
kleing@13633
    97
  apply (case_tac prim_ty)
kleing@13633
    98
  apply auto
kleing@13633
    99
  apply (case_tac prim_ty)
kleing@13633
   100
  apply auto
kleing@13633
   101
  apply (case_tac list)
kleing@13633
   102
  apply auto
kleing@13633
   103
  apply (case_tac a)
kleing@13633
   104
  apply auto
kleing@13633
   105
  apply (case_tac prim_ty)
kleing@13633
   106
  apply auto
kleing@13633
   107
  done
kleing@13633
   108
 
kleing@13633
   109
kleing@13633
   110
lemma app'Ifcmpeq[simp]:
kleing@13633
   111
  "app' (Ifcmpeq b, G, pc, maxs, rT, (ST,LT)) =
kleing@13633
   112
  (\<exists>T1 T2 ST'. ST = T1#T2#ST' \<and> 0 \<le> b + int pc \<and> 
kleing@13633
   113
  ((\<exists>p. T1 = PrimT p \<and> T1 = T2) \<or> 
kleing@13633
   114
  (\<exists>r r'. T1 = RefT r \<and> T2 = RefT r')))" 
kleing@13633
   115
  apply auto
kleing@13633
   116
  apply (cases ST)
kleing@13633
   117
  apply simp
kleing@13633
   118
  apply (cases "tl ST")
kleing@13633
   119
  apply (case_tac a)
kleing@13633
   120
  apply auto
kleing@13633
   121
  done
kleing@13633
   122
  
kleing@13633
   123
kleing@13633
   124
lemma app'Return[simp]:
kleing@13633
   125
  "app' (Return, G, pc, maxs, rT, (ST,LT)) = 
kleing@13633
   126
  (\<exists>T ST'. ST = T#ST'\<and> G \<turnstile> T \<preceq> rT)" 
kleing@13633
   127
  by (cases ST, auto)
kleing@13633
   128
kleing@13633
   129
kleing@13633
   130
lemma app'Throw[simp]:
kleing@13633
   131
  "app' (Throw, G, pc, maxs, rT, (ST,LT)) = 
kleing@13633
   132
  (\<exists>ST' r. ST = RefT r#ST')"
kleing@13633
   133
  apply (cases ST, simp)
kleing@13633
   134
  apply (cases "hd ST")
kleing@13633
   135
  apply auto
kleing@13633
   136
  done
kleing@13633
   137
kleing@13633
   138
  
kleing@13633
   139
lemma app'Invoke[simp]:
kleing@13633
   140
"app' (Invoke C mn fpTs, G, pc, maxs, rT, ST, LT) = 
kleing@13633
   141
 (\<exists>apTs X ST' mD' rT' b'.
kleing@13633
   142
  ST = (rev apTs) @ X # ST' \<and> 
kleing@13633
   143
  length apTs = length fpTs \<and> is_class G C \<and>
kleing@13633
   144
  (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> 
kleing@13633
   145
  method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
kleing@13633
   146
  (is "?app ST LT = ?P ST LT")
kleing@13633
   147
proof
kleing@13633
   148
  assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def)
kleing@13633
   149
next  
kleing@13633
   150
  assume app: "?app ST LT"
kleing@13633
   151
  hence l: "length fpTs < length ST" by simp
kleing@13633
   152
  obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs"
kleing@13633
   153
  proof -
kleing@13633
   154
    have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
kleing@13633
   155
    moreover from l have "length (take (length fpTs) ST) = length fpTs"
kleing@13633
   156
      by (simp add: min_def)
kleing@13633
   157
    ultimately show ?thesis ..
kleing@13633
   158
  qed
kleing@13633
   159
  obtain apTs where
kleing@13633
   160
    "ST = (rev apTs) @ ys" and "length apTs = length fpTs"
kleing@13633
   161
  proof -
kleing@13633
   162
    have "ST = rev (rev xs) @ ys" by simp
kleing@13633
   163
    with xs show ?thesis by - (rule that, assumption, simp)
kleing@13633
   164
  qed
kleing@13633
   165
  moreover
kleing@13633
   166
  from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
kleing@13633
   167
  ultimately
kleing@13633
   168
  have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
kleing@13633
   169
  with app
kleing@13633
   170
  show "?P ST LT"
kleing@13633
   171
    apply (clarsimp simp add: list_all2_def min_def)
kleing@13633
   172
    apply ((rule exI)+, (rule conjI)?)+
kleing@13633
   173
    apply auto
kleing@13633
   174
    done
kleing@13633
   175
qed 
kleing@13633
   176
kleing@13633
   177
lemma approx_loc_len [simp]:
kleing@13633
   178
  "approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
kleing@13633
   179
  by (simp add: approx_loc_def list_all2_def)
kleing@13633
   180
kleing@13633
   181
lemma approx_stk_len [simp]:
kleing@13633
   182
  "approx_stk G hp stk ST \<Longrightarrow> length stk = length ST"
kleing@13633
   183
  by (simp add: approx_stk_def)
kleing@13633
   184
kleing@13633
   185
lemma isRefI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> RefT T \<Longrightarrow> isRef v"
kleing@13633
   186
  apply (drule conf_RefTD)
kleing@13633
   187
  apply (auto simp add: isRef_def)
kleing@13633
   188
  done
kleing@13633
   189
kleing@13633
   190
lemma isIntgI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> PrimT Integer \<Longrightarrow> isIntg v"
kleing@13633
   191
  apply (unfold conf_def)
kleing@13633
   192
  apply auto
kleing@13633
   193
  apply (erule widen.elims)
kleing@13633
   194
  apply auto
kleing@13633
   195
  apply (cases v)
kleing@13633
   196
  apply auto
kleing@13633
   197
  done
kleing@13633
   198
kleing@13633
   199
lemma list_all2_approx:
kleing@13633
   200
  "\<And>s. list_all2 (approx_val G hp) s (map OK S) = 
kleing@13633
   201
       list_all2 (conf G hp) s S"
kleing@13633
   202
  apply (induct S)
kleing@13633
   203
  apply (auto simp add: list_all2_Cons2 approx_val_def)
kleing@13633
   204
  done
kleing@13633
   205
kleing@13633
   206
lemma list_all2_conf_widen:
kleing@13633
   207
  "wf_prog mb G \<Longrightarrow>
kleing@13633
   208
  list_all2 (conf G hp) a b \<Longrightarrow>
kleing@13633
   209
  list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) b c \<Longrightarrow>
kleing@13633
   210
  list_all2 (conf G hp) a c"
kleing@13633
   211
  apply (rule list_all2_trans)
kleing@13633
   212
  defer
kleing@13633
   213
  apply assumption
kleing@13633
   214
  apply assumption
kleing@13633
   215
  apply (drule conf_widen, assumption+)
kleing@13633
   216
  done
kleing@13633
   217
kleing@13633
   218
kleing@13633
   219
text {*
kleing@13633
   220
  The main theorem: welltyped programs do not produce type errors if they
kleing@13633
   221
  are started in a conformant state.
kleing@13633
   222
*}
kleing@13633
   223
theorem no_type_error:
kleing@13633
   224
  assumes welltyped: "wt_jvm_prog G Phi" and conforms: "G,Phi \<turnstile>JVM s \<surd>"
kleing@13633
   225
  shows "exec_d G (Normal s) \<noteq> TypeError"
kleing@13633
   226
proof -
kleing@13633
   227
  from welltyped obtain mb where wf: "wf_prog mb G" by (fast dest: wt_jvm_progD)
kleing@13633
   228
  
kleing@13633
   229
  obtain xcp hp frs where s [simp]: "s = (xcp, hp, frs)" by (cases s)
kleing@13633
   230
kleing@13633
   231
  from conforms have "xcp \<noteq> None \<or> frs = [] \<Longrightarrow> check G s" 
kleing@13633
   232
    by (unfold correct_state_def check_def) auto
kleing@13633
   233
  moreover {
kleing@13633
   234
    assume "\<not>(xcp \<noteq> None \<or> frs = [])"
kleing@13633
   235
    then obtain stk loc C sig pc frs' where
kleing@13633
   236
      xcp [simp]: "xcp = None" and
kleing@13633
   237
      frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" 
kleing@13633
   238
      by (clarsimp simp add: neq_Nil_conv) fast
kleing@13633
   239
kleing@13633
   240
    from conforms obtain  ST LT rT maxs maxl ins et where
kleing@13633
   241
      hconf:  "G \<turnstile>h hp \<surd>" and
kleing@13633
   242
      class:  "is_class G C" and
kleing@13633
   243
      meth:   "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
kleing@13633
   244
      phi:    "Phi C sig ! pc = Some (ST,LT)" and
kleing@13633
   245
      frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
kleing@13633
   246
      frames: "correct_frames G hp Phi rT sig frs'"
kleing@13633
   247
      by (auto simp add: correct_state_def)
kleing@13633
   248
kleing@13633
   249
    from frame obtain
kleing@13633
   250
      stk: "approx_stk G hp stk ST" and
kleing@13633
   251
      loc: "approx_loc G hp loc LT" and
kleing@13633
   252
      pc:  "pc < length ins" and
kleing@13633
   253
      len: "length loc = length (snd sig) + maxl + 1"
kleing@13633
   254
      by (auto simp add: correct_frame_def)
kleing@13633
   255
kleing@13633
   256
    note approx_val_def [simp]
kleing@13633
   257
kleing@13633
   258
    from welltyped meth conforms
kleing@13633
   259
    have "wt_instr (ins!pc) G rT (Phi C sig) maxs (length ins) et pc"
kleing@13633
   260
      by simp (rule wt_jvm_prog_impl_wt_instr_cor)    
kleing@13633
   261
    then obtain
kleing@13633
   262
      app': "app (ins!pc) G maxs rT pc et (Phi C sig!pc) " and
kleing@13633
   263
      eff: "\<forall>(pc', s')\<in>set (eff (ins ! pc) G pc et (Phi C sig ! pc)). pc' < length ins"
kleing@13633
   264
      by (simp add: wt_instr_def phi) blast
kleing@13633
   265
kleing@13633
   266
    from eff 
kleing@13633
   267
    have pc': "\<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins"
kleing@13633
   268
      by (simp add: eff_def) blast
kleing@13633
   269
kleing@13633
   270
    from app' phi
kleing@13633
   271
    have app:
kleing@13633
   272
      "xcpt_app (ins!pc) G pc et \<and> app' (ins!pc, G, pc, maxs, rT, (ST,LT))"
kleing@13633
   273
      by (clarsimp simp add: app_def)
kleing@13633
   274
kleing@13633
   275
    with eff stk loc pc'
kleing@13822
   276
    have "check_instr (ins!pc) G hp stk loc C sig pc maxs frs'"
kleing@13633
   277
    proof (cases "ins!pc")
kleing@13633
   278
      case (Getfield F C) 
kleing@13633
   279
      with app stk loc phi obtain v vT stk' where
kleing@13633
   280
        class: "is_class G C" and
kleing@13633
   281
        field: "field (G, C) F = Some (C, vT)" and
kleing@13633
   282
        stk:   "stk = v # stk'" and
kleing@13633
   283
        conf:  "G,hp \<turnstile> v ::\<preceq> Class C"
kleing@13633
   284
        apply clarsimp
kleing@13633
   285
        apply (blast dest: conf_widen [OF wf])
kleing@13633
   286
        done
kleing@13633
   287
      from conf have isRef: "isRef v" ..
kleing@13633
   288
      moreover {
kleing@13633
   289
        assume "v \<noteq> Null" 
kleing@13633
   290
        with conf field isRef wf
kleing@13633
   291
        have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C" 
kleing@13633
   292
          by (auto dest!: non_np_objD)
kleing@13633
   293
      }
streckem@14045
   294
      ultimately show ?thesis using Getfield field class stk hconf wf
kleing@13633
   295
        apply clarsimp
streckem@14045
   296
        apply (fastsimp intro: wf_prog_ws_prog
streckem@14045
   297
	  dest!: hconfD widen_cfs_fields oconf_objD)
kleing@13633
   298
        done
kleing@13633
   299
    next
kleing@13633
   300
      case (Putfield F C)
kleing@13633
   301
      with app stk loc phi obtain v ref vT stk' where
kleing@13633
   302
        class: "is_class G C" and
kleing@13633
   303
        field: "field (G, C) F = Some (C, vT)" and
kleing@13633
   304
        stk:   "stk = v # ref # stk'" and
kleing@13633
   305
        confv: "G,hp \<turnstile> v ::\<preceq> vT" and
kleing@13633
   306
        confr: "G,hp \<turnstile> ref ::\<preceq> Class C"
kleing@13633
   307
        apply clarsimp
kleing@13633
   308
        apply (blast dest: conf_widen [OF wf])
kleing@13633
   309
        done
kleing@13633
   310
      from confr have isRef: "isRef ref" ..
kleing@13633
   311
      moreover {
kleing@13633
   312
        assume "ref \<noteq> Null" 
kleing@13633
   313
        with confr field isRef wf
kleing@13633
   314
        have "\<exists>D vs. hp (the_Addr ref) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
kleing@13633
   315
          by (auto dest: non_np_objD)
kleing@13633
   316
      }
kleing@13633
   317
      ultimately show ?thesis using Putfield field class stk confv
kleing@13633
   318
        by clarsimp
kleing@13633
   319
    next      
kleing@13633
   320
      case (Invoke C mn ps)
kleing@13633
   321
      with app
kleing@13633
   322
      obtain apTs X ST' where
kleing@13633
   323
        ST: "ST = rev apTs @ X # ST'" and
kleing@13633
   324
        ps: "length apTs = length ps" and
kleing@13633
   325
        w:   "\<forall>x\<in>set (zip apTs ps). x \<in> widen G" and
kleing@13633
   326
        C:   "G \<turnstile> X \<preceq> Class C" and
kleing@13633
   327
        mth: "method (G, C) (mn, ps) \<noteq> None"
kleing@13633
   328
        by (simp del: app'.simps) blast
kleing@13633
   329
        
kleing@13633
   330
      from ST stk
kleing@13633
   331
      obtain aps x stk' where
kleing@13633
   332
        stk': "stk = aps @ x # stk'" and
kleing@13633
   333
        aps: "approx_stk G hp aps (rev apTs)" and
kleing@13633
   334
        x: "G,hp \<turnstile> x ::\<preceq> X" and        
kleing@13633
   335
        l: "length aps = length apTs"
kleing@13633
   336
        by (auto dest!: approx_stk_append)
kleing@13633
   337
      
kleing@13633
   338
      from stk' l ps 
kleing@13633
   339
      have [simp]: "stk!length ps = x" by (simp add: nth_append)
kleing@13633
   340
      from stk' l ps
kleing@13633
   341
      have [simp]: "take (length ps) stk = aps" by simp
kleing@13633
   342
      from w ps
kleing@13633
   343
      have widen: "list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs ps"
kleing@13633
   344
        by (simp add: list_all2_def) 
kleing@13633
   345
kleing@13633
   346
      from stk' l ps have "length ps < length stk" by simp
kleing@13633
   347
      moreover
kleing@13633
   348
      from wf x C 
kleing@13633
   349
      have x: "G,hp \<turnstile> x ::\<preceq> Class C" by (rule conf_widen) 
kleing@13633
   350
      hence "isRef x" by simp
kleing@13633
   351
      moreover
kleing@13633
   352
      { assume "x \<noteq> Null"
kleing@13633
   353
        with x
kleing@13633
   354
        obtain D fs where
kleing@13633
   355
          hp: "hp (the_Addr x) = Some (D,fs)" and
kleing@13633
   356
          D:  "G \<turnstile> D \<preceq>C C"
kleing@13633
   357
          by - (drule non_npD, assumption, clarsimp, blast)
kleing@13633
   358
        hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
kleing@13633
   359
        moreover
kleing@13633
   360
        from wf mth hp D
kleing@13633
   361
        have "method (G, cname_of hp x) (mn, ps) \<noteq> None" (is ?P2)
kleing@13633
   362
          by (auto dest: subcls_widen_methd)
kleing@13633
   363
        moreover
kleing@13633
   364
        from aps have "list_all2 (conf G hp) aps (rev apTs)"
kleing@13633
   365
          by (simp add: list_all2_approx approx_stk_def approx_loc_def)        
kleing@13633
   366
        hence "list_all2 (conf G hp) (rev aps) (rev (rev apTs))"
kleing@13633
   367
          by (simp only: list_all2_rev)
kleing@13633
   368
        hence "list_all2 (conf G hp) (rev aps) apTs" by simp
kleing@13633
   369
        with wf widen        
kleing@13633
   370
        have "list_all2 (conf G hp) (rev aps) ps" (is ?P3)
kleing@13633
   371
          by - (rule list_all2_conf_widen) 
kleing@13633
   372
        ultimately
kleing@13633
   373
        have "?P1 \<and> ?P2 \<and> ?P3" by blast
kleing@13633
   374
      }
kleing@13633
   375
      moreover 
kleing@13633
   376
      note Invoke
kleing@13633
   377
      ultimately
kleing@13633
   378
      show ?thesis by simp
kleing@13633
   379
    next
kleing@13633
   380
      case Return with stk app phi meth frames 
kleing@13633
   381
      show ?thesis        
kleing@13633
   382
        apply clarsimp
kleing@13633
   383
        apply (drule conf_widen [OF wf], assumption)
kleing@13633
   384
        apply (clarsimp simp add: neq_Nil_conv isRef_def2)
kleing@13633
   385
        done
kleing@13633
   386
    qed auto
kleing@13822
   387
    hence "check G s" by (simp add: check_def meth pc)
kleing@13633
   388
  } ultimately
kleing@13633
   389
  have "check G s" by blast
kleing@13633
   390
  thus "exec_d G (Normal s) \<noteq> TypeError" ..
kleing@13633
   391
qed
kleing@13633
   392
kleing@13633
   393
kleing@13633
   394
text {*
kleing@13633
   395
  The theorem above tells us that, in welltyped programs, the
kleing@13633
   396
  defensive machine reaches the same result as the aggressive
kleing@13633
   397
  one (after arbitrarily many steps).
kleing@13633
   398
*}
kleing@13633
   399
theorem welltyped_aggressive_imp_defensive:
kleing@13633
   400
  "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t 
kleing@13633
   401
  \<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)"
kleing@13633
   402
  apply (unfold exec_all_def) 
kleing@13633
   403
  apply (erule rtrancl_induct)
kleing@13633
   404
   apply (simp add: exec_all_d_def)
kleing@13633
   405
  apply simp
kleing@13633
   406
  apply (fold exec_all_def)
kleing@13633
   407
  apply (frule BV_correct, assumption+)
kleing@13633
   408
  apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
kleing@13633
   409
  apply (simp add: exec_all_d_def)
kleing@13633
   410
  apply (rule rtrancl_trans, assumption)
kleing@13633
   411
  apply blast
kleing@13633
   412
  done
kleing@13633
   413
kleing@13633
   414
kleing@13822
   415
lemma neq_TypeError_eq [simp]: "s \<noteq> TypeError = (\<exists>s'. s = Normal s')"
kleing@13822
   416
  by (cases s, auto)
kleing@13822
   417
kleing@13822
   418
theorem no_type_errors:
kleing@13822
   419
  "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd>
kleing@13822
   420
  \<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> t \<Longrightarrow> t \<noteq> TypeError"
kleing@13822
   421
  apply (unfold exec_all_d_def)   
kleing@13822
   422
  apply (erule rtrancl_induct)
kleing@13822
   423
   apply simp
kleing@13822
   424
  apply (fold exec_all_d_def)
kleing@13822
   425
  apply (auto dest: defensive_imp_aggressive BV_correct no_type_error)
kleing@13822
   426
  done
kleing@13822
   427
kleing@13822
   428
corollary no_type_errors_initial:
kleing@13822
   429
  fixes G ("\<Gamma>") and Phi ("\<Phi>")
kleing@13822
   430
  assumes "wt_jvm_prog \<Gamma> \<Phi>"  
kleing@13822
   431
  assumes "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
kleing@13822
   432
  defines start: "s \<equiv> start_state \<Gamma> C m"
kleing@13822
   433
kleing@13822
   434
  assumes "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> t" 
kleing@13822
   435
  shows "t \<noteq> TypeError"
kleing@13822
   436
proof -
kleing@13822
   437
  have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
kleing@13822
   438
  thus ?thesis by - (rule no_type_errors)
kleing@13822
   439
qed
kleing@13822
   440
kleing@13633
   441
text {*
kleing@13633
   442
  As corollary we get that the aggressive and the defensive machine
kleing@13633
   443
  are equivalent for welltyped programs (if started in a conformant
kleing@13633
   444
  state or in the canonical start state)
kleing@13633
   445
*} 
kleing@13633
   446
corollary welltyped_commutes:
kleing@13633
   447
  fixes G ("\<Gamma>") and Phi ("\<Phi>")
kleing@13633
   448
  assumes "wt_jvm_prog \<Gamma> \<Phi>" and "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" 
kleing@13633
   449
  shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
kleing@13633
   450
  by rule (erule defensive_imp_aggressive,rule welltyped_aggressive_imp_defensive)
kleing@13633
   451
kleing@13633
   452
kleing@13633
   453
corollary welltyped_initial_commutes:
kleing@13633
   454
  fixes G ("\<Gamma>") and Phi ("\<Phi>")
kleing@13633
   455
  assumes "wt_jvm_prog \<Gamma> \<Phi>"  
kleing@13633
   456
  assumes "is_class \<Gamma> C" "method (\<Gamma>,C) (m,[]) = Some (C, b)" "m \<noteq> init"
kleing@13633
   457
  defines start: "s \<equiv> start_state \<Gamma> C m"
kleing@13633
   458
  shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
kleing@13633
   459
proof -
kleing@13633
   460
  have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>" by (unfold start, rule BV_correct_initial)
kleing@13633
   461
  thus ?thesis by  - (rule welltyped_commutes)
kleing@13633
   462
qed
kleing@13633
   463
 
kleing@13633
   464
end