src/HOL/MicroJava/J/JTypeSafe.thy
author streckem
Fri Aug 08 14:57:46 2003 +0200 (2003-08-08)
changeset 14142 0b04f6587e67
parent 14045 a34d89ce6097
child 16417 9bc16273c2d4
permissions -rw-r--r--
Changed lemmas .._type_sound
nipkow@8011
     1
(*  Title:      HOL/MicroJava/J/JTypeSafe.thy
nipkow@8011
     2
    ID:         $Id$
nipkow@8011
     3
    Author:     David von Oheimb
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
oheimb@11070
     5
*)
nipkow@8011
     6
kleing@12911
     7
header {* \isaheader{Type Safety Proof} *}
nipkow@8011
     8
oheimb@11026
     9
theory JTypeSafe = Eval + Conform:
oheimb@11026
    10
oheimb@11026
    11
declare split_beta [simp]
oheimb@11026
    12
oheimb@11026
    13
lemma NewC_conforms: 
streckem@13672
    14
"[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>  
streckem@13672
    15
  (x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)"
oheimb@11026
    16
apply( erule conforms_upd_obj)
oheimb@11026
    17
apply(  unfold oconf_def)
streckem@14045
    18
apply(  auto dest!: fields_is_type simp add: wf_prog_ws_prog)
oheimb@11026
    19
done
streckem@14045
    20
streckem@14045
    21
oheimb@11026
    22
lemma Cast_conf: 
streckem@14045
    23
 "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>CC; G\<turnstile>CC \<preceq>? Class D; cast_ok G D h v|]  
streckem@14045
    24
  ==> G,h\<turnstile>v::\<preceq>Class D"
streckem@14045
    25
apply (case_tac "CC")
streckem@14045
    26
apply simp
streckem@14045
    27
apply (case_tac "ref_ty")
streckem@14045
    28
apply (clarsimp simp add: conf_def)
streckem@14045
    29
apply simp
streckem@14045
    30
apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D", simp) 
streckem@14045
    31
apply (rule conf_widen, assumption+) apply (erule widen.subcls)
streckem@14045
    32
oheimb@11026
    33
apply (unfold cast_ok_def)
oheimb@11026
    34
apply( case_tac "v = Null")
oheimb@11026
    35
apply(  simp)
oheimb@11026
    36
apply(  clarify)
oheimb@11026
    37
apply( drule (1) non_npD)
oheimb@11026
    38
apply( auto intro!: conf_AddrI simp add: obj_ty_def)
oheimb@11026
    39
done
oheimb@11026
    40
streckem@13672
    41
oheimb@11026
    42
lemma FAcc_type_sound: 
streckem@13672
    43
"[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT);  
oheimb@11026
    44
  x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==>  
oheimb@11026
    45
  G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft"
oheimb@11026
    46
apply( drule np_NoneD)
oheimb@11026
    47
apply( erule conjE)
oheimb@11026
    48
apply( erule (1) notE impE)
oheimb@11026
    49
apply( drule non_np_objD)
oheimb@11026
    50
apply   auto
oheimb@11026
    51
apply( drule conforms_heapD [THEN hconfD])
oheimb@11026
    52
apply(  assumption)
streckem@14045
    53
apply (frule wf_prog_ws_prog)
oheimb@11026
    54
apply( drule (2) widen_cfs_fields)
oheimb@11026
    55
apply( drule (1) oconf_objD)
oheimb@11026
    56
apply auto
oheimb@11026
    57
done
oheimb@11026
    58
oheimb@11026
    59
lemma FAss_type_sound: 
oheimb@11026
    60
 "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a);  
