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