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