oheimb@11026
    61
    (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft;  
oheimb@11026
    62
    (G, lT)\<turnstile>aa::Class C;  
oheimb@11026
    63
    field (G,C) fn = Some (fd, ft); h''\<le>|h';  
oheimb@11026
    64
    x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h;  
streckem@13672
    65
    Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>  
oheimb@11026
    66
  h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and>   
streckem@13672
    67
  Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>   
oheimb@11026
    68
  G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'"
oheimb@11026
    69
apply( drule np_NoneD)
oheimb@11026
    70
apply( erule conjE)
oheimb@11026
    71
apply( simp)
oheimb@11026
    72
apply( drule non_np_objD)
kleing@12951
    73
apply(  assumption)
oheimb@11026
    74
apply( clarify)
oheimb@11026
    75
apply( simp (no_asm_use))
oheimb@11026
    76
apply( frule (1) hext_objD)
oheimb@11026
    77
apply( erule exE)
oheimb@11026
    78
apply( simp)
oheimb@11026
    79
apply( clarify)
oheimb@11026
    80
apply( rule conjI)
oheimb@11026
    81
apply(  fast elim: hext_trans hext_upd_obj)
oheimb@11026
    82
apply( rule conjI)
oheimb@11026
    83
prefer 2
oheimb@11026
    84
apply(  fast elim: conf_upd_obj [THEN iffD2])
oheimb@11026
    85
oheimb@11026
    86
apply( rule conforms_upd_obj)
oheimb@11026
    87
apply   auto
oheimb@11026
    88
apply(  rule_tac [2] hextI)
oheimb@11026
    89
prefer 2
oheimb@11026
    90
apply(  force)
oheimb@11026
    91
apply( rule oconf_hext)
oheimb@11026
    92
apply(  erule_tac [2] hext_upd_obj)
streckem@14045
    93
apply (frule wf_prog_ws_prog)
oheimb@11026
    94
apply( drule (2) widen_cfs_fields)
oheimb@11026
    95
apply( rule oconf_obj [THEN iffD2])
oheimb@11026
    96
apply( simp (no_asm))
oheimb@11026
    97
apply( intro strip)
oheimb@11026
    98
apply( case_tac "(aaa, b) = (fn, fd)")
oheimb@11026
    99
apply(  simp)
oheimb@11026
   100
apply(  fast intro: conf_widen)
oheimb@11026
   101
apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
oheimb@11026
   102
done
oheimb@11026
   103
streckem@13672
   104
streckem@13672
   105
oheimb@11026
   106
lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;  
oheimb@11026
   107
   list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;  
nipkow@12888
   108
  length pTs' = length pns; distinct pns;  
oheimb@11026
   109
  Ball (set lvars) (split (\<lambda>vn. is_type G))  
oheimb@11026
   110
  |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
oheimb@11026
   111
apply (unfold wf_mhead_def)
oheimb@11026
   112
apply( clarsimp)
oheimb@11026
   113
apply( rule lconf_ext_list)
oheimb@11026
   114
apply(    rule Ball_set_table [THEN lconf_init_vars])
oheimb@11026
   115
apply(    force)
oheimb@11026
   116
apply(   assumption)
oheimb@11026
   117
apply(  assumption)
oheimb@11026
   118
apply( erule (2) conf_list_gext_widen)
oheimb@11026
   119
done
oheimb@11026
   120
oheimb@11026
   121
lemma Call_type_sound: 
streckem@13672
   122
 "[| wf_java_prog G; a' \<noteq> Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y;  
oheimb@11026
   123
     max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h;  
oheimb@11026
   124
     list_all2 (conf G h) pvs pTsa; 
oheimb@11026
   125
     (md, rT, pns, lvars, blk, res) =  
oheimb@11026
   126
               the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); 
streckem@13672
   127
  \<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->  
streckem@13672
   128
  (G, lT)\<turnstile>blk\<surd> -->  h\<le>|xi \<and>  (xcptb, xi, xl)::\<preceq>(G, lT);  
streckem@13672
   129
  \<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->  
streckem@13672
   130
          xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));  
streckem@13672
   131
  G,xh\<turnstile>a'::\<preceq> Class C
streckem@13672
   132
  |] ==>  
