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