src/HOL/Bali/Decl.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 63680 6e1e8b5abbfa
child 67443 3abf6a722518
permissions -rw-r--r--
proper merge (amending fb46c031c841);
wenzelm@12857
     1
(*  Title:      HOL/Bali/Decl.thy
schirmer@12925
     2
    Author:     David von Oheimb and Norbert Schirmer
schirmer@12854
     3
*)
wenzelm@62042
     4
subsection \<open>Field, method, interface, and class declarations, whole Java programs
wenzelm@62042
     5
\<close>
schirmer@12854
     6
haftmann@26566
     7
theory Decl
krauss@44013
     8
imports Term Table
krauss@44013
     9
  (** order is significant, because of clash for "var" **)
haftmann@26566
    10
begin
schirmer@12854
    11
wenzelm@62042
    12
text \<open>
schirmer@12854
    13
improvements:
schirmer@12854
    14
\begin{itemize}
schirmer@12854
    15
\item clarification and correction of some aspects of the package/access concept
schirmer@12854
    16
  (Also submitted as bug report to the Java Bug Database:
schirmer@12854
    17
   Bug Id: 4485402 and Bug Id: 4493343 
wenzelm@63680
    18
   \<^url>\<open>http://developer.java.sun.com/developer/bugParade/index.jshtml\<close>
schirmer@12854
    19
  )
schirmer@12854
    20
\end{itemize}
schirmer@12854
    21
simplifications:
schirmer@12854
    22
\begin{itemize}
schirmer@12854
    23
\item the only field and method modifiers are static and the access modifiers
schirmer@12854
    24
\item no constructors, which may be simulated by new + suitable methods
schirmer@12854
    25
\item there is just one global initializer per class, which can simulate all 
schirmer@12854
    26
      others
schirmer@12854
    27
schirmer@12854
    28
\item no throws clause
schirmer@12854
    29
\item a void method is replaced by one that returns Unit (of dummy type Void)
schirmer@12854
    30
schirmer@12854
    31
\item no interface fields
schirmer@12854
    32
schirmer@12854
    33
\item every class has an explicit superclass (unused for Object)
schirmer@12854
    34
\item the (standard) methods of Object and of standard exceptions are not 
schirmer@12854
    35
      specified
schirmer@12854
    36
schirmer@12854
    37
\item no main method
schirmer@12854
    38
\end{itemize}
wenzelm@62042
    39
\<close>
schirmer@12854
    40
wenzelm@62042
    41
subsection \<open>Modifier\<close>
schirmer@12854
    42
wenzelm@62042
    43
subsubsection \<open>Access modifier\<close>
schirmer@12854
    44
blanchet@58310
    45
datatype acc_modi (* access modifier *)
schirmer@12854
    46
         = Private | Package | Protected | Public 
schirmer@12854
    47
wenzelm@62042
    48
text \<open>
schirmer@12854
    49
We can define a linear order for the access modifiers. With Private yielding the
schirmer@12854
    50
most restrictive access and public the most liberal access policy:
schirmer@12854
    51
  Private < Package < Protected < Public
wenzelm@62042
    52
\<close>
schirmer@12854
    53
 
haftmann@26566
    54
instantiation acc_modi :: linorder
haftmann@26566
    55
begin
schirmer@12854
    56
haftmann@26566
    57
definition
haftmann@26566
    58
  less_acc_def: "a < b
haftmann@26566
    59
      \<longleftrightarrow> (case a of
schirmer@12854
    60
             Private    \<Rightarrow> (b=Package \<or> b=Protected \<or> b=Public)
schirmer@12854
    61
           | Package    \<Rightarrow> (b=Protected \<or> b=Public)
schirmer@12854
    62
           | Protected  \<Rightarrow> (b=Public)
schirmer@12854
    63
           | Public     \<Rightarrow> False)"
schirmer@12854
    64
haftmann@26566
    65
definition
haftmann@27682
    66
  le_acc_def: "(a :: acc_modi) \<le> b \<longleftrightarrow> a < b \<or> a = b"
haftmann@26566
    67
wenzelm@41525
    68
instance
wenzelm@41525
    69
proof
schirmer@12854
    70
  fix x y z::acc_modi
haftmann@27682
    71
  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
nipkow@63648
    72
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.split) 
wenzelm@62042
    73
  show "x \<le> x"                       \<comment> reflexivity
schirmer@12854
    74
    by (auto simp add: le_acc_def)
wenzelm@41525
    75
  {
wenzelm@62042
    76
    assume "x \<le> y" "y \<le> z"           \<comment> transitivity 
wenzelm@41525
    77
    then show "x \<le> z"
nipkow@63648
    78
      by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
schirmer@12854
    79
  next
wenzelm@62042
    80
    assume "x \<le> y" "y \<le> x"           \<comment> antisymmetry
wenzelm@41525
    81
    moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
nipkow@63648
    82
      by (auto simp add: less_acc_def split: acc_modi.split)
wenzelm@41525
    83
    ultimately show "x = y" by (unfold le_acc_def) iprover
schirmer@12854
    84
  next
wenzelm@41525
    85
    fix x y:: acc_modi
wenzelm@41525
    86
    show "x \<le> y \<or> y \<le> x"   
nipkow@63648
    87
      by (auto simp add: less_acc_def le_acc_def split: acc_modi.split)
haftmann@27682
    88
  }
schirmer@12854
    89
qed
haftmann@26566
    90
  
haftmann@26566
    91
end
schirmer@12854
    92
schirmer@12854
    93
lemma acc_modi_top [simp]: "Public \<le> a \<Longrightarrow> a = Public"
schirmer@12854
    94
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
    95
schirmer@12854
    96
lemma acc_modi_top1 [simp, intro!]: "a \<le> Public"
schirmer@12854
    97
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
    98
schirmer@12854
    99
lemma acc_modi_le_Public: 
schirmer@12854
   100
"a \<le> Public \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
schirmer@12854
   101
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
   102
schirmer@12854
   103
lemma acc_modi_bottom: "a \<le> Private \<Longrightarrow> a = Private"
schirmer@12854
   104
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
   105