streckem@13672
   133
  xc\<le>|h' \<and> (x',(h', l))::\<preceq>(G, lT) \<and>  (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
oheimb@11026
   134
apply( drule max_spec2mheads)
oheimb@11026
   135
apply( clarify)
oheimb@11026
   136
apply( drule (2) non_np_objD')
oheimb@11026
   137
apply( clarsimp)
oheimb@11026
   138
apply( frule (1) hext_objD)
oheimb@11026
   139
apply( clarsimp)
oheimb@11026
   140
apply( drule (3) Call_lemma)
oheimb@11026
   141
apply( clarsimp simp add: wf_java_mdecl_def)
oheimb@11026
   142
apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
streckem@13672
   143
apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac 2")
oheimb@11026
   144
apply(  rule conformsI)
oheimb@11026
   145
apply(   erule conforms_heapD)
oheimb@11026
   146
apply(  rule lconf_ext)
oheimb@11026
   147
apply(   force elim!: Call_lemma2)
oheimb@11026
   148
apply(  erule conf_hext, erule (1) conf_obj_AddrI)
streckem@13672
   149
apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) 
streckem@13672
   150
apply (simp add: conforms_def)
streckem@13672
   151
oheimb@11026
   152
apply( erule conjE)
oheimb@11026
   153
apply( drule spec, erule (1) impE)
oheimb@11026
   154
apply( drule spec, erule (1) impE)
oheimb@11026
   155
apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
oheimb@11026
   156
apply( clarify)
oheimb@11026
   157
apply( rule conjI)
oheimb@11026
   158
apply(  fast intro: hext_trans)
oheimb@11026
   159
apply( rule conjI)
oheimb@11026
   160
apply(  rule_tac [2] impI)
oheimb@11026
   161
apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
oheimb@11026
   162
apply(  frule_tac [2] conf_widen)
oheimb@11026
   163
apply(    tactic "assume_tac 4")
oheimb@11026
   164
apply(   tactic "assume_tac 2")
oheimb@11026
   165
prefer 2
oheimb@11026
   166
apply(  fast elim!: widen_trans)
streckem@13672
   167
apply (rule conforms_xcpt_change)
streckem@13672
   168
apply( rule conforms_hext) apply assumption
oheimb@11026
   169
apply(  erule (1) hext_trans)
oheimb@11026
   170
apply( erule conforms_heapD)
streckem@13672
   171
apply (simp add: conforms_def)
oheimb@11026
   172
done
oheimb@11026
   173
streckem@13672
   174
streckem@13672
   175
oheimb@11026
   176
declare split_if [split del]
oheimb@11026
   177
declare fun_upd_apply [simp del]
oheimb@11026
   178
declare fun_upd_same [simp]
streckem@14045
   179
declare wf_prog_ws_prog [simp]
streckem@14045
   180
oheimb@11026
   181
ML{*
oheimb@11026
   182
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
kleing@12517
   183
  (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
oheimb@11026
   184
*}
oheimb@11026
   185
ML{*
oheimb@11026
   186
Unify.search_bound := 40;
oheimb@11026
   187
Unify.trace_bound  := 40
oheimb@11026
   188
*}
streckem@13672
   189
streckem@13672
   190
oheimb@11026
   191
theorem eval_evals_exec_type_sound: 
oheimb@11026
   192
"wf_java_prog G ==>  
oheimb@11026
   193
  (G\<turnstile>(x,(h,l)) -e  \<succ>v  -> (x', (h',l')) -->  
streckem@13672
   194
      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e  :: T -->  
streckem@13672
   195
      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v  ::\<preceq> T )))) \<and>  
oheimb@11026
   196
  (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->  
streckem@13672
   197
      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->  
streckem@13672
   198
      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>  
oheimb@11026
   199
  (G\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) -->  
streckem@13672
   200
      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) -->       (G,lT)\<turnstile>c  \<surd> -->  
streckem@13672
   201
      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT)))"
