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