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