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