src/HOL/MicroJava/J/WellForm.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 33640 0d82107dc07a
child 35416 d8d7d1b785af
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
     1 (*  Title:      HOL/MicroJava/J/WellForm.thy
     2     Author:     David von Oheimb
     3     Copyright   1999 Technische Universitaet Muenchen
     4 *)
     5 
     6 header {* \isaheader{Well-formedness of Java programs} *}
     7 
     8 theory WellForm
     9 imports TypeRel SystemClasses
    10 begin
    11 
    12 text {*
    13 for static checks on expressions and statements, see WellType.
    14 
    15 \begin{description}
    16 \item[improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):]\ \\
    17 \begin{itemize}
    18 \item a method implementing or overwriting another method may have a result type
    19 that widens to the result type of the other method (instead of identical type)
    20 \end{itemize}
    21 
    22 \item[simplifications:]\ \\
    23 \begin{itemize}
    24 \item for uniformity, Object is assumed to be declared like any other class
    25 \end{itemize}
    26 \end{description}
    27 *}
    28 types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
    29 
    30 constdefs
    31  wf_syscls :: "'c prog => bool"
    32 "wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
    33 
    34  wf_fdecl :: "'c prog => fdecl => bool"
    35 "wf_fdecl G == \<lambda>(fn,ft). is_type G ft"
    36 
    37  wf_mhead :: "'c prog => sig => ty => bool"
    38 "wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT"
    39 
    40  ws_cdecl :: "'c prog => 'c cdecl => bool"
    41 "ws_cdecl G ==
    42    \<lambda>(C,(D,fs,ms)).
    43   (\<forall>f\<in>set fs. wf_fdecl G         f) \<and>  unique fs \<and>
    44   (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT) \<and> unique ms \<and>
    45   (C \<noteq> Object \<longrightarrow> is_class G D \<and>  \<not>G\<turnstile>D\<preceq>C C)"
    46 
    47  ws_prog :: "'c prog => bool"
    48 "ws_prog G == 
    49   wf_syscls G \<and> (\<forall>c\<in>set G. ws_cdecl G c) \<and> unique G"
    50 
    51  wf_mrT   :: "'c prog => 'c cdecl => bool"
    52 "wf_mrT G ==
    53    \<lambda>(C,(D,fs,ms)).
    54   (C \<noteq> Object \<longrightarrow> (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
    55                       method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
    56 
    57  wf_cdecl_mdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
    58 "wf_cdecl_mdecl wf_mb G ==
    59    \<lambda>(C,(D,fs,ms)). (\<forall>m\<in>set ms. wf_mb G C m)"
    60 
    61  wf_prog :: "'c wf_mb => 'c prog => bool"
    62 "wf_prog wf_mb G == 
    63      ws_prog G \<and> (\<forall>c\<in> set G. wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)"
    64 
    65  wf_mdecl :: "'c wf_mb => 'c wf_mb"
    66 "wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)"
    67 
    68  wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
    69 "wf_cdecl wf_mb G ==
    70    \<lambda>(C,(D,fs,ms)).
    71   (\<forall>f\<in>set fs. wf_fdecl G         f) \<and>  unique fs \<and>
    72   (\<forall>m\<in>set ms. wf_mdecl wf_mb G C m) \<and>  unique ms \<and>
    73   (C \<noteq> Object \<longrightarrow> is_class G D \<and>  \<not>G\<turnstile>D\<preceq>C C \<and>
    74                    (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
    75                       method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
    76 
    77 lemma wf_cdecl_mrT_cdecl_mdecl:
    78   "(wf_cdecl wf_mb G c) = (ws_cdecl G c \<and> wf_mrT G c \<and> wf_cdecl_mdecl wf_mb G c)"
    79 apply (rule iffI)
    80 apply (simp add: wf_cdecl_def ws_cdecl_def wf_mrT_def wf_cdecl_mdecl_def 
    81   wf_mdecl_def wf_mhead_def split_beta)+
    82 done
    83 
    84 lemma wf_cdecl_ws_cdecl [intro]: "wf_cdecl wf_mb G cd \<Longrightarrow> ws_cdecl G cd"
    85 by (simp add: wf_cdecl_mrT_cdecl_mdecl)
    86 
    87 lemma wf_prog_ws_prog [intro]: "wf_prog wf_mb G \<Longrightarrow> ws_prog G"
    88 by (simp add: wf_prog_def ws_prog_def)
    89 
    90 lemma wf_prog_wf_mdecl: 
    91   "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; ((mn,pTs),rT,code) \<in> set mdecls\<rbrakk>
    92   \<Longrightarrow> wf_mdecl wf_mb G C ((mn,pTs),rT,code)"
    93 by (auto simp add: wf_prog_def ws_prog_def wf_mdecl_def  
    94   wf_cdecl_mdecl_def ws_cdecl_def)
    95 
    96 lemma class_wf: 
    97  "[|class G C = Some c; wf_prog wf_mb G|] 
    98   ==> wf_cdecl wf_mb G (C,c) \<and> wf_mrT G (C,c)"
    99 apply (unfold wf_prog_def ws_prog_def wf_cdecl_def class_def)
   100 apply clarify
   101 apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
   102 apply (drule_tac x="(C,c)" in bspec, fast dest: map_of_SomeD)
   103 apply (simp add: wf_cdecl_def ws_cdecl_def wf_mdecl_def
   104   wf_cdecl_mdecl_def wf_mrT_def split_beta)
   105 done
   106 
   107 lemma class_wf_struct: 
   108  "[|class G C = Some c; ws_prog G|] 
   109   ==> ws_cdecl G (C,c)"
   110 apply (unfold ws_prog_def class_def)
   111 apply (fast dest: map_of_SomeD)
   112 done
   113 
   114 lemma class_Object [simp]: 
   115   "ws_prog G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
   116 apply (unfold ws_prog_def wf_syscls_def class_def)
   117 apply (auto simp: map_of_SomeI)
   118 done
   119 
   120 lemma class_Object_syscls [simp]: 
   121   "wf_syscls G ==> unique G \<Longrightarrow> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
   122 apply (unfold wf_syscls_def class_def)
   123 apply (auto simp: map_of_SomeI)
   124 done
   125 
   126 lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
   127   by (simp add: is_class_def)
   128 
   129 lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)"
   130   apply (simp add: ws_prog_def wf_syscls_def)
   131   apply (simp add: is_class_def class_def)
   132   apply clarify
   133   apply (erule_tac x = x in allE)
   134   apply clarify
   135   apply (auto intro!: map_of_SomeI)
   136   done
   137 
   138 lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> (D, C) \<notin> (subcls1 G)^+"
   139 apply( frule trancl.r_into_trancl [where r="subcls1 G"])
   140 apply( drule subcls1D)
   141 apply(clarify)
   142 apply( drule (1) class_wf_struct)
   143 apply( unfold ws_cdecl_def)
   144 apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
   145 done
   146 
   147 lemma wf_cdecl_supD: 
   148 "!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
   149 apply (unfold ws_cdecl_def)
   150 apply (auto split add: option.split_asm)
   151 done
   152 
   153 lemma subcls_asym: "[|ws_prog G; (C, D) \<in> (subcls1 G)^+|] ==> (D, C) \<notin> (subcls1 G)^+"
   154 apply(erule trancl.cases)
   155 apply(fast dest!: subcls1_wfD )
   156 apply(fast dest!: subcls1_wfD intro: trancl_trans)
   157 done
   158 
   159 lemma subcls_irrefl: "[|ws_prog G; (C, D) \<in> (subcls1 G)^+|] ==> C \<noteq> D"
   160 apply (erule trancl_trans_induct)
   161 apply  (auto dest: subcls1_wfD subcls_asym)
   162 done
   163 
   164 lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
   165 apply (simp add: acyclic_def)
   166 apply (fast dest: subcls_irrefl)
   167 done
   168 
   169 lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
   170 apply (rule finite_acyclic_wf)
   171 apply ( subst finite_converse)
   172 apply ( rule finite_subcls1)
   173 apply (subst acyclic_converse)
   174 apply (erule acyclic_subcls1)
   175 done
   176 
   177 lemma subcls_induct_struct: 
   178 "[|ws_prog G; !!C. \<forall>D. (C, D) \<in> (subcls1 G)^+ --> P D ==> P C|] ==> P C"
   179 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
   180 proof -
   181   assume p: "PROP ?P"
   182   assume ?A thus ?thesis apply -
   183 apply(drule wf_subcls1)
   184 apply(drule wf_trancl)
   185 apply(simp only: trancl_converse)
   186 apply(erule_tac a = C in wf_induct)
   187 apply(rule p)
   188 apply(auto)
   189 done
   190 qed
   191 
   192 lemma subcls_induct: 
   193 "[|wf_prog wf_mb G; !!C. \<forall>D. (C, D) \<in> (subcls1 G)^+ --> P D ==> P C|] ==> P C"
   194 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
   195 by (fact subcls_induct_struct [OF wf_prog_ws_prog])
   196 
   197 lemma subcls1_induct:
   198 "[|is_class G C; wf_prog wf_mb G; P Object;  
   199    !!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and>  
   200     wf_cdecl wf_mb G (C,D,fs,ms) \<and> G\<turnstile>C\<prec>C1D \<and> is_class G D \<and> P D|] ==> P C 
   201  |] ==> P C"
   202 (is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
   203 proof -
   204   assume p: "PROP ?P"
   205   assume ?A ?B ?C thus ?thesis apply -
   206 apply(unfold is_class_def)
   207 apply( rule impE)
   208 prefer 2
   209 apply(   assumption)
   210 prefer 2
   211 apply(  assumption)
   212 apply( erule thin_rl)
   213 apply( rule subcls_induct)
   214 apply(  assumption)
   215 apply( rule impI)
   216 apply( case_tac "C = Object")
   217 apply(  fast)
   218 apply auto
   219 apply( frule (1) class_wf) apply (erule conjE)+
   220 apply (frule wf_cdecl_ws_cdecl)
   221 apply( frule (1) wf_cdecl_supD)
   222 
   223 apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
   224 apply( erule_tac [2] subcls1I)
   225 apply(  rule p)
   226 apply (unfold is_class_def)
   227 apply auto
   228 done
   229 qed
   230 
   231 lemma subcls1_induct_struct:
   232 "[|is_class G C; ws_prog G; P Object;  
   233    !!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and>  
   234     ws_cdecl G (C,D,fs,ms) \<and> G\<turnstile>C\<prec>C1D \<and> is_class G D \<and> P D|] ==> P C 
   235  |] ==> P C"
   236 (is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
   237 proof -
   238   assume p: "PROP ?P"
   239   assume ?A ?B ?C thus ?thesis apply -
   240 apply(unfold is_class_def)
   241 apply( rule impE)
   242 prefer 2
   243 apply(   assumption)
   244 prefer 2
   245 apply(  assumption)
   246 apply( erule thin_rl)
   247 apply( rule subcls_induct_struct)
   248 apply(  assumption)
   249 apply( rule impI)
   250 apply( case_tac "C = Object")
   251 apply(  fast)
   252 apply auto
   253 apply( frule (1) class_wf_struct)
   254 apply( frule (1) wf_cdecl_supD)
   255 
   256 apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
   257 apply( erule_tac [2] subcls1I)
   258 apply(  rule p)
   259 apply (unfold is_class_def)
   260 apply auto
   261 done
   262 qed
   263 
   264 lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma];
   265 
   266 lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
   267 
   268 lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); ws_prog G\<rbrakk>
   269 \<Longrightarrow> field (G, C) =
   270    (if C = Object then empty else field (G, D)) ++
   271    map_of (map (\<lambda>(s, f). (s, C, f)) fs)"
   272 apply (simp only: field_def)
   273 apply (frule fields_rec, assumption)
   274 apply (rule HOL.trans)
   275 apply (simp add: o_def)
   276 apply (simp (no_asm_use) add: split_beta split_def o_def)
   277 done
   278 
   279 lemma method_Object [simp]:
   280   "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> ws_prog G \<Longrightarrow> D = Object"  
   281   apply (frule class_Object, clarify)
   282   apply (drule method_rec, assumption)
   283   apply (auto dest: map_of_SomeD)
   284   done
   285 
   286 
   287 lemma fields_Object [simp]: "\<lbrakk> ((vn, C), T) \<in> set (fields (G, Object)); ws_prog G \<rbrakk>
   288   \<Longrightarrow> C = Object"
   289 apply (frule class_Object)
   290 apply clarify
   291 apply (subgoal_tac "fields (G, Object) = map (\<lambda>(fn,ft). ((fn,Object),ft)) fs")
   292 apply (simp add: image_iff split_beta)
   293 apply auto
   294 apply (rule trans)
   295 apply (rule fields_rec, assumption+)
   296 apply simp
   297 done
   298 
   299 lemma subcls_C_Object: "[|is_class G C; ws_prog G|] ==> G\<turnstile>C\<preceq>C Object"
   300 apply(erule subcls1_induct_struct)
   301 apply(  assumption)
   302 apply( fast)
   303 apply(auto dest!: wf_cdecl_supD)
   304 done
   305 
   306 lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
   307 apply (unfold wf_mhead_def)
   308 apply auto
   309 done
   310 
   311 lemma widen_fields_defpl': "[|is_class G C; ws_prog G|] ==>  
   312   \<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
   313 apply( erule subcls1_induct_struct)
   314 apply(   assumption)
   315 apply(  frule class_Object)
   316 apply(  clarify)
   317 apply(  frule fields_rec, assumption)
   318 apply(  fastsimp)
   319 apply( tactic "safe_tac HOL_cs")
   320 apply( subst fields_rec)
   321 apply(   assumption)
   322 apply(  assumption)
   323 apply( simp (no_asm) split del: split_if)
   324 apply( rule ballI)
   325 apply( simp (no_asm_simp) only: split_tupled_all)
   326 apply( simp (no_asm))
   327 apply( erule UnE)
   328 apply(  force)
   329 apply( erule r_into_rtrancl [THEN rtrancl_trans])
   330 apply auto
   331 done
   332 
   333 lemma widen_fields_defpl: 
   334   "[|((fn,fd),fT) \<in> set (fields (G,C)); ws_prog G; is_class G C|] ==>  
   335   G\<turnstile>C\<preceq>C fd"
   336 apply( drule (1) widen_fields_defpl')
   337 apply (fast)
   338 done
   339 
   340 lemma unique_fields: 
   341   "[|is_class G C; ws_prog G|] ==> unique (fields (G,C))"
   342 apply( erule subcls1_induct_struct)
   343 apply(   assumption)
   344 apply(  frule class_Object)
   345 apply(  clarify)
   346 apply(  frule fields_rec, assumption)
   347 apply(  drule class_wf_struct, assumption)
   348 apply(  simp add: ws_cdecl_def)
   349 apply(  rule unique_map_inj)
   350 apply(   simp)
   351 apply(  rule inj_onI)
   352 apply(  simp)
   353 apply( safe dest!: wf_cdecl_supD)
   354 apply( drule subcls1_wfD)
   355 apply(  assumption)
   356 apply( subst fields_rec)
   357 apply   auto
   358 apply( rotate_tac -1)
   359 apply( frule class_wf_struct)
   360 apply  auto
   361 apply( simp add: ws_cdecl_def)
   362 apply( erule unique_append)
   363 apply(  rule unique_map_inj)
   364 apply(   clarsimp)
   365 apply  (rule inj_onI)
   366 apply(  simp)
   367 apply(auto dest!: widen_fields_defpl)
   368 done
   369 
   370 lemma fields_mono_lemma [rule_format (no_asm)]: 
   371   "[|ws_prog G; (C', C) \<in> (subcls1 G)^*|] ==>  
   372   x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
   373 apply(erule converse_rtrancl_induct)
   374 apply( safe dest!: subcls1D)
   375 apply(subst fields_rec)
   376 apply(  auto)
   377 done
   378 
   379 lemma fields_mono: 
   380 "\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; ws_prog G\<rbrakk> 
   381   \<Longrightarrow> map_of (fields (G,D)) fn = Some f"
   382 apply (rule map_of_SomeI)
   383 apply  (erule (1) unique_fields)
   384 apply (erule (1) fields_mono_lemma)
   385 apply (erule map_of_SomeD)
   386 done
   387 
   388 lemma widen_cfs_fields: 
   389 "[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>  
   390   map_of (fields (G,D)) (fn, fd) = Some fT"
   391 apply (drule field_fields)
   392 apply (drule rtranclD)
   393 apply safe
   394 apply (frule subcls_is_class)
   395 apply (drule trancl_into_rtrancl)
   396 apply (fast dest: fields_mono)
   397 done
   398 
   399 lemma method_wf_mdecl [rule_format (no_asm)]: 
   400   "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   
   401      method (G,C) sig = Some (md,mh,m) 
   402    --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
   403 apply (frule wf_prog_ws_prog)
   404 apply( erule subcls1_induct)
   405 apply(   assumption)
   406 apply(  clarify) 
   407 apply(  frule class_Object)
   408 apply(  clarify)
   409 apply(  frule method_rec, assumption)
   410 apply(  drule class_wf, assumption)
   411 apply(  simp add: wf_cdecl_def)
   412 apply(  drule map_of_SomeD)
   413 apply(  subgoal_tac "md = Object")
   414 apply(   fastsimp) 
   415 apply(  fastsimp)
   416 apply( clarify)
   417 apply( frule_tac C = C in method_rec)
   418 apply(  assumption)
   419 apply( rotate_tac -1)
   420 apply( simp)
   421 apply( drule map_add_SomeD)
   422 apply( erule disjE)
   423 apply(  erule_tac V = "?P --> ?Q" in thin_rl)
   424 apply (frule map_of_SomeD)
   425 apply (clarsimp simp add: wf_cdecl_def)
   426 apply( clarify)
   427 apply( rule rtrancl_trans)
   428 prefer 2
   429 apply(  assumption)
   430 apply( rule r_into_rtrancl)
   431 apply( fast intro: subcls1I)
   432 done
   433 
   434 
   435 lemma method_wf_mhead [rule_format (no_asm)]: 
   436   "ws_prog G ==> is_class G C \<Longrightarrow>   
   437      method (G,C) sig = Some (md,rT,mb) 
   438    --> G\<turnstile>C\<preceq>C md \<and> wf_mhead G sig rT"
   439 apply( erule subcls1_induct_struct)
   440 apply(   assumption)
   441 apply(  clarify) 
   442 apply(  frule class_Object)
   443 apply(  clarify)
   444 apply(  frule method_rec, assumption)
   445 apply(  drule class_wf_struct, assumption)
   446 apply(  simp add: ws_cdecl_def)
   447 apply(  drule map_of_SomeD)
   448 apply(  subgoal_tac "md = Object")
   449 apply(   fastsimp)
   450 apply(  fastsimp)
   451 apply( clarify)
   452 apply( frule_tac C = C in method_rec)
   453 apply(  assumption)
   454 apply( rotate_tac -1)
   455 apply( simp)
   456 apply( drule map_add_SomeD)
   457 apply( erule disjE)
   458 apply(  erule_tac V = "?P --> ?Q" in thin_rl)
   459 apply (frule map_of_SomeD)
   460 apply (clarsimp simp add: ws_cdecl_def)
   461 apply blast
   462 apply clarify
   463 apply( rule rtrancl_trans)
   464 prefer 2
   465 apply(  assumption)
   466 apply( rule r_into_rtrancl)
   467 apply( fast intro: subcls1I)
   468 done
   469 
   470 lemma subcls_widen_methd [rule_format (no_asm)]: 
   471   "[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>  
   472    \<forall>D rT b. method (G,T) sig = Some (D,rT ,b) --> 
   473   (\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)"
   474 apply( drule rtranclD)
   475 apply( erule disjE)
   476 apply(  fast)
   477 apply( erule conjE)
   478 apply( erule trancl_trans_induct)
   479 prefer 2
   480 apply(  clarify)
   481 apply(  drule spec, drule spec, drule spec, erule (1) impE)
   482 apply(  fast elim: widen_trans rtrancl_trans)
   483 apply( clarify)
   484 apply( drule subcls1D)
   485 apply( clarify)
   486 apply( subst method_rec)
   487 apply(  assumption)
   488 apply( unfold map_add_def)
   489 apply( simp (no_asm_simp) add: wf_prog_ws_prog del: split_paired_Ex)
   490 apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
   491 apply(  erule exE)
   492 apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
   493 prefer 2
   494 apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
   495 apply(  tactic "asm_full_simp_tac (HOL_ss addsimps [@{thm not_None_eq} RS sym]) 1")
   496 apply(  simp_all (no_asm_simp) del: split_paired_Ex)
   497 apply( frule (1) class_wf)
   498 apply( simp (no_asm_simp) only: split_tupled_all)
   499 apply( unfold wf_cdecl_def)
   500 apply( drule map_of_SomeD)
   501 apply (auto simp add: wf_mrT_def)
   502 apply (rule rtrancl_trans)
   503 defer
   504 apply (rule method_wf_mhead [THEN conjunct1])
   505 apply (simp only: wf_prog_def)
   506 apply (simp add: is_class_def)
   507 apply assumption
   508 apply (auto intro: subcls1I)
   509 done
   510 
   511 
   512 lemma subtype_widen_methd: 
   513  "[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;  
   514      method (G,D) sig = Some (md, rT, b) |]  
   515   ==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
   516 apply(auto dest: subcls_widen_methd 
   517            simp add: wf_mdecl_def wf_mhead_def split_def)
   518 done
   519 
   520 
   521 lemma method_in_md [rule_format (no_asm)]: 
   522   "ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
   523   --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
   524 apply (erule (1) subcls1_induct_struct)
   525  apply clarify
   526  apply (frule method_Object, assumption)
   527  apply hypsubst
   528  apply simp
   529 apply (erule conjE)
   530 apply (simplesubst method_rec, assumption+)
   531 apply (clarify)
   532 apply (erule_tac x = "Da" in allE)
   533 apply (clarsimp)
   534  apply (simp add: map_of_map)
   535  apply (clarify)
   536  apply (subst method_rec, assumption+)
   537  apply (simp add: map_add_def map_of_map split add: option.split)
   538 done
   539 
   540 
   541 lemma method_in_md_struct [rule_format (no_asm)]: 
   542   "ws_prog G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
   543   --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
   544 apply (erule (1) subcls1_induct_struct)
   545  apply clarify
   546  apply (frule method_Object, assumption)
   547  apply hypsubst
   548  apply simp
   549 apply (erule conjE)
   550 apply (simplesubst method_rec, assumption+)
   551 apply (clarify)
   552 apply (erule_tac x = "Da" in allE)
   553 apply (clarsimp)
   554  apply (simp add: map_of_map)
   555  apply (clarify)
   556  apply (subst method_rec, assumption+)
   557  apply (simp add: map_add_def map_of_map split add: option.split)
   558 done
   559 
   560 lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
   561   \<Longrightarrow> \<forall> vn D T. (((vn,D),T) \<in> set (fields (G,C))
   562   \<longrightarrow> (is_class G D \<and> ((vn,D),T) \<in> set (fields (G,D))))"
   563 apply (erule (1) subcls1_induct)
   564 
   565 apply clarify
   566 apply (frule wf_prog_ws_prog)
   567 apply (frule fields_Object, assumption+)
   568 apply (simp only: is_class_Object) apply simp
   569 
   570 apply clarify
   571 apply (frule fields_rec)
   572 apply (simp (no_asm_simp) add: wf_prog_ws_prog)
   573 
   574 apply (case_tac "Da=C")
   575 apply blast                     (* case Da=C *)
   576 
   577 apply (subgoal_tac "((vn, Da), T) \<in> set (fields (G, D))") apply blast
   578 apply (erule thin_rl)
   579 apply (rotate_tac 1)
   580 apply (erule thin_rl, erule thin_rl, erule thin_rl, 
   581       erule thin_rl, erule thin_rl, erule thin_rl)
   582 apply auto
   583 done
   584 
   585 lemma field_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
   586   \<Longrightarrow> \<forall> vn D T. (field (G,C) vn = Some(D,T) 
   587   \<longrightarrow> is_class G D \<and> field (G,D) vn = Some(D,T))"
   588 apply (erule (1) subcls1_induct)
   589 
   590 apply clarify
   591 apply (frule field_fields)
   592 apply (drule map_of_SomeD)
   593 apply (frule wf_prog_ws_prog)
   594 apply (drule fields_Object, assumption+)
   595 apply simp
   596 
   597 apply clarify
   598 apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)")
   599 apply (simp (no_asm_use) only: map_add_Some_iff)
   600 apply (erule disjE)
   601 apply (simp (no_asm_use) add: map_of_map) apply blast
   602 apply blast
   603 apply (rule trans [THEN sym], rule sym, assumption)
   604 apply (rule_tac x=vn in fun_cong)
   605 apply (rule trans, rule field_rec, assumption+)
   606 apply (simp (no_asm_simp) add: wf_prog_ws_prog) 
   607 apply (simp (no_asm_use)) apply blast
   608 done
   609 
   610 
   611 lemma widen_methd: 
   612 "[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\<turnstile>T''\<preceq>C C|] 
   613   ==> \<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
   614 apply( drule subcls_widen_methd)
   615 apply   auto
   616 done
   617 
   618 lemma widen_field: "\<lbrakk> (field (G,C) fn) = Some (fd, fT); wf_prog wf_mb G; is_class G C \<rbrakk>
   619   \<Longrightarrow> G\<turnstile>C\<preceq>C fd"
   620 apply (rule widen_fields_defpl)
   621 apply (simp add: field_def)
   622 apply (rule map_of_SomeD)
   623 apply (rule table_of_remap_SomeD) 
   624 apply assumption+
   625 apply (simp (no_asm_simp) add: wf_prog_ws_prog)+
   626 done
   627 
   628 lemma Call_lemma: 
   629 "[|method (G,C) sig = Some (md,rT,b); G\<turnstile>T''\<preceq>C C; wf_prog wf_mb G;  
   630   class G C = Some y|] ==> \<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \<and>  
   631   G\<turnstile>rT'\<preceq>rT \<and> G\<turnstile>T''\<preceq>C T' \<and> wf_mhead G sig rT' \<and> wf_mb G T' (sig,rT',b)"
   632 apply( drule (2) widen_methd)
   633 apply( clarify)
   634 apply( frule subcls_is_class2)
   635 apply (unfold is_class_def)
   636 apply (simp (no_asm_simp))
   637 apply( drule method_wf_mdecl)
   638 apply( unfold wf_mdecl_def)
   639 apply( unfold is_class_def)
   640 apply auto
   641 done
   642 
   643 lemma fields_is_type_lemma [rule_format (no_asm)]: 
   644   "[|is_class G C; ws_prog G|] ==>  
   645   \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
   646 apply( erule (1) subcls1_induct_struct)
   647 apply(  frule class_Object)
   648 apply(  clarify)
   649 apply(  frule fields_rec, assumption)
   650 apply(  drule class_wf_struct, assumption)
   651 apply(  simp add: ws_cdecl_def wf_fdecl_def)
   652 apply(  fastsimp)
   653 apply( subst fields_rec)
   654 apply(   fast)
   655 apply(  assumption)
   656 apply( clarsimp)
   657 apply( safe)
   658 prefer 2
   659 apply(  force)
   660 apply( drule (1) class_wf_struct)
   661 apply( unfold ws_cdecl_def)
   662 apply( clarsimp)
   663 apply( drule (1) bspec)
   664 apply( unfold wf_fdecl_def)
   665 apply auto
   666 done
   667 
   668 
   669 lemma fields_is_type: 
   670   "[|map_of (fields (G,C)) fn = Some f; ws_prog G; is_class G C|] ==>  
   671   is_type G f"
   672 apply(drule map_of_SomeD)
   673 apply(drule (2) fields_is_type_lemma)
   674 apply(auto)
   675 done
   676 
   677 
   678 lemma field_is_type: "\<lbrakk> ws_prog G; is_class G C; field (G, C) fn = Some (fd, fT) \<rbrakk>
   679   \<Longrightarrow> is_type G fT"
   680 apply (frule_tac f="((fn, fd), fT)" in fields_is_type_lemma)
   681 apply (auto simp add: field_def dest: map_of_SomeD)
   682 done
   683 
   684 
   685 lemma methd:
   686   "[| ws_prog G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
   687   ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
   688 proof -
   689   assume wf: "ws_prog G" and C:  "(C,S,fs,mdecls) \<in> set G" and
   690          m: "(sig,rT,code) \<in> set mdecls"
   691   moreover
   692   from wf C have "class G C = Some (S,fs,mdecls)"
   693     by (auto simp add: ws_prog_def class_def is_class_def intro: map_of_SomeI)
   694   moreover
   695   from wf C 
   696   have "unique mdecls" by (unfold ws_prog_def ws_cdecl_def) auto
   697   hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)  
   698   with m 
   699   have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
   700     by (force intro: map_of_SomeI)
   701   ultimately
   702   show ?thesis by (auto simp add: is_class_def dest: method_rec)
   703 qed
   704 
   705 
   706 lemma wf_mb'E:
   707   "\<lbrakk> wf_prog wf_mb G; \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set G; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_mb' G C m \<rbrakk>
   708   \<Longrightarrow> wf_prog wf_mb' G"
   709   apply (simp only: wf_prog_def)
   710   apply auto
   711   apply (simp add: wf_cdecl_mdecl_def)
   712   apply safe
   713   apply (drule bspec, assumption) apply simp
   714   done
   715 
   716 
   717 lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast
   718 
   719 lemma wf_syscls:
   720   "set SystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G"
   721   apply (drule fst_mono)
   722   apply (simp add: SystemClasses_def wf_syscls_def)
   723   apply (simp add: ObjectC_def) 
   724   apply (rule allI, case_tac x)
   725   apply (auto simp add: NullPointerC_def ClassCastC_def OutOfMemoryC_def)
   726   done
   727 
   728 end