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