oheimb@11026
   202
apply( rule eval_evals_exec_induct)
oheimb@11026
   203
apply( unfold c_hupd_def)
oheimb@11026
   204
kleing@12517
   205
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
oheimb@11026
   206
apply( simp_all)
oheimb@11026
   207
apply( tactic "ALLGOALS strip_tac")
kleing@12517
   208
apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
kleing@12517
   209
                 THEN_ALL_NEW Full_simp_tac) *})
kleing@12517
   210
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
oheimb@11026
   211
kleing@12517
   212
-- "Level 7"
kleing@12517
   213
-- "15 NewC"
streckem@13672
   214
apply (drule sym)
oheimb@11026
   215
apply( drule new_AddrD)
oheimb@11026
   216
apply( erule disjE)
oheimb@11026
   217
prefer 2
oheimb@11026
   218
apply(  simp (no_asm_simp))
streckem@13672
   219
apply (rule conforms_xcpt_change, assumption) 
streckem@13672
   220
apply (simp (no_asm_simp) add: xconf_def)
oheimb@11026
   221
apply( clarsimp)
oheimb@11026
   222
apply( rule conjI)
oheimb@11026
   223
apply(  force elim!: NewC_conforms)
oheimb@11026
   224
apply( rule conf_obj_AddrI)
oheimb@11026
   225
apply(  rule_tac [2] rtrancl_refl)
oheimb@11026
   226
apply( simp (no_asm))
oheimb@11026
   227
kleing@12517
   228
-- "for Cast"
oheimb@11026
   229
defer 1
oheimb@11026
   230
kleing@12517
   231
-- "14 Lit"
oheimb@11026
   232
apply( erule conf_litval)
oheimb@11026
   233
kleing@12517
   234
-- "13 BinOp"
oheimb@11026
   235
apply (tactic "forward_hyp_tac")
oheimb@11026
   236
apply (tactic "forward_hyp_tac")
oheimb@11026
   237
apply( rule conjI, erule (1) hext_trans)
oheimb@11026
   238
apply( erule conjI)
oheimb@11026
   239
apply( clarsimp)
oheimb@11026
   240
apply( drule eval_no_xcpt)
oheimb@11026
   241
apply( simp split add: binop.split)
oheimb@11026
   242
kleing@12517
   243
-- "12 LAcc"
streckem@13672
   244
apply simp
oheimb@11026
   245
apply( fast elim: conforms_localD [THEN lconfD])
oheimb@11026
   246
kleing@12517
   247
-- "for FAss"
kleing@12517
   248
apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
kleing@12517
   249
       THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
oheimb@11026
   250
kleing@12517
   251
-- "for if"
oheimb@11026
   252
apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
oheimb@11026
   253
oheimb@11026
   254
apply (tactic "forward_hyp_tac")
oheimb@11026
   255
kleing@12517
   256
-- "11+1 if"
oheimb@11026
   257
prefer 8
oheimb@11026
   258
apply(  fast intro: hext_trans)
oheimb@11026
   259
prefer 8
oheimb@11026
   260
apply(  fast intro: hext_trans)
oheimb@11026
   261
kleing@12517
   262
-- "10 Expr"
streckem@13672
   263
prefer 7
oheimb@11026
   264
apply( fast)
oheimb@11026
   265
kleing@12517
   266
-- "9 ???"
oheimb@11026
   267
apply( simp_all)
oheimb@11026
   268
kleing@12517
   269
-- "8 Cast"
oheimb@11026
   270
prefer 8
streckem@13672
   271
apply (rule conjI)
streckem@13672
   272
  apply (fast intro: conforms_xcpt_change xconf_raise_if)
streckem@13672
   273
streckem@13672
   274
  apply clarify
streckem@13672
   275
  apply (drule raise_if_NoneD)
streckem@13672
   276
  apply (clarsimp)
streckem@13672
   277
  apply (rule Cast_conf)
