src/HOL/MicroJava/J/JTypeSafe.thy
author oheimb
Mon Feb 05 20:14:15 2001 +0100 (2001-02-05)
changeset 11070 cc421547e744
parent 11026 a50365d21144
child 11644 3dfde687f0d7
permissions -rw-r--r--
improved document (added headers etc)
     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 (unfold wf_java_prog_def)
   122 apply( drule max_spec2mheads)
   123 apply( clarify)
   124 apply( drule (2) non_np_objD')
   125 apply(  clarsimp)
   126 apply( clarsimp)
   127 apply( frule (1) hext_objD)
   128 apply( clarsimp)
   129 apply( drule (3) Call_lemma)
   130 apply( clarsimp simp add: wf_java_mdecl_def)
   131 apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
   132 apply( drule spec, erule impE)
   133 apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
   134 apply(  rule conformsI)
   135 apply(   erule conforms_heapD)
   136 apply(  rule lconf_ext)
   137 apply(   force elim!: Call_lemma2)
   138 apply(  erule conf_hext, erule (1) conf_obj_AddrI)
   139 apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
   140 apply( erule conjE)
   141 apply( drule spec, erule (1) impE)
   142 apply( drule spec, erule (1) impE)
   143 apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
   144 apply( clarify)
   145 apply( rule conjI)
   146 apply(  fast intro: hext_trans)
   147 apply( rule conjI)
   148 apply(  rule_tac [2] impI)
   149 apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
   150 apply(  frule_tac [2] conf_widen)
   151 apply(    tactic "assume_tac 4")
   152 apply(   tactic "assume_tac 2")
   153 prefer 2
   154 apply(  fast elim!: widen_trans)
   155 apply( erule conforms_hext)
   156 apply(  erule (1) hext_trans)
   157 apply( erule conforms_heapD)
   158 done
   159 
   160 declare split_if [split del]
   161 declare fun_upd_apply [simp del]
   162 declare fun_upd_same [simp]
   163 ML{*
   164 val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
   165 	(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
   166 *}
   167 ML{*
   168 Unify.search_bound := 40;
   169 Unify.trace_bound  := 40
   170 *}
   171 theorem eval_evals_exec_type_sound: 
   172 "wf_java_prog G ==>  
   173   (G\<turnstile>(x,(h,l)) -e  \<succ>v  -> (x', (h',l')) -->  
   174       (\<forall>lT.   (h ,l )::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e  :: T -->  
   175       h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v  ::\<preceq> T )))) \<and>  
   176   (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->  
   177       (\<forall>lT.   (h ,l )::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->  
   178       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>  
   179   (G\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) -->  
   180       (\<forall>lT.   (h ,l )::\<preceq>(G,lT) -->       (G,lT)\<turnstile>c  \<surd> -->  
   181       h\<le>|h' \<and> (h',l')::\<preceq>(G,lT)))"
   182 apply( rule eval_evals_exec_induct)
   183 apply( unfold c_hupd_def)
   184 
   185 (* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
   186 apply( simp_all)
   187 apply( tactic "ALLGOALS strip_tac")
   188 apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *})
   189 apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
   190 apply( unfold wf_java_prog_def)
   191 
   192 (* Level 7 *)
   193 
   194 (* 15 NewC *)
   195 apply( drule new_AddrD)
   196 apply( erule disjE)
   197 prefer 2
   198 apply(  simp (no_asm_simp))
   199 apply( clarsimp)
   200 apply( rule conjI)
   201 apply(  force elim!: NewC_conforms)
   202 apply( rule conf_obj_AddrI)
   203 apply(  rule_tac [2] rtrancl_refl)
   204 apply( simp (no_asm))
   205 
   206 (* for Cast *)
   207 defer 1
   208 
   209 (* 14 Lit *)
   210 apply( erule conf_litval)
   211 
   212 (* 13 BinOp *)
   213 apply (tactic "forward_hyp_tac")
   214 apply (tactic "forward_hyp_tac")
   215 apply( rule conjI, erule (1) hext_trans)
   216 apply( erule conjI)
   217 apply( clarsimp)
   218 apply( drule eval_no_xcpt)
   219 apply( simp split add: binop.split)
   220 
   221 (* 12 LAcc *)
   222 apply( fast elim: conforms_localD [THEN lconfD])
   223 
   224 (* for FAss *)
   225 apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 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") THEN_ALL_NEW Full_simp_tac) 1 *})
   255 apply( blast intro: conforms_upd_local conf_widen)
   256 
   257 (* 6 FAcc *)
   258 apply( fast elim!: FAcc_type_sound)
   259 
   260 (* 5 While *)
   261 prefer 5
   262 apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
   263 apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
   264 apply(force elim: hext_trans)
   265 
   266 apply (tactic "forward_hyp_tac")
   267 
   268 (* 4 Cons *)
   269 prefer 3
   270 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
   271 
   272 (* 3 ;; *)
   273 prefer 3
   274 apply( fast intro: hext_trans)
   275 
   276 (* 2 FAss *)
   277 apply( case_tac "x2 = None")
   278 prefer 2
   279 apply(  simp (no_asm_simp))
   280 apply(  fast intro: hext_trans)
   281 apply( simp)
   282 apply( drule eval_no_xcpt)
   283 apply( erule FAss_type_sound, rule HOL.refl, assumption+)
   284 
   285 apply( tactic prune_params_tac)
   286 (* Level 52 *)
   287 
   288 (* 1 Call *)
   289 apply( case_tac "x")
   290 prefer 2
   291 apply(  clarsimp)
   292 apply(  drule exec_xcpt)
   293 apply(  simp)
   294 apply(  drule_tac eval_xcpt)
   295 apply(  simp)
   296 apply(  fast elim: hext_trans)
   297 apply( clarify)
   298 apply( drule evals_no_xcpt)
   299 apply( simp)
   300 apply( case_tac "a' = Null")
   301 apply(  simp)
   302 apply(  drule exec_xcpt)
   303 apply(  simp)
   304 apply(  drule eval_xcpt)
   305 apply(  simp)
   306 apply(  fast elim: hext_trans)
   307 apply( drule (1) ty_expr_is_type)
   308 apply(clarsimp)
   309 apply(unfold is_class_def)
   310 apply(clarsimp)
   311 apply(rule Call_type_sound [unfolded wf_java_prog_def]);
   312 prefer 11
   313 apply blast
   314 apply (simp (no_asm_simp))+
   315 done
   316 ML{*
   317 Unify.search_bound := 20;
   318 Unify.trace_bound  := 20
   319 *}
   320 
   321 lemma eval_type_sound: "!!E s s'.  
   322   [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); s::\<preceq>E; E\<turnstile>e::T |]  
   323   ==> s'::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
   324 apply( simp (no_asm_simp) only: split_tupled_all)
   325 apply (drule eval_evals_exec_type_sound 
   326              [THEN conjunct1, THEN mp, THEN spec, THEN mp])
   327 apply auto
   328 done
   329 
   330 lemma exec_type_sound: "!!E s s'.  
   331   [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); s::\<preceq>E; E\<turnstile>s0\<surd> |]  
   332   ==> s'::\<preceq>E"
   333 apply( simp (no_asm_simp) only: split_tupled_all)
   334 apply (drule eval_evals_exec_type_sound 
   335              [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
   336 apply   auto
   337 done
   338 
   339 theorem all_methods_understood: 
   340 "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; 
   341           s::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>  
   342   method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
   343 apply( drule (4) eval_type_sound)
   344 apply(clarsimp)
   345 apply(unfold wf_java_prog_def)
   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