# Theory Decl

Up to index of Isabelle/HOL/Bali

theory Decl
imports Term Table
begin

    (*  Title:      HOL/Bali/Decl.thy
        ID:         $Id: Decl.thy,v 1.14 2005/09/22 21:56:23 nipkow Exp $
        Author:     David von Oheimb and Norbert Schirmer
    *)
    header {* Field, method, interface, and class declarations, whole Java programs
    *}

    (** order is significant, because of clash for "var" **)
    theory Decl imports Term Table begin

    text {*
    improvements:
    \begin{itemize}
    \item clarification and correction of some aspects of the package/access concept
      (Also submitted as bug report to the Java Bug Database:
       Bug Id: 4485402 and Bug Id: 4493343
       http://developer.java.sun.com/developer/bugParade/index.jshtml
      )
    \end{itemize}
    simplifications:
    \begin{itemize}
    \item the only field and method modifiers are static and the access modifiers
    \item no constructors, which may be simulated by new + suitable methods
    \item there is just one global initializer per class, which can simulate all
          others

    \item no throws clause
    \item a void method is replaced by one that returns Unit (of dummy type Void)

    \item no interface fields

    \item every class has an explicit superclass (unused for Object)
    \item the (standard) methods of Object and of standard exceptions are not
          specified

    \item no main method
    \end{itemize}
    *}

    subsection {* Modifier*}

    subsubsection {* Access modifier *}

    datatype acc_modi (* access modifier *)
             = Private | Package | Protected | Public

    text {*
    We can define a linear order for the access modifiers. With Private yielding the
    most restrictive access and public the most liberal access policy:
      Private < Package < Protected < Public
    *}

    instance acc_modi:: ord ..

    defs (overloaded)
    less_acc_def:
     "a < (b::acc_modi)
          ≡ (case a of
                 Private    => (b=Package ∨ b=Protected ∨ b=Public)
               | Package    => (b=Protected ∨ b=Public)
               | Protected  => (b=Public)
               | Public     => False)"
    le_acc_def:
     "a ≤ (b::acc_modi) ≡ (a = b) ∨ (a < b)"

    instance acc_modi:: order
    proof
      fix x y z::acc_modi
      {
      show "x ≤ x"                       -- reflexivity
        by (auto simp add: le_acc_def)
      next
      assume "x ≤ y" "y ≤ z"           -- transitivity
      thus "x ≤ z"
        by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
      next
      assume "x ≤ y" "y ≤ x"           -- antisymmetry
      thus "x = y"
      proof -
        have "∀ x y. x < (y::acc_modi) ∧ y < x --> False"
          by (auto simp add: less_acc_def split add: acc_modi.split)
        with prems show ?thesis
          by (unfold le_acc_def) iprover
      qed
      next
      show "(x < y) = (x ≤ y ∧ x ≠ y)"
        by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
      }
    qed

    instance acc_modi:: linorder
    proof
      fix x y:: acc_modi
      show  "x ≤ y ∨ y ≤ x"
      by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
    qed

    lemma acc_modi_top [simp]: "Public ≤ a ==> a = Public"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemma acc_modi_top1 [simp, intro!]: "a ≤ Public"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemma acc_modi_le_Public:
    "a ≤ Public ==> a=Private ∨ a = Package ∨ a=Protected ∨ a=Public"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemma acc_modi_bottom: "a ≤ Private ==> a = Private"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemma acc_modi_Private_le:
    "Private ≤ a ==> a=Private ∨ a = Package ∨ a=Protected ∨ a=Public"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemma acc_modi_Package_le:
      "Package ≤ a ==> a = Package ∨ a=Protected ∨ a=Public"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.split)

    lemma acc_modi_le_Package:
      "a ≤ Package ==> a=Private ∨ a = Package"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemma acc_modi_Protected_le:
      "Protected ≤ a ==> a=Protected ∨ a=Public"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemma acc_modi_le_Protected:
      "a ≤ Protected  ==> a=Private ∨ a = Package ∨ a = Protected"
    by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)

    lemmas acc_modi_le_Dests = acc_modi_top           acc_modi_le_Public
                               acc_modi_Private_le    acc_modi_bottom
                               acc_modi_Package_le    acc_modi_le_Package
                               acc_modi_Protected_le  acc_modi_le_Protected

    lemma acc_modi_Package_le_cases
     [consumes 1,case_names Package Protected Public]:
     "Package ≤ m ==> ( m = Package ==> P m) ==> (m=Protected ==> P m) ==>
       (m=Public ==> P m) ==> P m"
    by (auto dest: acc_modi_Package_le)

    subsubsection {* Static Modifier *}
    types stat_modi = bool (* modifier: static *)

    subsection {* Declaration (base "class" for member,interface and class
     declarations *}

    record decl =
            access :: acc_modi

    translations
      "decl" <= (type) "(|access::acc_modi|)),"
      "decl" <= (type) "(|access::acc_modi,…::'a|)),"

    subsection {* Member (field or method)*}
    record  member = decl +
             static :: stat_modi

    translations
      "member" <= (type) "(|access::acc_modi,static::bool|)),"
      "member" <= (type) "(|access::acc_modi,static::bool,…::'a|)),"

    subsection {* Field *}

    record field = member +
            type :: ty
    translations
      "field" <= (type) "(|access::acc_modi, static::bool, type::ty|)),"
      "field" <= (type) "(|access::acc_modi, static::bool, type::ty,…::'a|)),"

    types
            fdecl           (* field declaration, cf. 8.3 *)
            = "vname × field"

    translations
      "fdecl" <= (type) "vname × field"

    subsection  {* Method *}

    record mhead = member +     (* method head (excluding signature) *)
            pars ::"vname list" (* parameter names *)
            resT ::ty           (* result type *)

    record mbody =                      (* method body *)
            lcls::  "(vname × ty) list" (* local variables *)
            stmt:: stmt                 (* the body statement *)

    record methd = mhead + (* method in a class *)
            mbody::mbody

    types mdecl = "sig × methd"  (* method declaration in a class *)

    translations
      "mhead" <= (type) "(|access::acc_modi, static::bool,
                          pars::vname list, resT::ty|)),"
      "mhead" <= (type) "(|access::acc_modi, static::bool,
                          pars::vname list, resT::ty,…::'a|)),"
      "mbody" <= (type) "(|lcls::(vname × ty) list,stmt::stmt|)),"
      "mbody" <= (type) "(|lcls::(vname × ty) list,stmt::stmt,…::'a|)),"
      "methd" <= (type) "(|access::acc_modi, static::bool,
                          pars::vname list, resT::ty,mbody::mbody|)),"
      "methd" <= (type) "(|access::acc_modi, static::bool,
                          pars::vname list, resT::ty,mbody::mbody,…::'a|)),"
      "mdecl" <= (type) "sig × methd"

    constdefs
      mhead::"methd => mhead"
      "mhead m ≡ (|access=access m, static=static m, pars=pars m, resT=resT m|)),"

    lemma access_mhead [simp]:"access (mhead m) = access m"
    by (simp add: mhead_def)

    lemma static_mhead [simp]:"static (mhead m) = static m"
    by (simp add: mhead_def)

    lemma pars_mhead [simp]:"pars (mhead m) = pars m"
    by (simp add: mhead_def)

    lemma resT_mhead [simp]:"resT (mhead m) = resT m"
    by (simp add: mhead_def)

    text {* To be able to talk uniformaly about field and method declarations we
    introduce the notion of a member declaration (e.g. useful to define
    accessiblity ) *}

    datatype memberdecl = fdecl fdecl | mdecl mdecl

    datatype memberid = fid vname | mid sig

    axclass has_memberid < "type"
    consts
     memberid :: "'a::has_memberid => memberid"

    instance memberdecl::has_memberid ..

    defs (overloaded)
    memberdecl_memberid_def:
      "memberid m ≡ (case m of
                        fdecl (vn,f)  => fid vn
                      | mdecl (sig,m) => mid sig)"

    lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
    by (simp add: memberdecl_memberid_def)

    lemma memberid_fdecl_simp1: "memberid (fdecl f) = fid (fst f)"
    by (cases f) (simp add: memberdecl_memberid_def)

    lemma memberid_mdecl_simp[simp]: "memberid (mdecl (sig,m)) = mid sig"
    by (simp add: memberdecl_memberid_def)

    lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
    by (cases m) (simp add: memberdecl_memberid_def)

    instance * :: (type, has_memberid) has_memberid ..

    defs (overloaded)
    pair_memberid_def:
      "memberid p ≡ memberid (snd p)"

    lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
    by (simp add: pair_memberid_def)

    lemma memberid_pair_simp1: "memberid p  = memberid (snd p)"
    by (simp add: pair_memberid_def)

    constdefs is_field :: "qtname × memberdecl => bool"
    "is_field m ≡ ∃ declC f. m=(declC,fdecl f)"

    lemma is_fieldD: "is_field m ==> ∃ declC f. m=(declC,fdecl f)"
    by (simp add: is_field_def)

    lemma is_fieldI: "is_field (C,fdecl f)"
    by (simp add: is_field_def)

    constdefs is_method :: "qtname × memberdecl => bool"
    "is_method membr ≡ ∃ declC m. membr=(declC,mdecl m)"

    lemma is_methodD: "is_method membr ==> ∃ declC m. membr=(declC,mdecl m)"
    by (simp add: is_method_def)

    lemma is_methodI: "is_method (C,mdecl m)"
    by (simp add: is_method_def)

    subsection {* Interface *}

    record  ibody = decl +  --{* interface body *}
              imethods :: "(sig × mhead) list" --{* method heads *}

    record  iface = ibody + --{* interface *}
             isuperIfs:: "qtname list" --{* superinterface list *}
    types
            idecl           --{* interface declaration, cf. 9.1 *}
            = "qtname × iface"

    translations
      "ibody" <= (type) "(|access::acc_modi,imethods::(sig × mhead) list|)),"
      "ibody" <= (type) "(|access::acc_modi,imethods::(sig × mhead) list,…::'a|)),"
      "iface" <= (type) "(|access::acc_modi,imethods::(sig × mhead) list,
                          isuperIfs::qtname list|)),"
      "iface" <= (type) "(|access::acc_modi,imethods::(sig × mhead) list,
                          isuperIfs::qtname list,…::'a|)),"
      "idecl" <= (type) "qtname × iface"

    constdefs
      ibody :: "iface => ibody"
      "ibody i ≡ (|access=access i,imethods=imethods i|)),"

    lemma access_ibody [simp]: "(access (ibody i)) = access i"
    by (simp add: ibody_def)

    lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i"
    by (simp add: ibody_def)

    subsection  {* Class *}
    record cbody = decl +          --{* class body *}
             cfields:: "fdecl list"
             methods:: "mdecl list"
             init   :: "stmt"       --{* initializer *}

    record class = cbody +           --{* class *}
            super   :: "qtname"      --{* superclass *}
            superIfs:: "qtname list" --{* implemented interfaces *}
    types
            cdecl           --{* class declaration, cf. 8.1 *}
            = "qtname × class"

    translations
      "cbody" <= (type) "(|access::acc_modi,cfields::fdecl list,
                          methods::mdecl list,init::stmt|)),"
      "cbody" <= (type) "(|access::acc_modi,cfields::fdecl list,
                          methods::mdecl list,init::stmt,…::'a|)),"
      "class" <= (type) "(|access::acc_modi,cfields::fdecl list,
                          methods::mdecl list,init::stmt,
                          super::qtname,superIfs::qtname list|)),"
      "class" <= (type) "(|access::acc_modi,cfields::fdecl list,
                          methods::mdecl list,init::stmt,
                          super::qtname,superIfs::qtname list,…::'a|)),"
      "cdecl" <= (type) "qtname × class"

    constdefs
      cbody :: "class => cbody"
      "cbody c ≡ (|access=access c, cfields=cfields c,methods=methods c,init=init c|)),"

    lemma access_cbody [simp]:"access (cbody c) = access c"
    by (simp add: cbody_def)

    lemma cfields_cbody [simp]:"cfields (cbody c) = cfields c"
    by (simp add: cbody_def)

    lemma methods_cbody [simp]:"methods (cbody c) = methods c"
    by (simp add: cbody_def)

    lemma init_cbody [simp]:"init (cbody c) = init c"
    by (simp add: cbody_def)

    section "standard classes"

    consts

      Object_mdecls  ::  "mdecl list" --{* methods of Object *}
      SXcpt_mdecls   ::  "mdecl list" --{* methods of SXcpts *}
      ObjectC ::         "cdecl"      --{* declaration  of root      class   *}
      SXcptC  ::"xname => cdecl"      --{* declarations of throwable classes *}

    defs

    ObjectC_def:"ObjectC  ≡ (Object,(|access=Public,cfields=[],methods=Object_mdecls,
                                      init=Skip,super=arbitrary,superIfs=[]|)),)"
    SXcptC_def:"SXcptC xn≡ (SXcpt xn,(|access=Public,cfields=[],methods=SXcpt_mdecls,
                                       init=Skip,
                                       super=if xn = Throwable then Object
                                                               else SXcpt Throwable,
                                       superIfs=[]|)),)"

    lemma ObjectC_neq_SXcptC [simp]: "ObjectC ≠ SXcptC xn"
    by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)

    lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
    apply (simp add: SXcptC_def)
    apply auto
    done

    constdefs standard_classes :: "cdecl list"
             "standard_classes ≡ [ObjectC, SXcptC Throwable,
                    SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
                    SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"

    section "programs"

    record prog =
            ifaces ::"idecl list"
            "classes"::"cdecl list"

    translations
         "prog"<= (type) "(|ifaces::idecl list,classes::cdecl list|)),"
         "prog"<= (type) "(|ifaces::idecl list,classes::cdecl list,…::'a|)),"

    syntax
      iface     :: "prog  => (qtname, iface) table"
      class     :: "prog  => (qtname, class) table"
      is_iface  :: "prog  => qtname  => bool"
      is_class  :: "prog  => qtname  => bool"

    translations
               "iface G I" == "table_of (ifaces G) I"
               "class G C" == "table_of (classes G) C"
            "is_iface G I" == "iface G I ≠ None"
            "is_class G C" == "class G C ≠ None"

    section "is type"

    consts
      is_type :: "prog =>     ty => bool"
      isrtype :: "prog => ref_ty => bool"

    primrec "is_type G (PrimT pt)  = True"
            "is_type G (RefT  rt)  = isrtype G rt"
            "isrtype G (NullT    ) = True"
            "isrtype G (IfaceT tn) = is_iface G tn"
            "isrtype G (ClassT tn) = is_class G tn"
            "isrtype G (ArrayT T ) = is_type  G T"

    lemma type_is_iface: "is_type G (Iface I) ==> is_iface G I"
    by auto

    lemma type_is_class: "is_type G (Class C) ==>  is_class G C"
    by auto

    section "subinterface and subclass relation, in anticipation of TypeRel.thy"

    consts
      subint1  :: "prog => (qtname × qtname) set" --{* direct subinterface *}
      subcls1  :: "prog => (qtname × qtname) set" --{* direct subclass     *}

    defs
      subint1_def: "subint1 G ≡ {(I,J). ∃i∈iface G I: J∈set (isuperIfs i)}"
      subcls1_def: "subcls1 G ≡ {(C,D). C≠Object ∧ (∃c∈class G C: super c = D)}"

    syntax
     "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
     "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
     "@subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)

    syntax (xsymbols)
      "@subcls1" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>C1_"  [71,71,71] 70)
      "@subclseq":: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>C _"  [71,71,71] 70)
      "@subcls"  :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>C _"  [71,71,71] 70)

    translations
            "G\<turnstile>C \<prec>C1 D" == "(C,D) ∈ subcls1 G"
            "G\<turnstile>C \<preceq>C  D" == "(C,D) ∈(subcls1 G)^*" (* cf. 8.1.3 *)
            "G\<turnstile>C \<prec>C  D" == "(C,D) ∈(subcls1 G)^+"

    lemma subint1I: "[|iface G I = Some i; J ∈ set (isuperIfs i)|]
                     ==> (I,J) ∈ subint1 G"
    apply (simp add: subint1_def)
    done

    lemma subcls1I:"[|class G C = Some c; C ≠ Object|] ==> (C,(super c)) ∈ subcls1 G"
    apply (simp add: subcls1_def)
    done

    lemma subint1D: "(I,J)∈subint1 G==> ∃i∈iface G I: J∈set (isuperIfs i)"
    by (simp add: subint1_def)

    lemma subcls1D:
      "(C,D)∈subcls1 G ==> C≠Object ∧ (∃c. class G C = Some c ∧ (super c = D))"
    apply (simp add: subcls1_def)
    apply auto
    done

    lemma subint1_def2:
      "subint1 G = (SIGMA I: {I. is_iface G I}. set (isuperIfs (the (iface G I))))"
    apply (unfold subint1_def)
    apply auto
    done

    lemma subcls1_def2:
      "subcls1 G =
         (SIGMA C: {C. is_class G C}. {D. C≠Object ∧ super (the(class G C))=D})"
    apply (unfold subcls1_def)
    apply auto
    done

    lemma subcls_is_class:
    "[|G\<turnstile>C \<prec>C D|] ==> ∃ c. class G C = Some c"
    by (auto simp add: subcls1_def dest: tranclD)

    lemma no_subcls1_Object:"G\<turnstile>Object\<prec>C1 D ==> P"
    by (auto simp add: subcls1_def)

    lemma no_subcls_Object: "G\<turnstile>Object\<prec>C D ==> P"
    apply (erule trancl_induct)
    apply (auto intro: no_subcls1_Object)
    done

    section "well-structured programs"

    constdefs
      ws_idecl :: "prog => qtname => qtname list => bool"
     "ws_idecl G I si ≡ ∀J∈set si.  is_iface G J   ∧ (J,I)∉(subint1 G)^+"

      ws_cdecl :: "prog => qtname => qtname => bool"
     "ws_cdecl G C sc ≡ C≠Object --> is_class G sc ∧ (sc,C)∉(subcls1 G)^+"

      ws_prog  :: "prog => bool"
     "ws_prog G ≡ (∀(I,i)∈set (ifaces  G). ws_idecl G I (isuperIfs i)) ∧
                  (∀(C,c)∈set (classes G). ws_cdecl G C (super c))"

    lemma ws_progI:
    "[|∀(I,i)∈set (ifaces G). ∀J∈set (isuperIfs i). is_iface G J ∧
                                                    (J,I) ∉ (subint1 G)^+;
      ∀(C,c)∈set (classes G). C≠Object --> is_class G (super c) ∧
                                            ((super c),C) ∉ (subcls1 G)^+
     |] ==> ws_prog G"
    apply (unfold ws_prog_def ws_idecl_def ws_cdecl_def)
    apply (erule_tac conjI)
    apply blast
    done

    lemma ws_prog_ideclD:
    "[|iface G I = Some i; J∈set (isuperIfs i); ws_prog G|] ==>
      is_iface G J ∧ (J,I)∉(subint1 G)^+"
    apply (unfold ws_prog_def ws_idecl_def)
    apply clarify
    apply (drule_tac map_of_SomeD)
    apply auto
    done

    lemma ws_prog_cdeclD:
    "[|class G C = Some c; C≠Object; ws_prog G|] ==>
      is_class G (super c) ∧ (super c,C)∉(subcls1 G)^+"
    apply (unfold ws_prog_def ws_cdecl_def)
    apply clarify
    apply (drule_tac map_of_SomeD)
    apply auto
    done

    section "well-foundedness"

    lemma finite_is_iface: "finite {I. is_iface G I}"
    apply (fold dom_def)
    apply (rule_tac finite_dom_map_of)
    done

    lemma finite_is_class: "finite {C. is_class G C}"
    apply (fold dom_def)
    apply (rule_tac finite_dom_map_of)
    done

    lemma finite_subint1: "finite (subint1 G)"
    apply (subst subint1_def2)
    apply (rule finite_SigmaI)
    apply (rule finite_is_iface)
    apply (simp (no_asm))
    done

    lemma finite_subcls1: "finite (subcls1 G)"
    apply (subst subcls1_def2)
    apply (rule finite_SigmaI)
    apply (rule finite_is_class)
    apply (rule_tac B = "{super (the (class G C))}" in finite_subset)
    apply  auto
    done

    lemma subint1_irrefl_lemma1:
      "ws_prog G ==> (subint1 G)^-1 ∩ (subint1 G)^+ = {}"
    apply (force dest: subint1D ws_prog_ideclD conjunct2)
    done

    lemma subcls1_irrefl_lemma1:
      "ws_prog G ==> (subcls1 G)^-1 ∩ (subcls1 G)^+ = {}"
    apply (force dest: subcls1D ws_prog_cdeclD conjunct2)
    done

    lemmas subint1_irrefl_lemma2 = subint1_irrefl_lemma1 [THEN irrefl_tranclI']
    lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']

    lemma subint1_irrefl: "[|(x, y) ∈ subint1 G; ws_prog G|] ==> x ≠ y"
    apply (rule irrefl_trancl_rD)
    apply (rule subint1_irrefl_lemma2)
    apply auto
    done

    lemma subcls1_irrefl: "[|(x, y) ∈ subcls1 G; ws_prog G|] ==> x ≠ y"
    apply (rule irrefl_trancl_rD)
    apply (rule subcls1_irrefl_lemma2)
    apply auto
    done

    lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
    lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]

    lemma wf_subint1: "ws_prog G ==> wf ((subint1 G)¯)"
    by (auto intro: finite_acyclic_wf_converse finite_subint1 subint1_acyclic)

    lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)¯)"
    by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)

    lemma subint1_induct:
      "[|ws_prog G; !!x. ∀y. (x, y) ∈ subint1 G --> P y ==> P x|] ==> P a"
    apply (frule wf_subint1)
    apply (erule wf_induct)
    apply (simp (no_asm_use) only: converse_iff)
    apply blast
    done

    lemma subcls1_induct [consumes 1]:
      "[|ws_prog G; !!x. ∀y. (x, y) ∈ subcls1 G --> P y ==> P x|] ==> P a"
    apply (frule wf_subcls1)
    apply (erule wf_induct)
    apply (simp (no_asm_use) only: converse_iff)
    apply blast
    done

    lemma ws_subint1_induct:
     "[|is_iface G I; ws_prog G; !!I i. [|iface G I = Some i ∧
       (∀J ∈ set (isuperIfs i). (I,J)∈subint1 G ∧ P J ∧ is_iface G J)|] ==> P I
      |] ==> P I"
    apply (erule make_imp)
    apply (rule subint1_induct)
    apply  assumption
    apply safe
    apply (fast dest: subint1I ws_prog_ideclD)
    done

    lemma ws_subcls1_induct: "[|is_class G C; ws_prog G;
      !!C c. [|class G C = Some c;
     (C ≠ Object --> (C,(super c))∈subcls1 G ∧
                      P (super c) ∧ is_class G (super c))|] ==> P C
     |] ==> P C"
    apply (erule make_imp)
    apply (rule subcls1_induct)
    apply  assumption
    apply safe
    apply (fast dest: subcls1I ws_prog_cdeclD)
    done

    lemma ws_class_induct [consumes 2, case_names Object Subcls]:
    "[|class G C = Some c; ws_prog G;
      !! co. class G Object = Some co ==> P Object;
      !!  C c. [|class G C = Some c; C ≠ Object; P (super c)|] ==> P C
     |] ==> P C"
    proof -
      assume clsC: "class G C = Some c"
      and    init: "!! co. class G Object = Some co ==> P Object"
      and    step: "!!   C c. [|class G C = Some c; C ≠ Object; P (super c)|] ==> P C"
      assume ws: "ws_prog G"
      then have "is_class G C ==> P C"
      proof (induct rule: subcls1_induct)
        fix C
        assume   hyp:"∀ S. G\<turnstile>C \<prec>C1 S --> is_class G S --> P S"
           and iscls:"is_class G C"
        show "P C"
        proof (cases "C=Object")
          case True with iscls init show "P C" by auto
        next
          case False with ws step hyp iscls
          show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
        qed
      qed
      with clsC show ?thesis by simp
    qed

    lemma ws_class_induct' [consumes 2, case_names Object Subcls]:
    "[|is_class G C; ws_prog G;
      !! co. class G Object = Some co ==> P Object;
      !! C c. [|class G C = Some c; C ≠ Object; P (super c)|] ==> P C
     |] ==> P C"
    by (blast intro: ws_class_induct)

    lemma ws_class_induct'' [consumes 2, case_names Object Subcls]:
    "[|class G C = Some c; ws_prog G;
      !! co. class G Object = Some co ==> P Object co;
      !!  C c sc. [|class G C = Some c; class G (super c) = Some sc;
                C ≠ Object; P (super c) sc|] ==> P C c
     |] ==> P C c"
    proof -
      assume clsC: "class G C = Some c"
      and    init: "!! co. class G Object = Some co ==> P Object co"
      and    step: "!! C c sc . [|class G C = Some c; class G (super c) = Some sc;
                                 C ≠ Object; P (super c) sc|] ==> P C c"
      assume ws: "ws_prog G"
      then have "!! c. class G C = Some c==> P C c"
      proof (induct rule: subcls1_induct)
        fix C c
        assume   hyp:"∀ S. G\<turnstile>C \<prec>C1 S --> (∀ s. class G S = Some s --> P S s)"
           and iscls:"class G C = Some c"
        show "P C c"
        proof (cases "C=Object")
          case True with iscls init show "P C c" by auto
        next
          case False
          with ws iscls obtain sc where
            sc: "class G (super c) = Some sc"
            by (auto dest: ws_prog_cdeclD)
          from iscls False have "G\<turnstile>C \<prec>C1 (super c)" by (rule subcls1I)
          with False ws step hyp iscls sc
          show "P C c"
            by (auto)
        qed
      qed
      with clsC show "P C c" by auto
    qed

    lemma ws_interface_induct [consumes 2, case_names Step]:
      assumes is_if_I: "is_iface G I" and
                   ws: "ws_prog G" and
              hyp_sub: "!!I i. [|iface G I = Some i;
                                ∀ J ∈ set (isuperIfs i).
                                     (I,J)∈subint1 G ∧ P J ∧ is_iface G J|] ==> P I"
      shows "P I"
    proof -
      from is_if_I ws
      show "P I"
      proof (rule ws_subint1_induct)
        fix I i
        assume hyp: "iface G I = Some i ∧
                    (∀J∈set (isuperIfs i). (I,J) ∈subint1 G ∧ P J ∧ is_iface G J)"
        then have if_I: "iface G I = Some i"
          by blast
        show "P I"
        proof (cases "isuperIfs i")
          case Nil
          with if_I hyp_sub
          show "P I"
            by auto
        next
          case (Cons hd tl)
          with hyp if_I hyp_sub
          show "P I"
            by auto
        qed
      qed
    qed

    section "general recursion operators for the interface and class hiearchies"

    consts
      iface_rec  :: "prog × qtname =>       (qtname => iface => 'a set => 'a) => 'a"
      class_rec  :: "prog × qtname => 'a => (qtname => class => 'a     => 'a) => 'a"

    recdef iface_rec "same_fst ws_prog (λG. (subint1 G)^-1)"
    "iface_rec (G,I) =
      (λf. case iface G I of
             None => arbitrary
           | Some i => if ws_prog G
                          then f I i
                                   ((λJ. iface_rec (G,J) f)`set (isuperIfs i))
                          else arbitrary)"
    (hints recdef_wf: wf_subint1 intro: subint1I)
    declare iface_rec.simps [simp del]

    lemma iface_rec:
    "[|iface G I = Some i; ws_prog G|] ==>
     iface_rec (G,I) f = f I i ((λJ. iface_rec (G,J) f)`set (isuperIfs i))"
    apply (subst iface_rec.simps)
    apply simp
    done

    recdef class_rec "same_fst ws_prog (λG. (subcls1 G)^-1)"
    "class_rec(G,C) =
      (λt f. case class G C of
               None => arbitrary
             | Some c => if ws_prog G
                            then f C c
                                     (if C = Object then t
                                                    else class_rec (G,super c) t f)
                            else arbitrary)"
    (hints recdef_wf: wf_subcls1 intro: subcls1I)
    declare class_rec.simps [simp del]

    lemma class_rec: "[|class G C = Some c; ws_prog G|] ==>
     class_rec (G,C) t f =
       f C c (if C = Object then t else class_rec (G,super c) t f)"
    apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
    apply simp
    done

    constdefs
    imethds:: "prog => qtname => (sig,qtname × mhead) tables"
      --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    "imethds G I
      ≡ iface_rec (G,I)
                  (λI i ts. (Un_tables ts) ⊕⊕
                            (o2s o table_of (map (λ(s,m). (s,I,m)) (imethods i))))"

    end

### Modifier

#### Access modifier

lemma acc_modi_top:

      Public ≤ a ==> a = Public

lemma acc_modi_top1:

      a ≤ Public

lemma acc_modi_le_Public:

      a ≤ Public ==> a = Private ∨ a = Package ∨ a = Protected ∨ a = Public

lemma acc_modi_bottom:

      a ≤ Private ==> a = Private

lemma acc_modi_Private_le:

      Private ≤ a ==> a = Private ∨ a = Package ∨ a = Protected ∨ a = Public

lemma acc_modi_Package_le:

      Package ≤ a ==> a = Package ∨ a = Protected ∨ a = Public

lemma acc_modi_le_Package:

      a ≤ Package ==> a = Private ∨ a = Package

lemma acc_modi_Protected_le:

      Protected ≤ a ==> a = Protected ∨ a = Public

lemma acc_modi_le_Protected:

      a ≤ Protected ==> a = Private ∨ a = Package ∨ a = Protected

lemmas acc_modi_le_Dests:

      Public ≤ a ==> a = Public

      a ≤ Public ==> a = Private ∨ a = Package ∨ a = Protected ∨ a = Public

      Private ≤ a ==> a = Private ∨ a = Package ∨ a = Protected ∨ a = Public

      a ≤ Private ==> a = Private

      Package ≤ a ==> a = Package ∨ a = Protected ∨ a = Public

      a ≤ Package ==> a = Private ∨ a = Package

      Protected ≤ a ==> a = Protected ∨ a = Public

      a ≤ Protected ==> a = Private ∨ a = Package ∨ a = Protected

lemmas acc_modi_le_Dests:

      Public ≤ a ==> a = Public

      a ≤ Public ==> a = Private ∨ a = Package ∨ a = Protected ∨ a = Public

      Private ≤ a ==> a = Private ∨ a = Package ∨ a = Protected ∨ a = Public

      a ≤ Private ==> a = Private

      Package ≤ a ==> a = Package ∨ a = Protected ∨ a = Public

      a ≤ Package ==> a = Private ∨ a = Package

      Protected ≤ a ==> a = Protected ∨ a = Public

      a ≤ Protected ==> a = Private ∨ a = Package ∨ a = Protected

lemma acc_modi_Package_le_cases:

      [| Package ≤ m; m = Package ==> P m; m = Protected ==> P m;
         m = Public ==> P m |]
      ==> P m

#### Static Modifier

### Declaration (base "class" for member,interface and class declarations

### Member (field or method)

### Field

### Method

lemma access_mhead:

      access (mhead m) = access m

lemma static_mhead:

      static (mhead m) = static m

lemma pars_mhead:

      pars (mhead m) = pars m

lemma resT_mhead:

      resT (mhead m) = resT m

lemma memberid_fdecl_simp:

      memberid (fdecl (vn, f)) = fid vn

lemma memberid_fdecl_simp1:

      memberid (fdecl f) = fid (fst f)

lemma memberid_mdecl_simp:

      memberid (mdecl (sig, m)) = mid sig

lemma memberid_mdecl_simp1:

      memberid (mdecl m) = mid (fst m)

lemma memberid_pair_simp:

      memberid (c, m) = memberid m

lemma memberid_pair_simp1:

      memberid p = memberid (snd p)

lemma is_fieldD:

      is_field m ==> ∃declC f. m = (declC, fdecl f)

lemma is_fieldI:

      is_field (C, fdecl f)

lemma is_methodD:

      is_method membr ==> ∃declC m. membr = (declC, mdecl m)

lemma is_methodI:

      is_method (C, mdecl m)

### Interface

lemma access_ibody:

      access (ibody i) = access i

lemma imethods_ibody:

      imethods (ibody i) = imethods i

### Class

lemma access_cbody:

      access (cbody c) = access c

lemma cfields_cbody:

      cfields (cbody c) = cfields c

lemma methods_cbody:

      methods (cbody c) = methods c

lemma init_cbody:

      init (cbody c) = init c

## standard classes

lemma ObjectC_neq_SXcptC:

      ObjectC ≠ SXcptC xn

lemma SXcptC_inject:

      (SXcptC xn = SXcptC xm) = (xn = xm)

## programs

## is type

lemma type_is_iface:

      is_type G (Iface I) ==> is_iface G I

lemma type_is_class:

      is_type G (Class C) ==> is_class G C

## subinterface and subclass relation, in anticipation of TypeRel.thy

lemma subint1I:

      [| iface G I = Some i; J ∈ set (isuperIfs i) |] ==> (I, J) ∈ subint1 G

lemma subcls1I:

      [| class G C = Some c; C ≠ Object |] ==> G|-C<:C1super c

lemma subint1D:

      (I, J) ∈ subint1 G ==> ? i:iface G I: J ∈ set (isuperIfs i)

lemma subcls1D:

      G|-C<:C1D ==> C ≠ Object ∧ (∃c. class G C = Some c ∧ super c = D)

lemma subint1_def2:

      subint1 G = (SIGMA I:{I. is_iface G I}. set (isuperIfs (the (iface G I))))

lemma subcls1_def2:

      subcls1 G =
      (SIGMA C:{C. is_class G C}. {D. C ≠ Object ∧ super (the (class G C)) = D})

lemma subcls_is_class:

      G|-C<:C D ==> ∃c. class G C = Some c

lemma no_subcls1_Object:

      G|-Object<:C1D ==> P

lemma no_subcls_Object:

      G|-Object<:C D ==> P

## well-structured programs

lemma ws_progI:

      [| ∀(I, i)∈set (ifaces G).
            ∀J∈set (isuperIfs i). is_iface G J ∧ (J, I) ∉ (subint1 G)+;
         ∀(C, c)∈set (classes G).
            C ≠ Object --> is_class G (super c) ∧ (super c, C) ∉ (subcls1 G)+ |]
      ==> ws_prog G

lemma ws_prog_ideclD:

      [| iface G I = Some i; J ∈ set (isuperIfs i); ws_prog G |]
      ==> is_iface G J ∧ (J, I) ∉ (subint1 G)+

lemma ws_prog_cdeclD:

      [| class G C = Some c; C ≠ Object; ws_prog G |]
      ==> is_class G (super c) ∧ (super c, C) ∉ (subcls1 G)+

## well-foundedness

lemma finite_is_iface:

      finite {I. is_iface G I}

lemma finite_is_class:

      finite {C. is_class G C}

lemma finite_subint1:

      finite (subint1 G)

lemma finite_subcls1:

      finite (subcls1 G)

lemma subint1_irrefl_lemma1:

      ws_prog G ==> (subint1 G)^-1 ∩ (subint1 G)+ = {}

lemma subcls1_irrefl_lemma1:

      ws_prog G ==> (subcls1 G)^-1 ∩ (subcls1 G)+ = {}

lemmas subint1_irrefl_lemma2:

      ws_prog G1 ==> ∀x. (x, x) ∉ (subint1 G1)+

lemmas subint1_irrefl_lemma2:

      ws_prog G1 ==> ∀x. (x, x) ∉ (subint1 G1)+

lemmas subcls1_irrefl_lemma2:

      ws_prog G1 ==> ∀x. (x, x) ∉ (subcls1 G1)+

lemmas subcls1_irrefl_lemma2:

      ws_prog G1 ==> ∀x. (x, x) ∉ (subcls1 G1)+

lemma subint1_irrefl:

      [| (x, y) ∈ subint1 G; ws_prog G |] ==> x ≠ y

lemma subcls1_irrefl:

      [| G|-x<:C1y; ws_prog G |] ==> x ≠ y

lemmas subint1_acyclic:

      ws_prog G ==> acyclic (subint1 G)

lemmas subint1_acyclic:

      ws_prog G ==> acyclic (subint1 G)

lemmas subcls1_acyclic:

      ws_prog G ==> acyclic (subcls1 G)

lemmas subcls1_acyclic:

      ws_prog G ==> acyclic (subcls1 G)

lemma wf_subint1:

      ws_prog G ==> wf ((subint1 G)^-1)

lemma wf_subcls1:

      ws_prog G ==> wf ((subcls1 G)^-1)

lemma subint1_induct:

      [| ws_prog G; !!x. ∀y. (x, y) ∈ subint1 G --> P y ==> P x |] ==> P a

lemma subcls1_induct:

      [| ws_prog G; !!x. ∀y. G|-x<:C1y --> P y ==> P x |] ==> P a

lemma ws_subint1_induct:

      [| is_iface G I; ws_prog G;
         !!I i. iface G I = Some i ∧
                (∀J∈set (isuperIfs i). (I, J) ∈ subint1 G ∧ P J ∧ is_iface G J)
                ==> P I |]
      ==> P I

lemma ws_subcls1_induct:

      [| is_class G C; ws_prog G;
         !!C c. [| class G C = Some c;
                   C ≠ Object -->
                   G|-C<:C1super c ∧ P (super c) ∧ is_class G (super c) |]
                ==> P C |]
      ==> P C

lemma ws_class_induct:

      [| class G C = Some c; ws_prog G; !!co. class G Object = Some co ==> P Object;
         !!C c. [| class G C = Some c; C ≠ Object; P (super c) |] ==> P C |]
      ==> P C

lemma ws_class_induct':

      [| is_class G C; ws_prog G; !!co. class G Object = Some co ==> P Object;
         !!C c. [| class G C = Some c; C ≠ Object; P (super c) |] ==> P C |]
      ==> P C

lemma ws_class_induct'':

      [| class G C = Some c; ws_prog G;
         !!co. class G Object = Some co ==> P Object co;
         !!C c sc.
            [| class G C = Some c; class G (super c) = Some sc; C ≠ Object;
               P (super c) sc |]
            ==> P C c |]
      ==> P C c

lemma ws_interface_induct:

      [| is_iface G I; ws_prog G;
         !!I i. [| iface G I = Some i;
                   ∀J∈set (isuperIfs i). (I, J) ∈ subint1 G ∧ P J ∧ is_iface G J |]
                ==> P I |]
      ==> P I

## general recursion operators for the interface and class hiearchies

lemma iface_rec:

      [| iface G I = Some i; ws_prog G |]
      ==> iface_rec (G, I) f = f I i ((%J. iface_rec (G, J) f) ` set (isuperIfs i))

lemma class_rec:

      [| class G C = Some c; ws_prog G |]
      ==> class_rec (G, C) t f =
          f C c (if C = Object then t else class_rec (G, super c) t f)