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