schirmer@12854
   106
lemma acc_modi_Private_le: 
schirmer@12854
   107
"Private \<le> a \<Longrightarrow> a=Private \<or> a = Package \<or> a=Protected \<or> a=Public"
schirmer@12854
   108
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
   109
schirmer@12854
   110
lemma acc_modi_Package_le: 
schirmer@12854
   111
  "Package \<le> a \<Longrightarrow> a = Package \<or> a=Protected \<or> a=Public"
schirmer@12854
   112
by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)
schirmer@12854
   113
schirmer@12854
   114
lemma acc_modi_le_Package: 
schirmer@12854
   115
  "a \<le> Package \<Longrightarrow> a=Private \<or> a = Package"
schirmer@12854
   116
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
   117
schirmer@12854
   118
lemma acc_modi_Protected_le: 
schirmer@12854
   119
  "Protected \<le> a \<Longrightarrow> a=Protected \<or> a=Public"
schirmer@12854
   120
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
   121
schirmer@12854
   122
lemma acc_modi_le_Protected: 
schirmer@12854
   123
  "a \<le> Protected  \<Longrightarrow> a=Private \<or> a = Package \<or> a = Protected"
schirmer@12854
   124
by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
schirmer@12854
   125
schirmer@12854
   126
schirmer@12854
   127
lemmas acc_modi_le_Dests = acc_modi_top           acc_modi_le_Public
schirmer@12854
   128
                           acc_modi_Private_le    acc_modi_bottom
schirmer@12854
   129
                           acc_modi_Package_le    acc_modi_le_Package
schirmer@12854
   130
                           acc_modi_Protected_le  acc_modi_le_Protected
schirmer@12854
   131
wenzelm@47176
   132
lemma acc_modi_Package_le_cases:
wenzelm@47176
   133
  assumes "Package \<le> m"
wenzelm@47176
   134
  obtains (Package) "m = Package"
wenzelm@47176
   135
    | (Protected) "m = Protected"
wenzelm@47176
   136
    | (Public) "m = Public"
wenzelm@47176
   137
using assms by (auto dest: acc_modi_Package_le)
schirmer@12854
   138
schirmer@12854
   139
wenzelm@62042
   140
subsubsection \<open>Static Modifier\<close>
wenzelm@41778
   141
type_synonym stat_modi = bool (* modifier: static *)
schirmer@12854
   142
wenzelm@62042
   143