streckem@13672
   278
  apply assumption+
oheimb@11026
   279
streckem@14045
   280
kleing@12517
   281
-- "7 LAss"
oheimb@11026
   282
apply (fold fun_upd_def)
kleing@12517
   283
apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
kleing@12517
   284
                 THEN_ALL_NEW Full_simp_tac) 1 *})
streckem@13672
   285
apply (intro strip)
streckem@13672
   286
apply (case_tac E)
streckem@13672
   287
apply (simp)
oheimb@11026
   288
apply( blast intro: conforms_upd_local conf_widen)
oheimb@11026
   289
kleing@12517
   290
-- "6 FAcc"
streckem@13672
   291
apply (rule conjI) 
streckem@13672
   292
  apply (simp add: np_def)
streckem@13672
   293
  apply (fast intro: conforms_xcpt_change xconf_raise_if)
oheimb@11026
   294
apply( fast elim!: FAcc_type_sound)
oheimb@11026
   295
kleing@12517
   296
-- "5 While"
oheimb@11026
   297
prefer 5
oheimb@11026
   298
apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
oheimb@11026
   299
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
oheimb@11026
   300
apply(force elim: hext_trans)
oheimb@11026
   301
oheimb@11026
   302
apply (tactic "forward_hyp_tac")
oheimb@11026
   303
streckem@13672
   304
-- "4 Cond"
streckem@13672
   305
prefer 4
streckem@13672
   306
apply (case_tac "the_Bool v")
streckem@13672
   307
apply simp
streckem@13672
   308
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
streckem@13672
   309
apply simp
oheimb@11026
   310
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
oheimb@11026
   311
kleing@12517
   312
-- "3 ;;"
oheimb@11026
   313
prefer 3
streckem@13672
   314
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
streckem@13672
   315
oheimb@11026
   316
kleing@12517
   317
-- "2 FAss"
streckem@13672
   318
apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)")
streckem@13672
   319
  prefer 2
streckem@13672
   320
  apply (simp add: np_def)
streckem@13672
   321
  apply (fast intro: conforms_xcpt_change xconf_raise_if)
streckem@13672
   322
apply( case_tac "x2")
streckem@13672
   323
  -- "x2 = None"
streckem@13672
   324
  apply (simp)
streckem@13672
   325
  apply (tactic forward_hyp_tac, clarify)
streckem@13672
   326
  apply( drule eval_no_xcpt)
streckem@13672
   327
  apply( erule FAss_type_sound, rule HOL.refl, assumption+)
streckem@13672
   328
  -- "x2 = Some a"
streckem@13672
   329
  apply (  simp (no_asm_simp))
streckem@13672
   330
  apply(  fast intro: hext_trans)
streckem@13672
   331
oheimb@11026
   332
oheimb@11026
   333
apply( tactic prune_params_tac)
kleing@12517
   334
-- "Level 52"
oheimb@11026
   335
kleing@12517
   336
-- "1 Call"
oheimb@11026
   337
apply( case_tac "x")
oheimb@11026
   338
prefer 2
oheimb@11026
   339
apply(  clarsimp)
oheimb@11026
   340
apply(  drule exec_xcpt)
oheimb@11026
   341
apply(  simp)
oheimb@11026
   342
apply(  drule_tac eval_xcpt)
oheimb@11026
   343
apply(  simp)
oheimb@11026
   344
apply(  fast elim: hext_trans)
oheimb@11026
   345
apply( clarify)
oheimb@11026
   346
apply( drule evals_no_xcpt)
oheimb@11026
   347
apply( simp)
oheimb@11026
   348
apply( case_tac "a' = Null")
oheimb@11026
   349
apply(  simp)
oheimb@11026
   350
apply(  drule exec_xcpt)
oheimb@11026
   351
apply(  simp)
oheimb@11026
   352
apply(  drule eval_xcpt)
oheimb@11026
   353
apply(  simp)
streckem@13672
   354
