src/HOL/MicroJava/J/WellForm.thy
author paulson
Thu Sep 26 10:51:29 2002 +0200 (2002-09-26)
changeset 13585 db4005b40cc6
parent 13051 8efb5d92cf55
child 13672 b95d12325b51
permissions -rw-r--r--
Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"
nipkow@8011
     1
(*  Title:      HOL/MicroJava/J/WellForm.thy
nipkow@8011
     2
    ID:         $Id$
nipkow@8011
     3
    Author:     David von Oheimb
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
oheimb@11070
     5
*)
nipkow@8011
     6
kleing@12911
     7
header {* \isaheader{Well-formedness of Java programs} *}
nipkow@8011
     8
kleing@12951
     9
theory WellForm = TypeRel + SystemClasses:
nipkow@8011
    10
oheimb@11070
    11
text {*
oheimb@11070
    12
for static checks on expressions and statements, see WellType.
oheimb@11070
    13
oheimb@11070
    14
\begin{description}
oheimb@11070
    15
\item[improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):]\ \\
oheimb@11070
    16
\begin{itemize}
oheimb@11070
    17
\item a method implementing or overwriting another method may have a result type
oheimb@11070
    18
that widens to the result type of the other method (instead of identical type)
oheimb@11070
    19
\end{itemize}
oheimb@11070
    20
oheimb@11070
    21
\item[simplifications:]\ \\
oheimb@11070
    22
\begin{itemize}
oheimb@11070
    23
\item for uniformity, Object is assumed to be declared like any other class
oheimb@11070
    24
\end{itemize}
oheimb@11070
    25
\end{description}
oheimb@11070
    26
*}
oheimb@11026
    27
types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
nipkow@8011
    28
nipkow@8011
    29
constdefs
kleing@10069
    30
 wf_fdecl :: "'c prog => fdecl => bool"
oheimb@11026
    31
"wf_fdecl G == \<lambda>(fn,ft). is_type G ft"
nipkow@8011
    32
kleing@10069
    33
 wf_mhead :: "'c prog => sig => ty => bool"
oheimb@11026
    34
"wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT"
nipkow@8011
    35
kleing@10061
    36
 wf_mdecl :: "'c wf_mb => 'c wf_mb"
oheimb@11026
    37
"wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)"
nipkow@8011
    38
kleing@10061
    39
 wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
kleing@10042
    40
"wf_cdecl wf_mb G ==
oheimb@11026
    41
   \<lambda>(C,(D,fs,ms)).
oheimb@11026
    42
  (\<forall>f\<in>set fs. wf_fdecl G         f) \<and>  unique fs \<and>
oheimb@11026
    43
  (\<forall>m\<in>set ms. wf_mdecl wf_mb G C m) \<and>  unique ms \<and>