subsection \<open>Declaration (base "class" for member,interface and class
wenzelm@62042
   144
 declarations\<close>
schirmer@12854
   145
schirmer@12854
   146
record decl =
schirmer@12854
   147
        access :: acc_modi
schirmer@12854
   148
schirmer@12854
   149
translations
wenzelm@35431
   150
  (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
wenzelm@35431
   151
  (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
schirmer@12854
   152
wenzelm@62042
   153
subsection \<open>Member (field or method)\<close>
schirmer@12854
   154
record  member = decl +
schirmer@12854
   155
         static :: stat_modi
schirmer@12854
   156
schirmer@12854
   157
translations
wenzelm@35431
   158
  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
wenzelm@35431
   159
  (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
schirmer@12854
   160
wenzelm@62042
   161
subsection \<open>Field\<close>
schirmer@12854
   162
schirmer@12854
   163
record field = member +
schirmer@12854
   164
        type :: ty
schirmer@12854
   165
translations
wenzelm@35431
   166
  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
wenzelm@35431
   167
  (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
schirmer@12854
   168
wenzelm@41778
   169
type_synonym fdecl          (* field declaration, cf. 8.3 *)
wenzelm@32960
   170
        = "vname \<times> field"
schirmer@12854
   171
schirmer@12854
   172
schirmer@12854
   173
translations
wenzelm@35431
   174
  (type) "fdecl" <= (type) "vname \<times> field"
schirmer@12854
   175
wenzelm@62042
   176
subsection  \<open>Method\<close>
schirmer@12854
   177
schirmer@12854
   178
record mhead = member +     (* method head (excluding signature) *)
schirmer@12854
   179
        pars ::"vname list" (* parameter names *)
schirmer@12854
   180
        resT ::ty           (* result type *)
schirmer@12854
   181
schirmer@12854
   182
record mbody =                      (* method body *)
schirmer@12854
   183
        lcls::  "(vname \<times> ty) list" (* local variables *)
schirmer@12854
   184
        stmt:: stmt                 (* the body statement *)
schirmer@12854
   185
schirmer@12854
   186
record methd = mhead + (* method in a class *)
schirmer@12854
   187
        mbody::mbody
schirmer@12854
   188
wenzelm@41778
   189
type_synonym mdecl = "sig \<times> methd"  (* method declaration in a class *)
schirmer@12854
   190
schirmer@12854
   191
schirmer@12854
   192
translations
wenzelm@35431
   193
  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
schirmer@12854
   194
                      pars::vname list, resT::ty\<rparr>"
wenzelm@35431
   195
  (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool, 
schirmer@12854
   196
                      pars::vname list, resT::ty,\<dots>::'a\<rparr>"
wenzelm@35431
   197
  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
wenzelm@35431
   198
  (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"      
wenzelm@35431
   199
  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
schirmer@12854
   200
                      pars::vname list, resT::ty,mbody::mbody\<rparr>"
wenzelm@35431
   201
  (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool, 
schirmer@12854
   202
                      pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
wenzelm@35431
   203
  (type) "mdecl" <= (type) "sig \<times> methd"
schirmer@12854
   204
schirmer@12854
   205
wenzelm@37956
   206
definition
wenzelm@37956
   207
  mhead :: "methd \<Rightarrow> mhead"
wenzelm@37956
   208
  where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
schirmer@12854
   209
schirmer@12854
   210
lemma access_mhead [simp]:"access (mhead m) = access m"
schirmer@12854
   211
by (simp add: mhead_def)
schirmer@12854
   212
schirmer@12854
   213
lemma static_mhead [simp]:"static (mhead m) = static m"
schirmer@12854
   214
by (simp add: mhead_def)
schirmer@12854
   215
schirmer@12854
   216
lemma pars_mhead [simp]:"pars (mhead m) = pars m"
schirmer@12854
   217
by (simp add: mhead_def)
schirmer@12854
   218
schirmer@12854
   219
lemma resT_mhead [simp]:"resT (mhead m) = resT m"
schirmer@12854
   220
by (simp add: mhead_def)
schirmer@12854
   221
wenzelm@62042
   222
text \<open>To be able to talk uniformaly about field and method declarations we
schirmer@12854
   223
introduce the notion of a member declaration (e.g. useful to define 
wenzelm@62042
   224
accessiblity )\<close>
schirmer@12854
   225
blanchet@58310
   226
datatype memberdecl = fdecl fdecl | mdecl mdecl
schirmer@12854
   227
blanchet@58310
   228
datatype memberid = fid vname | mid sig
schirmer@12854
   229
haftmann@35315
   230
class has_memberid =
haftmann@35315
   231
  fixes memberid :: "'a \<Rightarrow> memberid"
schirmer@12854
   232
haftmann@35315
   233
instantiation memberdecl :: has_memberid
haftmann@35315
   234
begin
schirmer@12854
   235
haftmann@35315
   236
definition
schirmer@12854
   237
memberdecl_memberid_def:
wenzelm@37956
   238
  "memberid m = (case m of
schirmer@12854
   239
                    fdecl (vn,f)  \<Rightarrow> fid vn
schirmer@12854
   240
                  | mdecl (sig,m) \<Rightarrow> mid sig)"
schirmer@12854
   241
haftmann@35315
   242
instance ..
haftmann@35315
   243
haftmann@35315
   244
end
haftmann@35315
   245
schirmer@12854
   246
lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
schirmer@12854
   247
by (simp add: memberdecl_memberid_def)
schirmer@12854
   248
schirmer@12854
   249
lemma memberid_fdecl_simp1: "memberid (fdecl f) = fid (fst f)"
schirmer@12854
   250
by (cases f) (simp add: memberdecl_memberid_def)
schirmer@12854
   251
schirmer@12854
   252
lemma memberid_mdecl_simp[simp]: "memberid (mdecl (sig,m)) = mid sig"
schirmer@12854
   253
by (simp add: memberdecl_memberid_def)
schirmer@12854
   254
schirmer@12854
   255
lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
schirmer@12854
   256
by (cases m) (simp add: memberdecl_memberid_def)
schirmer@12854
   257
haftmann@37678
   258
instantiation prod :: (type, has_memberid) has_memberid
haftmann@35315
   259
begin
schirmer@12854
   260
haftmann@35315
   261
definition
schirmer@12854
   262
pair_memberid_def:
wenzelm@37956
   263
  "memberid p = memberid (snd p)"
schirmer@12854
   264
haftmann@35315
   265
instance ..
haftmann@35315
   266
haftmann@35315
   267
end
haftmann@35315
   268
schirmer@12854
   269
lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
schirmer@12854
   270
by (simp add: pair_memberid_def)
schirmer@12854
   271
schirmer@12854
   272
lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
schirmer@12854
   273
by (simp add: pair_memberid_def)
schirmer@12854
   274
wenzelm@37956
   275
definition
wenzelm@37956
   276
  is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
wenzelm@37956
   277
  where "is_field m = (\<exists> declC f. m=(declC,fdecl f))"
schirmer@12854
   278
  
schirmer@12854
   279
lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
schirmer@12854
   280
by (simp add: is_field_def)
schirmer@12854
   281
schirmer@12854
   282
lemma is_fieldI: "is_field (C,fdecl f)"
schirmer@12854
   283
by (simp add: is_field_def)
schirmer@12854
   284
wenzelm@37956
   285
definition
wenzelm@37956
   286
  is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
wenzelm@37956
   287
  where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))"
schirmer@12854
   288
  
schirmer@12854
   289
lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
schirmer@12854
   290
by (simp add: is_method_def)
schirmer@12854
   291
schirmer@12854
   292
lemma is_methodI: "is_method (C,mdecl m)"
schirmer@12854
   293
by (simp add: is_method_def)
schirmer@12854
   294
schirmer@12854
   295
wenzelm@62042
   296
subsection \<open>Interface\<close>
schirmer@12854
   297
schirmer@12854
   298
wenzelm@62042
   299
record  ibody = decl +  \<comment>\<open>interface body\<close>
wenzelm@62042
   300
          imethods :: "(sig \<times> mhead) list" \<comment>\<open>method heads\<close>
schirmer@12854
   301
wenzelm@62042
   302
record  iface = ibody + \<comment>\<open>interface\<close>
wenzelm@62042
   303
         isuperIfs:: "qtname list" \<comment>\<open>superinterface list\<close>
wenzelm@41778
   304
type_synonym
wenzelm@62042
   305
        idecl           \<comment>\<open>interface declaration, cf. 9.1\<close>
wenzelm@32960
   306
        = "qtname \<times> iface"
schirmer@12854
   307
schirmer@12854
   308
translations
wenzelm@35431
   309
  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
wenzelm@35431
   310
  (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
wenzelm@35431
   311
  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
schirmer@12854
   312
                      isuperIfs::qtname list\<rparr>"
wenzelm@35431
   313
  (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
schirmer@12854
   314
                      isuperIfs::qtname list,\<dots>::'a\<rparr>"
wenzelm@35431
   315
  (type) "idecl" <= (type) "qtname \<times> iface"
schirmer@12854
   316
wenzelm@37956
   317
definition
wenzelm@37956
   318
  ibody :: "iface \<Rightarrow> ibody"
wenzelm@37956
   319
  where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>"
schirmer@12854
   320
schirmer@12854
   321
lemma access_ibody [simp]: "(access (ibody i)) = access i"
schirmer@12854
   322
by (simp add: ibody_def)
schirmer@12854
   323
schirmer@12854
   324
lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i"
schirmer@12854
   325
by (simp add: ibody_def)
schirmer@12854
   326
wenzelm@62042
   327
subsection  \<open>Class\<close>
wenzelm@62042
   328
record cbody = decl +          \<comment>\<open>class body\<close>
schirmer@12854
   329
         cfields:: "fdecl list" 
schirmer@12854
   330
         methods:: "mdecl list"
wenzelm@62042
   331
         init   :: "stmt"       \<comment>\<open>initializer\<close>
schirmer@12854
   332
wenzelm@62042
   333
record "class" = cbody +           \<comment>\<open>class\<close>
wenzelm@62042
   334
        super   :: "qtname"      \<comment>\<open>superclass\<close>
wenzelm@62042
   335
        superIfs:: "qtname list" \<comment>\<open>implemented interfaces\<close>
wenzelm@41778
   336
type_synonym
wenzelm@62042
   337
        cdecl           \<comment>\<open>class declaration, cf. 8.1\<close>
wenzelm@32960
   338
        = "qtname \<times> class"
schirmer@12854
   339
schirmer@12854
   340
translations
wenzelm@35431
   341
  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
schirmer@12854
   342
                      methods::mdecl list,init::stmt\<rparr>"
wenzelm@35431
   343
  (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
schirmer@12854
   344
                      methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
wenzelm@35431
   345
  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
schirmer@12854
   346
                      methods::mdecl list,init::stmt,
schirmer@12854
   347
                      super::qtname,superIfs::qtname list\<rparr>"
wenzelm@35431
   348
  (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
schirmer@12854
   349
                      methods::mdecl list,init::stmt,
schirmer@12854
   350
                      super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
wenzelm@35431
   351
  (type) "cdecl" <= (type) "qtname \<times> class"
schirmer@12854
   352
wenzelm@37956
   353
definition
wenzelm@37956
   354
  cbody :: "class \<Rightarrow> cbody"
wenzelm@37956
   355
  where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
schirmer@12854
   356
schirmer@12854
   357
lemma access_cbody [simp]:"access (cbody c) = access c"
schirmer@12854
   358
by (simp add: cbody_def)
schirmer@12854
   359
schirmer@12854
   360
lemma cfields_cbody [simp]:"cfields (cbody c) = cfields c"
schirmer@12854
   361
by (simp add: cbody_def)
schirmer@12854
   362
schirmer@12854
   363
lemma methods_cbody [simp]:"methods (cbody c) = methods c"
schirmer@12854
   364
by (simp add: cbody_def)
schirmer@12854
   365
schirmer@12854
   366
lemma init_cbody [simp]:"init (cbody c) = init c"
schirmer@12854
   367
by (simp add: cbody_def)
schirmer@12854
   368
schirmer@12854
   369
wenzelm@58887
   370
subsubsection "standard classes"
schirmer@12854
   371
schirmer@12854
   372
consts
wenzelm@62042
   373
  Object_mdecls  ::  "mdecl list" \<comment>\<open>methods of Object\<close>
wenzelm@62042
   374
  SXcpt_mdecls   ::  "mdecl list" \<comment>\<open>methods of SXcpts\<close>
schirmer@12854
   375
wenzelm@37956
   376
definition
wenzelm@62042
   377
  ObjectC ::         "cdecl"      \<comment>\<open>declaration  of root      class\<close> where
wenzelm@37956
   378
  "ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
wenzelm@37956
   379
                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
schirmer@12854
   380
wenzelm@37956
   381
definition
wenzelm@62042
   382
  SXcptC  ::"xname \<Rightarrow> cdecl"      \<comment>\<open>declarations of throwable classes\<close> where
wenzelm@37956
   383
  "SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
schirmer@12854
   384
                                   init=Skip,
schirmer@12854
   385
                                   super=if xn = Throwable then Object 
schirmer@12854
   386
                                                           else SXcpt Throwable,
schirmer@12854
   387
                                   superIfs=[]\<rparr>)"
schirmer@12854
   388
schirmer@12854
   389
lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn"
schirmer@12854
   390
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)
schirmer@12854
   391
schirmer@12854
   392
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
nipkow@17778
   393
by (simp add: SXcptC_def)
schirmer@12854
   394
wenzelm@37956
   395
definition
wenzelm@37956
   396
  standard_classes :: "cdecl list" where
wenzelm@37956
   397
  "standard_classes = [ObjectC, SXcptC Throwable,
wenzelm@32960
   398
                SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
wenzelm@32960
   399
                SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
schirmer@12854
   400
schirmer@12854
   401
wenzelm@58887
   402
subsubsection "programs"
schirmer@12854
   403
schirmer@12854
   404
record prog =
schirmer@12854
   405
        ifaces ::"idecl list"
schirmer@12854
   406
        "classes"::"cdecl list"
schirmer@12854
   407
schirmer@12854
   408
translations
wenzelm@35431
   409
     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
wenzelm@35431
   410
     (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
schirmer@12854
   411
wenzelm@35067
   412
abbreviation
wenzelm@35067
   413
  iface :: "prog  \<Rightarrow> (qtname, iface) table"
wenzelm@35067
   414
  where "iface G I == table_of (ifaces G) I"
wenzelm@35067
   415
wenzelm@35067
   416
abbreviation
wenzelm@35067
   417
  "class" :: "prog  \<Rightarrow> (qtname, class) table"
wenzelm@35067
   418
  where "class G C == table_of (classes G) C"
schirmer@12854
   419
wenzelm@35067
   420
abbreviation
wenzelm@35067
   421
  is_iface :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
wenzelm@35067
   422
  where "is_iface G I == iface G I \<noteq> None"
wenzelm@35067
   423
wenzelm@35067
   424
abbreviation
wenzelm@35067
   425
  is_class :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
wenzelm@35067
   426
  where "is_class G C == class G C \<noteq> None"
schirmer@12854
   427
schirmer@12854
   428
wenzelm@58887
   429
subsubsection "is type"
schirmer@12854
   430
wenzelm@37956
   431
primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
wenzelm@37956
   432
  and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
wenzelm@37956
   433
where
wenzelm@37956
   434
  "is_type G (PrimT pt)  = True"
wenzelm@37956
   435
| "is_type G (RefT  rt)  = isrtype G rt"
wenzelm@37956
   436
| "isrtype G (NullT) = True"
wenzelm@37956
   437
| "isrtype G (IfaceT tn) = is_iface G tn"
wenzelm@37956
   438
| "isrtype G (ClassT tn) = is_class G tn"
wenzelm@37956
   439
| "isrtype G (ArrayT T ) = is_type  G T"
schirmer@12854
   440
schirmer@12854
   441
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
schirmer@12854
   442
by auto
schirmer@12854
   443
schirmer@12854
   444
lemma type_is_class: "is_type G (Class C) \<Longrightarrow>  is_class G C"
schirmer@12854
   445
by auto
schirmer@12854
   446
schirmer@12854
   447
wenzelm@58887
   448
subsubsection "subinterface and subclass relation, in anticipation of TypeRel.thy"
schirmer@12854
   449
wenzelm@37956
   450
definition
wenzelm@62042
   451
  subint1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment>\<open>direct subinterface\<close>
wenzelm@37956
   452
  where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
schirmer@12854
   453
wenzelm@37956
   454
definition
wenzelm@62042
   455
  subcls1  :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment>\<open>direct subclass\<close>
wenzelm@37956
   456
  where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
schirmer@12854
   457
wenzelm@35067
   458
abbreviation
wenzelm@61989
   459
  subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>\<^sub>C1_"  [71,71,71] 70)
wenzelm@61989
   460
  where "G\<turnstile>C \<prec>\<^sub>C1 D == (C,D) \<in> subcls1 G"
wenzelm@35067
   461
wenzelm@35067
   462
abbreviation
wenzelm@61989
   463
  subclseq_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70) 
wenzelm@61989
   464
  where "G\<turnstile>C \<preceq>\<^sub>C D == (C,D) \<in>(subcls1 G)^*" (* cf. 8.1.3 *)
schirmer@12854
   465
wenzelm@35067
   466
abbreviation
wenzelm@61989
   467
  subcls_syntax :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
wenzelm@61989
   468
  where "G\<turnstile>C \<prec>\<^sub>C D == (C,D) \<in>(subcls1 G)^+"
schirmer@12854
   469
wenzelm@61989
   470
notation (ASCII)
wenzelm@61989
   471
  subcls1_syntax  ("_|-_<:C1_" [71,71,71] 70) and
wenzelm@61989
   472
  subclseq_syntax  ("_|-_<=:C _"[71,71,71] 70) and
wenzelm@61989
   473
  subcls_syntax  ("_|-_<:C _"[71,71,71] 70)
schirmer@12854
   474
schirmer@12854
   475
lemma subint1I: "\<lbrakk>iface G I = Some i; J \<in> set (isuperIfs i)\<rbrakk> 
schirmer@12854
   476
                 \<Longrightarrow> (I,J) \<in> subint1 G" 
schirmer@12854
   477
apply (simp add: subint1_def)
schirmer@12854
   478
done
schirmer@12854
   479
schirmer@12854
   480
lemma subcls1I:"\<lbrakk>class G C = Some c; C \<noteq> Object\<rbrakk> \<Longrightarrow> (C,(super c)) \<in> subcls1 G"
schirmer@12854
   481
apply (simp add: subcls1_def)
schirmer@12854
   482
done
schirmer@12854
   483
schirmer@12854
   484
schirmer@12854
   485
lemma subint1D: "(I,J)\<in>subint1 G\<Longrightarrow> \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)"
schirmer@12854
   486
by (simp add: subint1_def)
schirmer@12854
   487
schirmer@12854
   488
lemma subcls1D: 
schirmer@12854
   489
  "(C,D)\<in>subcls1 G \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c. class G C = Some c \<and> (super c = D))"
schirmer@12854
   490
apply (simp add: subcls1_def)
schirmer@12854
   491
apply auto
schirmer@12854
   492
done
schirmer@12854
   493
schirmer@12854
   494
lemma subint1_def2:  
paulson@14952
   495
  "subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))"
schirmer@12854
   496
apply (unfold subint1_def)
schirmer@12854
   497
apply auto
schirmer@12854
   498
done
schirmer@12854
   499
schirmer@12854
   500
lemma subcls1_def2: 
paulson@14952
   501
  "subcls1 G = 
paulson@14952
   502
     (SIGMA C: {C. is_class G C}. {D. C\<noteq>Object \<and> super (the(class G C))=D})"
schirmer@12854
   503
apply (unfold subcls1_def)
schirmer@12854
   504
apply auto
schirmer@12854
   505
done
schirmer@12854
   506
schirmer@12854
   507
lemma subcls_is_class:
schirmer@12854
   508
"\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D\<rbrakk> \<Longrightarrow> \<exists> c. class G C = Some c"
schirmer@12854
   509
by (auto simp add: subcls1_def dest: tranclD)
schirmer@12854
   510
haftmann@35416
   511
lemma no_subcls1_Object:"G\<turnstile>Object\<prec>\<^sub>C1 D \<Longrightarrow> P"
schirmer@12854
   512
by (auto simp add: subcls1_def)
schirmer@12854
   513
schirmer@12854
   514
lemma no_subcls_Object: "G\<turnstile>Object\<prec>\<^sub>C D \<Longrightarrow> P"
schirmer@12854
   515
apply (erule trancl_induct)
schirmer@12854
   516
apply (auto intro: no_subcls1_Object)
schirmer@12854
   517
done
schirmer@12854
   518
wenzelm@58887
   519
subsubsection "well-structured programs"
schirmer@12854
   520
wenzelm@37956
   521
definition
wenzelm@37956
   522
  ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
wenzelm@37956
   523
  where "ws_idecl G I si = (\<forall>J\<in>set si.  is_iface G J   \<and> (J,I)\<notin>(subint1 G)^+)"
schirmer@12854
   524
  
wenzelm@37956
   525
definition
wenzelm@37956
   526
  ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
wenzelm@37956
   527
  where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)"
schirmer@12854
   528
  
wenzelm@37956
   529
definition
wenzelm@37956
   530
  ws_prog  :: "prog \<Rightarrow> bool" where
wenzelm@37956
   531
  "ws_prog G = ((\<forall>(I,i)\<in>set (ifaces  G). ws_idecl G I (isuperIfs i)) \<and> 
wenzelm@37956
   532
                 (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c)))"
schirmer@12854
   533
schirmer@12854
   534
schirmer@12854
   535
lemma ws_progI: 
schirmer@12854
   536
"\<lbrakk>\<forall>(I,i)\<in>set (ifaces G). \<forall>J\<in>set (isuperIfs i). is_iface G J \<and> 
schirmer@12854
   537
                                                (J,I) \<notin> (subint1 G)^+; 
schirmer@12854
   538
  \<forall>(C,c)\<in>set (classes G). C\<noteq>Object \<longrightarrow> is_class G (super c) \<and> 
schirmer@12854
   539
                                        ((super c),C) \<notin> (subcls1 G)^+  
schirmer@12854
   540
 \<rbrakk> \<Longrightarrow> ws_prog G"
schirmer@12854
   541
apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def)
schirmer@12854
   542
apply (erule_tac conjI)
schirmer@12854
   543
apply blast
schirmer@12854
   544
done
schirmer@12854
   545
schirmer@12854
   546
lemma ws_prog_ideclD: 
schirmer@12854
   547
"\<lbrakk>iface G I = Some i; J\<in>set (isuperIfs i); ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
   548
  is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
schirmer@12854
   549
apply (unfold ws_prog_def ws_idecl_def)
schirmer@12854
   550
apply clarify
schirmer@12854
   551
apply (drule_tac map_of_SomeD)
schirmer@12854
   552
apply auto
schirmer@12854
   553
done
schirmer@12854
   554
schirmer@12854
   555
lemma ws_prog_cdeclD: 
schirmer@12854
   556
"\<lbrakk>class G C = Some c; C\<noteq>Object; ws_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12854
   557
  is_class G (super c) \<and> (super c,C)\<notin>(subcls1 G)^+"
schirmer@12854
   558
apply (unfold ws_prog_def ws_cdecl_def)
schirmer@12854
   559
apply clarify
schirmer@12854
   560
apply (drule_tac map_of_SomeD)
schirmer@12854
   561
apply auto
schirmer@12854
   562
done
schirmer@12854
   563
schirmer@12854
   564
wenzelm@58887
   565
subsubsection "well-foundedness"
schirmer@12854
   566
schirmer@12854
   567
lemma finite_is_iface: "finite {I. is_iface G I}"
schirmer@12854
   568
apply (fold dom_def)
schirmer@12854
   569
apply (rule_tac finite_dom_map_of)
schirmer@12854
   570
done
schirmer@12854
   571
schirmer@12854
   572
lemma finite_is_class: "finite {C. is_class G C}"
schirmer@12854
   573
apply (fold dom_def)
schirmer@12854
   574
apply (rule_tac finite_dom_map_of)
schirmer@12854
   575
done
schirmer@12854
   576
schirmer@12854
   577
lemma finite_subint1: "finite (subint1 G)"
schirmer@12854
   578
apply (subst subint1_def2)
schirmer@12854
   579
apply (rule finite_SigmaI)
schirmer@12854
   580
apply (rule finite_is_iface)
schirmer@12854
   581
apply (simp (no_asm))
schirmer@12854
   582
done
schirmer@12854
   583
schirmer@12854
   584
lemma finite_subcls1: "finite (subcls1 G)"
schirmer@12854
   585
apply (subst subcls1_def2)
schirmer@12854
   586
apply (rule finite_SigmaI)
schirmer@12854
   587
apply (rule finite_is_class)
schirmer@12854
   588
apply (rule_tac B = "{super (the (class G C))}" in finite_subset)
schirmer@12854
   589
apply  auto
schirmer@12854
   590
done
schirmer@12854
   591
schirmer@12854
   592
lemma subint1_irrefl_lemma1: 
schirmer@12854
   593
  "ws_prog G \<Longrightarrow> (subint1 G)^-1 \<inter> (subint1 G)^+ = {}"
schirmer@12854
   594
apply (force dest: subint1D ws_prog_ideclD conjunct2)
schirmer@12854
   595
done
schirmer@12854
   596
schirmer@12854
   597
lemma subcls1_irrefl_lemma1: 
schirmer@12854
   598
  "ws_prog G \<Longrightarrow> (subcls1 G)^-1 \<inter> (subcls1 G)^+ = {}"
schirmer@12854
   599
apply (force dest: subcls1D ws_prog_cdeclD conjunct2)
schirmer@12854
   600
done
schirmer@12854
   601
schirmer@12854
   602
lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI']
schirmer@12854
   603
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
schirmer@12854
   604
schirmer@12854
   605
lemma subint1_irrefl: "\<lbrakk>(x, y) \<in> subint1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
schirmer@12854
   606
apply (rule irrefl_trancl_rD)
schirmer@12854
   607
apply (rule subint1_irrefl_lemma2)
schirmer@12854
   608
apply auto
schirmer@12854
   609
done
schirmer@12854
   610
schirmer@12854
   611
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1 G; ws_prog G\<rbrakk> \<Longrightarrow> x \<noteq> y"
schirmer@12854
   612
apply (rule irrefl_trancl_rD)
schirmer@12854
   613
apply (rule subcls1_irrefl_lemma2)
schirmer@12854
   614
apply auto
schirmer@12854
   615
done
schirmer@12854
   616
wenzelm@45605
   617
lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI]
wenzelm@45605
   618
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI]
schirmer@12854
   619
schirmer@12854
   620
schirmer@12854
   621
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
schirmer@12854
   622
by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic)
schirmer@12854
   623