apply (rule conjI)
streckem@13672
   355
  apply(  fast elim: hext_trans)
streckem@14045
   356
  apply (rule conforms_xcpt_change, assumption) 
streckem@14045
   357
  apply (simp (no_asm_simp) add: xconf_def)
streckem@13672
   358
apply(clarsimp)
streckem@13672
   359
streckem@13672
   360
apply( drule ty_expr_is_type, simp)
oheimb@11026
   361
apply(clarsimp)
oheimb@11026
   362
apply(unfold is_class_def)
oheimb@11026
   363
apply(clarsimp)
streckem@13672
   364
streckem@11644
   365
apply(rule Call_type_sound);
oheimb@11026
   366
prefer 11
oheimb@11026
   367
apply blast
streckem@11644
   368
apply (simp (no_asm_simp))+ 
streckem@13672
   369
oheimb@11026
   370
done
oheimb@11026
   371
ML{*
oheimb@11026
   372
Unify.search_bound := 20;
oheimb@11026
   373
Unify.trace_bound  := 20
oheimb@11026
   374
*}
oheimb@11026
   375
streckem@14142
   376
oheimb@11026
   377
lemma eval_type_sound: "!!E s s'.  
streckem@14142
   378
  [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]  
streckem@14142
   379
  ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T) \<and> heap s \<le>| heap s'"
streckem@14142
   380
apply (simp (no_asm_simp) only: split_tupled_all)
streckem@14142
   381
apply (drule eval_evals_exec_type_sound [THEN conjunct1, THEN mp, THEN spec, THEN mp])
oheimb@11026
   382
apply auto
oheimb@11026
   383
done
oheimb@11026
   384
streckem@14142
   385
streckem@14045
   386
lemma evals_type_sound: "!!E s s'.  
streckem@14142
   387
  [| wf_java_prog G; G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>es[::]Ts; G=prg E |]  
streckem@14142
   388
  ==> (x',s')::\<preceq>E \<and> (x'=None --> (list_all2 (\<lambda>v T. G,heap s'\<turnstile>v::\<preceq>T) vs Ts)) \<and> heap s \<le>| heap s'"
streckem@14142
   389
apply (simp (no_asm_simp) only: split_tupled_all)
streckem@14142
   390
apply (drule eval_evals_exec_type_sound [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
streckem@14045
   391
apply auto
streckem@14045
   392
done
streckem@14045
   393
oheimb@11026
   394
lemma exec_type_sound: "!!E s s'.  
streckem@14142
   395
  \<lbrakk> wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd>; G=prg E \<rbrakk>
streckem@14142
   396
  \<Longrightarrow> (x',s')::\<preceq>E \<and> heap s \<le>| heap s'"
oheimb@11026
   397
apply( simp (no_asm_simp) only: split_tupled_all)
oheimb@11026
   398
apply (drule eval_evals_exec_type_sound 
oheimb@11026
   399
             [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
oheimb@11026
   400
apply   auto
oheimb@11026
   401
done
oheimb@11026
   402
oheimb@11026
   403
theorem all_methods_understood: 
oheimb@11026
   404
"[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; 
streckem@13672
   405
          (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>  
oheimb@11026
   406
  method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
streckem@14142
   407
apply (frule eval_type_sound, assumption+)
oheimb@11026
   408
apply(clarsimp)
oheimb@11026
   409
apply( frule widen_methd)
streckem@14142
   410
apply assumption
oheimb@11026
   411
prefer 2
oheimb@11026
   412
apply(  fast)
oheimb@11026
   413
apply( drule non_npD)
oheimb@11026
   414
apply auto
oheimb@11026
   415
done
oheimb@11026
   416
oheimb@11026
   417
declare split_beta [simp del]
oheimb@11026
   418
declare fun_upd_apply [simp]
streckem@14045
   419
declare wf_prog_ws_prog [simp del]
oheimb@11026
   420
oheimb@11026
   421
end
oheimb@11026
   422