oheimb@11026
    44
  (C \<noteq> Object \<longrightarrow> is_class G D \<and>  \<not>G\<turnstile>D\<preceq>C C \<and>
oheimb@11026
    45
                   (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
oheimb@11026
    46
                      method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
nipkow@8011
    47
kleing@12951
    48
 wf_syscls :: "'c prog => bool"
kleing@12951
    49
"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
kleing@12951
    50
kleing@10061
    51
 wf_prog :: "'c wf_mb => 'c prog => bool"
kleing@12951
    52
"wf_prog wf_mb G == 
kleing@12951
    53
   let cs = set G in wf_syscls G \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
oheimb@11026
    54
oheimb@11026
    55
lemma class_wf: 
oheimb@11026
    56
 "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
oheimb@11026
    57
apply (unfold wf_prog_def class_def)
oheimb@11026
    58
apply (simp)
oheimb@11026
    59
apply (fast dest: map_of_SomeD)
oheimb@11026
    60
done
oheimb@11026
    61
oheimb@11026
    62
lemma class_Object [simp]: 
kleing@12951
    63
  "wf_prog wf_mb G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
kleing@12951
    64
apply (unfold wf_prog_def wf_syscls_def class_def)
kleing@12951
    65
apply (auto simp: map_of_SomeI)
oheimb@11026
    66
done
oheimb@11026
    67
oheimb@11026
    68
lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
oheimb@11026
    69
apply (unfold is_class_def)
oheimb@11026
    70
apply (simp (no_asm_simp))
oheimb@11026
    71
done
oheimb@11026
    72
kleing@13051
    73
lemma is_class_xcpt [simp]: "wf_prog wf_mb G \<Longrightarrow> is_class G (Xcpt x)"
kleing@13051
    74
  apply (simp add: wf_prog_def wf_syscls_def)
kleing@13051
    75
  apply (simp add: is_class_def class_def)
kleing@13051
    76
  apply clarify
kleing@13051
    77
  apply (erule_tac x = x in allE)
kleing@13051
    78
  apply clarify
kleing@13051
    79
  apply (auto intro!: map_of_SomeI)
kleing@13051
    80
  done
kleing@13051
    81
oheimb@11026
    82
lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
oheimb@11026
    83
apply( frule r_into_trancl)
oheimb@11026
    84
apply( drule subcls1D)
oheimb@11026
    85
apply(clarify)
oheimb@11026
    86
apply( drule (1) class_wf)
oheimb@11026
    87
apply( unfold wf_cdecl_def)
oheimb@11026
    88
apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
oheimb@11026
    89
done
oheimb@11026
    90
oheimb@11026
    91
lemma wf_cdecl_supD: 
oheimb@11026
    92
"!!r. \<lbrakk>wf_cdecl wf_mb G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
oheimb@11026
    93
apply (unfold wf_cdecl_def)
oheimb@11026
    94
apply (auto split add: option.split_asm)
oheimb@11026
    95
done
oheimb@11026
    96
oheimb@11026
    97
lemma subcls_asym: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
oheimb@11026
    98
apply(erule tranclE)
oheimb@11026
    99
apply(fast dest!: subcls1_wfD )
oheimb@11026
   100
apply(fast dest!: subcls1_wfD intro: trancl_trans)
oheimb@11026
   101
done
oheimb@11026
   102
oheimb@11026
   103
lemma subcls_irrefl: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
oheimb@11026
   104
apply (erule trancl_trans_induct)
oheimb@11026
   105
apply  (auto dest: subcls1_wfD subcls_asym)
oheimb@11026
   106
done
oheimb@11026
   107
oheimb@11026
   108
lemma acyclic_subcls1: "wf_prog wf_mb G ==> acyclic (subcls1 G)"
oheimb@11026
   109
apply (unfold acyclic_def)
oheimb@11026
   110
apply (fast dest: subcls_irrefl)
oheimb@11026
   111
done
oheimb@11026
   112
oheimb@11026
   113
lemma wf_subcls1: "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)"
oheimb@11026
   114
apply (rule finite_acyclic_wf)
oheimb@11026
   115
apply ( subst finite_converse)
oheimb@11026
   116
apply ( rule finite_subcls1)
oheimb@11026
   117
apply (subst acyclic_converse)
oheimb@11026
   118
apply (erule acyclic_subcls1)
oheimb@11026
   119
done
oheimb@11026
   120
oheimb@11026
   121
lemma subcls_induct: 
oheimb@11026
   122
"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
oheimb@11026
   123
(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
oheimb@11026
   124
proof -
oheimb@11026
   125
  assume p: "PROP ?P"
oheimb@11026
   126
  assume ?A thus ?thesis apply -
oheimb@11026
   127
apply(drule wf_subcls1)
oheimb@11026
   128
apply(drule wf_trancl)
oheimb@11026
   129
apply(simp only: trancl_converse)
oheimb@11026
   130
apply(erule_tac a = C in wf_induct)
oheimb@11026
   131
apply(rule p)
oheimb@11026
   132
apply(auto)
oheimb@11026
   133
done
oheimb@11026
   134
qed
oheimb@11026
   135
oheimb@11026
   136
lemma subcls1_induct:
oheimb@11026
   137
"[|is_class G C; wf_prog wf_mb G; P Object;  
oheimb@11026
   138
   !!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and>  
oheimb@11026
   139
    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 
oheimb@11026
   140
 |] ==> P C"
oheimb@11026
   141
(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
oheimb@11026
   142
proof -
oheimb@11026
   143
  assume p: "PROP ?P"
oheimb@11026
   144
  assume ?A ?B ?C thus ?thesis apply -
oheimb@11026
   145
apply(unfold is_class_def)
oheimb@11026
   146
apply( rule impE)
oheimb@11026
   147
prefer 2
oheimb@11026
   148
apply(   assumption)
oheimb@11026
   149
prefer 2
oheimb@11026
   150
apply(  assumption)
oheimb@11026
   151
apply( erule thin_rl)
oheimb@11026
   152
apply( rule subcls_induct)
oheimb@11026
   153
apply(  assumption)
oheimb@11026
   154
apply( rule impI)
oheimb@11026
   155
apply( case_tac "C = Object")
oheimb@11026
   156
apply(  fast)
oheimb@11026
   157
apply safe
oheimb@11026
   158
apply( frule (1) class_wf)
oheimb@11026
   159
apply( frule (1) wf_cdecl_supD)
oheimb@11026
   160
oheimb@11026
   161
apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
oheimb@11026
   162
apply( erule_tac [2] subcls1I)
oheimb@11026
   163
apply(  rule p)
oheimb@11026
   164
apply (unfold is_class_def)
oheimb@11026
   165
apply auto
oheimb@11026
   166
done
oheimb@11026
   167
qed
oheimb@11026
   168
oheimb@11026
   169
lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma];
oheimb@11026
   170
oheimb@11026
   171
lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
oheimb@11026
   172
kleing@12951
   173
lemma method_Object [simp]:
kleing@12951
   174
  "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> wf_prog wf_mb G \<Longrightarrow> D = Object"  
kleing@12951
   175
  apply (frule class_Object, clarify)
kleing@12951
   176
  apply (drule method_rec, assumption)
kleing@12951
   177
  apply (auto dest: map_of_SomeD)
kleing@12951
   178
  done
oheimb@11026
   179
oheimb@11026
   180
lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
oheimb@11026
   181
apply(erule subcls1_induct)
oheimb@11026
   182
apply(  assumption)
oheimb@11026
   183
apply( fast)
oheimb@11026
   184
apply(auto dest!: wf_cdecl_supD)
nipkow@12566
   185
apply(erule (1) converse_rtrancl_into_rtrancl)
oheimb@11026
   186
done
oheimb@11026
   187
oheimb@11026
   188
lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
oheimb@11026
   189
apply (unfold wf_mhead_def)
oheimb@11026
   190
apply auto
oheimb@11026
   191
done
oheimb@11026
   192
oheimb@11026
   193
lemma widen_fields_defpl': "[|is_class G C; wf_prog wf_mb G|] ==>  
oheimb@11026
   194
  \<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
oheimb@11026
   195
apply( erule subcls1_induct)
oheimb@11026
   196
apply(   assumption)
kleing@12951
   197
apply(  frule class_Object)
kleing@12951
   198
apply(  clarify)
kleing@12951
   199
apply(  frule fields_rec, assumption)
kleing@12951
   200
apply(  fastsimp)
oheimb@11026
   201
apply( tactic "safe_tac HOL_cs")
oheimb@11026
   202
apply( subst fields_rec)
oheimb@11026
   203
apply(   assumption)
oheimb@11026
   204
apply(  assumption)
oheimb@11026
   205
apply( simp (no_asm) split del: split_if)
oheimb@11026
   206
apply( rule ballI)
oheimb@11026
   207
apply( simp (no_asm_simp) only: split_tupled_all)
oheimb@11026
   208
apply( simp (no_asm))
oheimb@11026
   209
apply( erule UnE)
oheimb@11026
   210
apply(  force)
oheimb@11026
   211
apply( erule r_into_rtrancl [THEN rtrancl_trans])
oheimb@11026
   212
apply auto
oheimb@11026
   213
done
oheimb@11026
   214
kleing@12517
   215
lemma widen_fields_defpl: 
kleing@12517
   216
  "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>  
oheimb@11026
   217
  G\<turnstile>C\<preceq>C fd"
oheimb@11026
   218
apply( drule (1) widen_fields_defpl')
oheimb@11026
   219
apply (fast)
oheimb@11026
   220
done
oheimb@11026
   221
kleing@12517
   222
lemma unique_fields: 
kleing@12517
   223
  "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
oheimb@11026
   224
apply( erule subcls1_induct)
oheimb@11026
   225
apply(   assumption)
kleing@12951
   226
apply(  frule class_Object)
kleing@12951
   227
apply(  clarify)
kleing@12951
   228
apply(  frule fields_rec, assumption)
kleing@12951
   229
apply(  drule class_wf, assumption)
kleing@12951
   230
apply(  simp add: wf_cdecl_def)
kleing@12951
   231
apply(  rule unique_map_inj)
kleing@12951
   232
apply(   simp)
paulson@13585
   233
apply(  rule inj_onI)
kleing@12951
   234
apply(  simp)
kleing@12951
   235
apply( safe dest!: wf_cdecl_supD)
oheimb@11026
   236
apply( drule subcls1_wfD)
oheimb@11026
   237
apply(  assumption)
oheimb@11026
   238
apply( subst fields_rec)
oheimb@11026
   239
apply   auto
oheimb@11026
   240
apply( rotate_tac -1)
oheimb@11026
   241
apply( frule class_wf)
oheimb@11026
   242
apply  auto
oheimb@11026
   243
apply( simp add: wf_cdecl_def)
oheimb@11026
   244
apply( erule unique_append)
oheimb@11026
   245
apply(  rule unique_map_inj)
oheimb@11026
   246
apply(   clarsimp)
paulson@13585
   247
apply  (rule inj_onI)
oheimb@11026
   248
apply(  simp)
oheimb@11026
   249
apply(auto dest!: widen_fields_defpl)
oheimb@11026
   250
done
oheimb@11026
   251
kleing@12517
   252
lemma fields_mono_lemma [rule_format (no_asm)]: 
kleing@12517
   253
  "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>  
oheimb@11026
   254
  x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
oheimb@11026
   255
apply(erule converse_rtrancl_induct)
oheimb@11026
   256
apply( safe dest!: subcls1D)
oheimb@11026
   257
apply(subst fields_rec)
oheimb@11026
   258
apply(  auto)
oheimb@11026
   259
done
oheimb@11026
   260
oheimb@11026
   261
lemma fields_mono: 
oheimb@11026
   262
"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; wf_prog wf_mb G\<rbrakk> 
oheimb@11026
   263
  \<Longrightarrow> map_of (fields (G,D)) fn = Some f"
oheimb@11026
   264
apply (rule map_of_SomeI)
oheimb@11026
   265
apply  (erule (1) unique_fields)
oheimb@11026
   266
apply (erule (1) fields_mono_lemma)
oheimb@11026
   267
apply (erule map_of_SomeD)
oheimb@11026
   268
done
oheimb@11026
   269
oheimb@11026
   270
lemma widen_cfs_fields: 
oheimb@11026
   271
"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; wf_prog wf_mb G|]==>  
oheimb@11026
   272
  map_of (fields (G,D)) (fn, fd) = Some fT"
oheimb@11026
   273
apply (drule field_fields)
oheimb@11026
   274
apply (drule rtranclD)
oheimb@11026
   275
apply safe
oheimb@11026
   276
apply (frule subcls_is_class)
oheimb@11026
   277
apply (drule trancl_into_rtrancl)
oheimb@11026
   278
apply (fast dest: fields_mono)
oheimb@11026
   279
done
oheimb@11026
   280
kleing@12517
   281
lemma method_wf_mdecl [rule_format (no_asm)]: 
kleing@12517
   282
  "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   
oheimb@11026
   283
     method (G,C) sig = Some (md,mh,m) 
oheimb@11026
   284
   --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
oheimb@11026
   285
apply( erule subcls1_induct)
oheimb@11026
   286
apply(   assumption)
kleing@12951
   287
apply(  clarify) 
kleing@12951
   288
apply(  frule class_Object)
kleing@12951
   289
apply(  clarify)
kleing@12951
   290
apply(  frule method_rec, assumption)
kleing@12951
   291
apply(  drule class_wf, assumption)
kleing@12951
   292
apply(  simp add: wf_cdecl_def)
kleing@12951
   293
apply(  drule map_of_SomeD)
kleing@12951
   294
apply(  subgoal_tac "md = Object")
kleing@12951
   295
apply(   fastsimp)
kleing@12951
   296
apply(  fastsimp)
oheimb@11026
   297
apply( clarify)
oheimb@11026
   298
apply( frule_tac C = C in method_rec)
oheimb@11026
   299
apply(  assumption)
oheimb@11026
   300
apply( rotate_tac -1)
oheimb@11026
   301
apply( simp)
oheimb@11026
   302
apply( drule override_SomeD)
oheimb@11026
   303
apply( erule disjE)
oheimb@11026
   304
apply(  erule_tac V = "?P --> ?Q" in thin_rl)
oheimb@11026
   305
apply (frule map_of_SomeD)
oheimb@11026
   306
apply (clarsimp simp add: wf_cdecl_def)
oheimb@11026
   307
apply( clarify)
oheimb@11026
   308
apply( rule rtrancl_trans)
oheimb@11026
   309
prefer 2
oheimb@11026
   310
apply(  assumption)
oheimb@11026
   311
apply( rule r_into_rtrancl)
oheimb@11026
   312
apply( fast intro: subcls1I)
oheimb@11026
   313
done
oheimb@11026
   314
oheimb@11026
   315
lemma subcls_widen_methd [rule_format (no_asm)]: 
oheimb@11026
   316
  "[|G\<turnstile>T\<preceq>C T'; wf_prog wf_mb G|] ==>  
oheimb@11026
   317
   \<forall>D rT b. method (G,T') sig = Some (D,rT ,b) --> 
oheimb@11026
   318
  (\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \<and> G\<turnstile>rT'\<preceq>rT)"
oheimb@11026
   319
apply( drule rtranclD)
oheimb@11026
   320
apply( erule disjE)
oheimb@11026
   321
apply(  fast)
oheimb@11026
   322
apply( erule conjE)
oheimb@11026
   323
apply( erule trancl_trans_induct)
oheimb@11026
   324
prefer 2
oheimb@11026
   325
apply(  clarify)
oheimb@11026
   326
apply(  drule spec, drule spec, drule spec, erule (1) impE)
oheimb@11026
   327
apply(  fast elim: widen_trans)
oheimb@11026
   328
apply( clarify)
oheimb@11026
   329
apply( drule subcls1D)
oheimb@11026
   330
apply( clarify)
oheimb@11026
   331
apply( subst method_rec)
oheimb@11026
   332
apply(  assumption)
oheimb@11026
   333
apply( unfold override_def)
oheimb@11026
   334
apply( simp (no_asm_simp) del: split_paired_Ex)
oheimb@11026
   335
apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
oheimb@11026
   336
apply(  erule exE)
oheimb@11026
   337
apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
oheimb@11026
   338
prefer 2
oheimb@11026
   339
apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
oheimb@11026
   340
apply(  tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1")
oheimb@11026
   341
apply(  simp_all (no_asm_simp) del: split_paired_Ex)
oheimb@11026
   342
apply( drule (1) class_wf)
oheimb@11026
   343
apply( simp (no_asm_simp) only: split_tupled_all)
oheimb@11026
   344
apply( unfold wf_cdecl_def)
oheimb@11026
   345
apply( drule map_of_SomeD)
oheimb@11026
   346
apply auto
oheimb@11026
   347
done
oheimb@11026
   348
oheimb@11026
   349
lemma subtype_widen_methd: 
oheimb@11026
   350
 "[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;  
oheimb@11026
   351
     method (G,D) sig = Some (md, rT, b) |]  
oheimb@11026
   352
  ==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
kleing@12517
   353
apply(auto dest: subcls_widen_methd method_wf_mdecl 
kleing@12517
   354
           simp add: wf_mdecl_def wf_mhead_def split_def)
oheimb@11026
   355
done
oheimb@11026
   356
kleing@12517
   357
lemma method_in_md [rule_format (no_asm)]: 
kleing@12517
   358
  "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
kleing@12517
   359
  --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
oheimb@11026
   360
apply (erule (1) subcls1_induct)
kleing@12951
   361
 apply clarify
kleing@12951
   362
 apply (frule method_Object, assumption)
kleing@12951
   363
 apply hypsubst
kleing@12951
   364
 apply simp
oheimb@11026
   365
apply (erule conjE)
oheimb@11026
   366
apply (subst method_rec)
oheimb@11026
   367
  apply (assumption)
oheimb@11026
   368
 apply (assumption)
oheimb@11026
   369
apply (clarify)
oheimb@11026
   370
apply (erule_tac "x" = "Da" in allE)
oheimb@11026
   371
apply (clarsimp)
oheimb@11026
   372
 apply (simp add: map_of_map)
oheimb@11026
   373
 apply (clarify)
oheimb@11026
   374
 apply (subst method_rec)
oheimb@11026
   375
   apply (assumption)
oheimb@11026
   376
  apply (assumption)
oheimb@11026
   377
 apply (simp add: override_def map_of_map split add: option.split)
oheimb@11026
   378
done
oheimb@11026
   379
oheimb@11026
   380
lemma widen_methd: 
oheimb@11026
   381
"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\<turnstile>T''\<preceq>C C|] 
oheimb@11026
   382
  ==> \<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
oheimb@11026
   383
apply( drule subcls_widen_methd)
oheimb@11026
   384
apply   auto
oheimb@11026
   385
done
oheimb@11026
   386
oheimb@11026
   387
lemma Call_lemma: 
oheimb@11026
   388
"[|method (G,C) sig = Some (md,rT,b); G\<turnstile>T''\<preceq>C C; wf_prog wf_mb G;  
oheimb@11026
   389
  class G C = Some y|] ==> \<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \<and>  
oheimb@11026
   390
  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)"
oheimb@11026
   391
apply( drule (2) widen_methd)
oheimb@11026
   392
apply( clarify)
oheimb@11026
   393
apply( frule subcls_is_class2)
oheimb@11026
   394
apply (unfold is_class_def)
oheimb@11026
   395
apply (simp (no_asm_simp))
oheimb@11026
   396
apply( drule method_wf_mdecl)
oheimb@11026
   397
apply( unfold wf_mdecl_def)
oheimb@11026
   398
apply( unfold is_class_def)
oheimb@11026
   399
apply auto
oheimb@11026
   400
done
oheimb@11026
   401
oheimb@11026
   402
kleing@12517
   403
lemma fields_is_type_lemma [rule_format (no_asm)]: 
kleing@12517
   404
  "[|is_class G C; wf_prog wf_mb G|] ==>  
oheimb@11026
   405
  \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
oheimb@11026
   406
apply( erule (1) subcls1_induct)
kleing@12951
   407
apply(  frule class_Object)
kleing@12951
   408
apply(  clarify)
kleing@12951
   409
apply(  frule fields_rec, assumption)
kleing@12951
   410
apply(  drule class_wf, assumption)
kleing@12951
   411
apply(  simp add: wf_cdecl_def wf_fdecl_def)
kleing@12951
   412
apply(  fastsimp)
oheimb@11026
   413
apply( subst fields_rec)
oheimb@11026
   414
apply(   fast)
oheimb@11026
   415
apply(  assumption)
oheimb@11026
   416
apply( clarsimp)
oheimb@11026
   417
apply( safe)
oheimb@11026
   418
prefer 2
oheimb@11026
   419
apply(  force)
oheimb@11026
   420
apply( drule (1) class_wf)
oheimb@11026
   421
apply( unfold wf_cdecl_def)
oheimb@11026
   422
apply( clarsimp)
oheimb@11026
   423
apply( drule (1) bspec)
oheimb@11026
   424
apply( unfold wf_fdecl_def)
oheimb@11026
   425
apply auto
oheimb@11026
   426
done
oheimb@11026
   427
kleing@12517
   428
lemma fields_is_type: 
kleing@12517
   429
  "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>  
oheimb@11026
   430
  is_type G f"
oheimb@11026
   431
apply(drule map_of_SomeD)
oheimb@11026
   432
apply(drule (2) fields_is_type_lemma)
oheimb@11026
   433
apply(auto)
oheimb@11026
   434
done
oheimb@11026
   435
oheimb@11026
   436
lemma methd:
oheimb@11026
   437
  "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
oheimb@11026
   438
  ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
oheimb@11026
   439
proof -
kleing@12951
   440
  assume wf: "wf_prog wf_mb G" and C:  "(C,S,fs,mdecls) \<in> set G" and
kleing@12951
   441
         m: "(sig,rT,code) \<in> set mdecls"
oheimb@11026
   442
  moreover
kleing@12951
   443
  from wf C have "class G C = Some (S,fs,mdecls)"
oheimb@11026
   444
    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
kleing@12951
   445
  moreover
kleing@12951
   446
  from wf C 
kleing@12951
   447
  have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
kleing@12951
   448
  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)  
kleing@12951
   449
  with m 
kleing@12951
   450
  have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
kleing@12951
   451
    by (force intro: map_of_SomeI)
oheimb@11026
   452
  ultimately
kleing@12517
   453
  show ?thesis by (auto simp add: is_class_def dest: method_rec)
oheimb@11026
   454
qed
nipkow@8011
   455
kleing@12951
   456
kleing@12951
   457
lemma wf_mb'E:
kleing@12951
   458
  "\<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>
kleing@12951
   459
  \<Longrightarrow> wf_prog wf_mb' G"
kleing@12951
   460
  apply (simp add: wf_prog_def)
kleing@12951
   461
  apply auto
kleing@12951
   462
  apply (simp add: wf_cdecl_def wf_mdecl_def)
kleing@12951
   463
  apply safe
kleing@12951
   464
  apply (drule bspec, assumption) apply simp
kleing@12951
   465
  apply (drule bspec, assumption) apply simp
kleing@12951
   466
  apply (drule bspec, assumption) apply simp
kleing@12951
   467
  apply clarify apply (drule bspec, assumption) apply simp
kleing@12951
   468
  apply (drule bspec, assumption) apply simp
kleing@12951
   469
  apply (drule bspec, assumption) apply simp
kleing@12951
   470
  apply (drule bspec, assumption) apply simp
kleing@12951
   471
  apply (drule bspec, assumption) apply simp
kleing@12951
   472
  apply (drule bspec, assumption) apply simp
kleing@12951
   473
  apply clarify apply (drule bspec, assumption)+ apply simp
kleing@12951
   474
  done
kleing@12951
   475
kleing@12951
   476
kleing@12951
   477
lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast
kleing@12951
   478
kleing@12951
   479
lemma wf_syscls:
kleing@12951
   480
  "set SystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G"
kleing@12951
   481
  apply (drule fst_mono)
kleing@12951
   482
  apply (simp add: SystemClasses_def wf_syscls_def)
kleing@12951
   483
  apply (simp add: ObjectC_def) 
kleing@12951
   484
  apply (rule allI, case_tac x)
kleing@12951
   485
  apply (auto simp add: NullPointerC_def ClassCastC_def OutOfMemoryC_def)
kleing@12951
   486
  done
kleing@12951
   487
nipkow@8011
   488
end