schirmer@12854
   624
lemma wf_subcls1: "ws_prog G \<Longrightarrow> wf ((subcls1 G)\<inverse>)"
schirmer@12854
   625
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
schirmer@12854
   626
schirmer@12854
   627
schirmer@12854
   628
lemma subint1_induct: 
schirmer@12854
   629
  "\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subint1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
schirmer@12854
   630
apply (frule wf_subint1)
schirmer@12854
   631
apply (erule wf_induct)
schirmer@12854
   632
apply (simp (no_asm_use) only: converse_iff)
schirmer@12854
   633
apply blast
schirmer@12854
   634
done
schirmer@12854
   635
schirmer@12854
   636
lemma subcls1_induct [consumes 1]:
schirmer@12854
   637
  "\<lbrakk>ws_prog G; \<And>x. \<forall>y. (x, y) \<in> subcls1 G \<longrightarrow> P y \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P a"
schirmer@12854
   638
apply (frule wf_subcls1)
schirmer@12854
   639
apply (erule wf_induct)
schirmer@12854
   640
apply (simp (no_asm_use) only: converse_iff)
schirmer@12854
   641
apply blast
schirmer@12854
   642
done
schirmer@12854
   643
schirmer@12854
   644
lemma ws_subint1_induct: 
schirmer@12854
   645
 "\<lbrakk>is_iface G I; ws_prog G; \<And>I i. \<lbrakk>iface G I = Some i \<and> 
