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