schirmer@12854
   646
   (\<forall>J \<in> set (isuperIfs i). (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J)\<rbrakk> \<Longrightarrow> P I
schirmer@12854
   647
  \<rbrakk> \<Longrightarrow> P I"
wenzelm@24038
   648
apply (erule rev_mp)
schirmer@12854
   649
apply (rule subint1_induct)
schirmer@12854
   650
apply  assumption
paulson@18447
   651
apply (simp (no_asm)) 
schirmer@12854
   652
apply safe
paulson@18447
   653
apply (blast dest: subint1I ws_prog_ideclD)
schirmer@12854
   654
done
schirmer@12854
   655
schirmer@12854
   656
schirmer@12854
   657
lemma ws_subcls1_induct: "\<lbrakk>is_class G C; ws_prog G;  
schirmer@12854
   658
  \<And>C c. \<lbrakk>class G C = Some c;  
schirmer@12854
   659
 (C \<noteq> Object \<longrightarrow> (C,(super c))\<in>subcls1 G \<and> 
schirmer@12854
   660
                  P (super c) \<and> is_class G (super c))\<rbrakk> \<Longrightarrow> P C
schirmer@12854
   661
 \<rbrakk> \<Longrightarrow> P C"
wenzelm@24038
   662
apply (erule rev_mp)
schirmer@12854
   663
apply (rule subcls1_induct)
schirmer@12854
   664
apply  assumption
paulson@18447
   665
apply (simp (no_asm)) 
schirmer@12854
   666
apply safe
schirmer@12854
   667
apply (fast dest: subcls1I ws_prog_cdeclD)
schirmer@12854
   668
done
schirmer@12854
   669
schirmer@12854
   670
lemma ws_class_induct [consumes 2, case_names Object Subcls]:
schirmer@12854
   671
"\<lbrakk>class G C = Some c; ws_prog G; 
schirmer@12854
   672
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
schirmer@12854
   673
  \<And>  C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
schirmer@12854
   674
 \<rbrakk> \<Longrightarrow> P C"
schirmer@12854
   675
proof -
schirmer@12854
   676
  assume clsC: "class G C = Some c"
schirmer@12854
   677
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object"
schirmer@12854
   678
  and    step: "\<And>   C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C"
schirmer@12854
   679
  assume ws: "ws_prog G"
schirmer@12854
   680
  then have "is_class G C \<Longrightarrow> P C"  
schirmer@12854
   681
  proof (induct rule: subcls1_induct)
schirmer@12854
   682
    fix C
haftmann@35416
   683
    assume   hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C1 S \<longrightarrow> is_class G S \<longrightarrow> P S"
schirmer@12854
   684
       and iscls:"is_class G C"
schirmer@12854
   685
    show "P C"
schirmer@12854
   686
    proof (cases "C=Object")
schirmer@12854
   687
      case True with iscls init show "P C" by auto
schirmer@12854
   688
    next
schirmer@12854
   689
      case False with ws step hyp iscls 
nipkow@18576
   690
      show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
schirmer@12854
   691
    qed
schirmer@12854
   692
  qed
schirmer@12854
   693
  with clsC show ?thesis by simp
schirmer@12854
   694
qed
schirmer@12854
   695
schirmer@12854
   696
lemma ws_class_induct' [consumes 2, case_names Object Subcls]:
schirmer@12854
   697
"\<lbrakk>is_class G C; ws_prog G; 
schirmer@12854
   698
  \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
schirmer@12854
   699
  \<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
schirmer@12854
   700
 \<rbrakk> \<Longrightarrow> P C"
paulson@18447
   701
by (auto intro: ws_class_induct)
schirmer@12854
   702
schirmer@12854
   703
lemma ws_class_induct'' [consumes 2, case_names Object Subcls]:
schirmer@12854
   704
"\<lbrakk>class G C = Some c; ws_prog G; 
schirmer@12854
   705
  \<And> co. class G Object = Some co \<Longrightarrow> P Object co; 
schirmer@12854
   706
  \<And>  C c sc. \<lbrakk>class G C = Some c; class G (super c) = Some sc;
schirmer@12854
   707
            C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c
schirmer@12854
   708
 \<rbrakk> \<Longrightarrow> P C c"
schirmer@12854
   709
proof -
schirmer@12854
   710
  assume clsC: "class G C = Some c"
schirmer@12854
   711
  and    init: "\<And> co. class G Object = Some co \<Longrightarrow> P Object co"
schirmer@12854
   712
  and    step: "\<And> C c sc . \<lbrakk>class G C = Some c; class G (super c) = Some sc;
schirmer@12854
   713
                             C \<noteq> Object; P (super c) sc\<rbrakk> \<Longrightarrow> P C c"
schirmer@12854
   714
  assume ws: "ws_prog G"
schirmer@12854
   715
  then have "\<And> c. class G C = Some c\<Longrightarrow> P C c"  
schirmer@12854
   716
  proof (induct rule: subcls1_induct)
schirmer@12854
   717
    fix C c
haftmann@35416
   718
    assume   hyp:"\<forall> S. G\<turnstile>C \<prec>\<^sub>C1 S \<longrightarrow> (\<forall> s. class G S = Some s \<longrightarrow> P S s)"
schirmer@12854
   719
       and iscls:"class G C = Some c"
schirmer@12854
   720
    show "P C c"
schirmer@12854
   721
    proof (cases "C=Object")
schirmer@12854
   722
      case True with iscls init show "P C c" by auto
schirmer@12854
   723
    next
schirmer@12854
   724
      case False
schirmer@12854
   725
      with ws iscls obtain sc where
wenzelm@32960
   726
        sc: "class G (super c) = Some sc"
wenzelm@32960
   727
        by (auto dest: ws_prog_cdeclD)
haftmann@35416
   728
      from iscls False have "G\<turnstile>C \<prec>\<^sub>C1 (super c)" by (rule subcls1I)
schirmer@12854
   729
      with False ws step hyp iscls sc
schirmer@12854
   730
      show "P C c" 
wenzelm@32960
   731
        by (auto)  
schirmer@12854
   732
    qed
schirmer@12854
   733
  qed
schirmer@12854
   734
  with clsC show "P C c" by auto
schirmer@12854
   735
qed
schirmer@12854
   736
schirmer@12854
   737
lemma ws_interface_induct [consumes 2, case_names Step]:
wenzelm@12937
   738
  assumes is_if_I: "is_iface G I" and 
schirmer@12854
   739
               ws: "ws_prog G" and
schirmer@12854
   740
          hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 
schirmer@12854
   741
                            \<forall> J \<in> set (isuperIfs i).
schirmer@12854
   742
                                 (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J\<rbrakk> \<Longrightarrow> P I"
wenzelm@12937
   743
  shows "P I"
schirmer@12854
   744
proof -
schirmer@12854
   745
  from is_if_I ws 
schirmer@12854
   746
  show "P I"
schirmer@12854
   747
  proof (rule ws_subint1_induct)
schirmer@12854
   748
    fix I i
schirmer@12854
   749
    assume hyp: "iface G I = Some i \<and>
schirmer@12854
   750
                (\<forall>J\<in>set (isuperIfs i). (I,J) \<in>subint1 G \<and> P J \<and> is_iface G J)"
schirmer@12854
   751
    then have if_I: "iface G I = Some i"
schirmer@12854
   752
      by blast
schirmer@12854
   753
    show "P I"
schirmer@12854
   754
    proof (cases "isuperIfs i")
schirmer@12854
   755
      case Nil
schirmer@12854
   756
      with if_I hyp_sub 
schirmer@12854
   757
      show "P I" 
wenzelm@32960
   758
        by auto
schirmer@12854
   759
    next
schirmer@12854
   760
      case (Cons hd tl)
schirmer@12854
   761
      with hyp if_I hyp_sub 
schirmer@12854
   762
      show "P I" 
wenzelm@32960
   763
        by auto
schirmer@12854
   764
    qed
schirmer@12854
   765
  qed
schirmer@12854
   766
qed
schirmer@12854
   767
wenzelm@58887
   768
subsubsection "general recursion operators for the interface and class hiearchies"
schirmer@12854
   769
wenzelm@46212
   770
function iface_rec  :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
krauss@35440
   771
where
krauss@35440
   772
[simp del]: "iface_rec G I f = 
krauss@35440
   773
  (case iface G I of 
haftmann@28524
   774
         None \<Rightarrow> undefined 
schirmer@12854
   775
       | Some i \<Rightarrow> if ws_prog G 
schirmer@12854
   776
                      then f I i 
krauss@35440
   777
                               ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))
haftmann@28524
   778
                      else undefined)"
krauss@35440
   779
by auto
krauss@35440
   780
termination
krauss@35440
   781
by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subint1 G)^-1)) (%(x,y,z). (x,y))")
krauss@35440
   782
 (auto simp: wf_subint1 subint1I wf_same_fst)
schirmer@12854
   783
schirmer@12854
   784
lemma iface_rec: 
schirmer@12854
   785
"\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow> 
krauss@35440
   786
 iface_rec G I f = f I i ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))"
schirmer@12854
   787
apply (subst iface_rec.simps)
schirmer@12854
   788
apply simp
schirmer@12854
   789
done
schirmer@12854
   790
krauss@35440
   791
krauss@35440
   792
function
krauss@35440
   793
  class_rec  :: "prog \<Rightarrow> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a     \<Rightarrow> 'a) \<Rightarrow> 'a"
krauss@35440
   794
where
krauss@35440
   795
[simp del]: "class_rec G C t f = 
krauss@35440
   796
  (case class G C of 
haftmann@28524
   797
           None \<Rightarrow> undefined 
schirmer@12854
   798
         | Some c \<Rightarrow> if ws_prog G 
schirmer@12854
   799
                        then f C c 
schirmer@12854
   800
                                 (if C = Object then t 
krauss@35440
   801
                                                else class_rec G (super c) t f)
haftmann@28524
   802
                        else undefined)"
krauss@35440
   803
krauss@35440
   804
by auto
krauss@35440
   805
termination
krauss@35440
   806
by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)) (%(x,y,z,w). (x,y))")
krauss@35440
   807
 (auto simp: wf_subcls1 subcls1I wf_same_fst)
schirmer@12854
   808
schirmer@12854
   809
lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>  
krauss@35440
   810
 class_rec G C t f = 
krauss@35440
   811
   f C c (if C = Object then t else class_rec G (super c) t f)"
krauss@35440
   812
apply (subst class_rec.simps)
schirmer@12854
   813
apply simp
schirmer@12854
   814
done
schirmer@12854
   815
wenzelm@37956
   816
definition
wenzelm@37956
   817
  imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
wenzelm@62042
   818
  \<comment>\<open>methods of an interface, with overriding and inheritance, cf. 9.2\<close>
wenzelm@37956
   819
  "imethds G I = iface_rec G I
schirmer@12854
   820
              (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
blanchet@55518
   821
                        (set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
wenzelm@32960
   822
        
schirmer@12854
   823
schirmer@12854
   824
schirmer@12854
   825
end