# Theory TypeRel

Up to index of Isabelle/HOL/Bali

theory TypeRel
imports Decl
begin

    (*  Title:      HOL/Bali/TypeRel.thy
        ID:         $Id: TypeRel.thy,v 1.8 2005/06/17 14:13:06 haftmann Exp $
        Author:     David von Oheimb
    *)
    header {* The relations between Java types *}

    theory TypeRel imports Decl begin

    text {*
    simplifications:
    \begin{itemize}
    \item subinterface, subclass and widening relation includes identity
    \end{itemize}
    improvements over Java Specification 1.0:
    \begin{itemize}
    \item narrowing reference conversion also in cases where the return types of a
          pair of methods common to both types are in widening (rather identity)
          relation
    \item one could add similar constraints also for other cases
    \end{itemize}
    design issues:
    \begin{itemize}
    \item the type relations do not require @{text is_type} for their arguments
    \item the subint1 and subcls1 relations imply @{text is_iface}/@{text is_class}
          for their first arguments, which is required for their finiteness
    \end{itemize}
    *}

    consts

    (*subint1, in Decl.thy*)                     (* direct subinterface       *)
    (*subint , by translation*)                  (* subinterface (+ identity) *)
    (*subcls1, in Decl.thy*)                     (* direct subclass           *)
    (*subcls , by translation*)                  (*        subclass           *)
    (*subclseq, by translation*)                 (* subclass + identity       *)
      implmt1   :: "prog => (qtname × qtname) set" --{* direct implementation *}
      implmt    :: "prog => (qtname × qtname) set" --{*        implementation *}
      widen     :: "prog => (ty    × ty   ) set" --{*        widening       *}
      narrow    :: "prog => (ty    × ty   ) set" --{*        narrowing      *}
      cast     :: "prog => (ty    × ty   ) set"  --{*        casting        *}

    syntax

     "@subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
     "@subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
     (* Defined in Decl.thy:
     "@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)
     *)
     "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
     "@implmt"  :: "prog => [qtname, qtname] => bool" ("_|-_~>_"   [71,71,71] 70)
     "@widen"   :: "prog => [ty   , ty   ] => bool" ("_|-_<=:_"  [71,71,71] 70)
     "@narrow"  :: "prog => [ty   , ty   ] => bool" ("_|-_:>_"   [71,71,71] 70)
     "@cast"    :: "prog => [ty   , ty   ] => bool" ("_|-_<=:? _"[71,71,71] 70)

    syntax (symbols)

      "@subint1" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
      "@subint"  :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
      (* Defined in Decl.thy:
    \  "@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)
      *)
      "@implmt1" :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
      "@implmt"  :: "prog => [qtname, qtname] => bool" ("_\<turnstile>_\<leadsto>_"   [71,71,71] 70)
      "@widen"   :: "prog => [ty   , ty   ] => bool" ("_\<turnstile>_\<preceq>_"    [71,71,71] 70)
      "@narrow"  :: "prog => [ty   , ty   ] => bool" ("_\<turnstile>_\<succ>_"    [71,71,71] 70)
      "@cast"    :: "prog => [ty   , ty   ] => bool" ("_\<turnstile>_\<preceq>? _"  [71,71,71] 70)

    translations

            "G\<turnstile>I \<prec>I1 J" == "(I,J) ∈ subint1 G"
            "G\<turnstile>I \<preceq>I  J" == "(I,J) ∈(subint1 G)^*" --{* cf. 9.1.3 *}
            (* Defined in Decl.thy:
            "G\<turnstile>C \<prec>C1 D" == "(C,D) ∈ subcls1 G"
            "G\<turnstile>C \<preceq>C  D" == "(C,D) ∈(subcls1 G)^*"
            *)
            "G\<turnstile>C \<leadsto>1 I" == "(C,I) ∈ implmt1 G"
            "G\<turnstile>C \<leadsto>  I" == "(C,I) ∈ implmt  G"
            "G\<turnstile>S \<preceq>   T" == "(S,T) ∈ widen   G"
            "G\<turnstile>S \<succ>   T" == "(S,T) ∈ narrow  G"
            "G\<turnstile>S \<preceq>?  T" == "(S,T) ∈ cast    G"

    section "subclass and subinterface relations"

      (* direct subinterface in Decl.thy, cf. 9.1.3 *)
      (* direct subclass     in Decl.thy, cf. 8.1.3 *)

    lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]

    lemma subcls_direct1:
     "[|class G C = Some c; C ≠ Object;D=super c|] ==> G\<turnstile>C\<preceq>C D"
    apply (auto dest: subcls_direct)
    done

    lemma subcls1I1:
     "[|class G C = Some c; C ≠ Object;D=super c|] ==> G\<turnstile>C\<prec>C1 D"
    apply (auto dest: subcls1I)
    done

    lemma subcls_direct2:
     "[|class G C = Some c; C ≠ Object;D=super c|] ==> G\<turnstile>C\<prec>C D"
    apply (auto dest: subcls1I1)
    done

    lemma subclseq_trans: "[|G\<turnstile>A \<preceq>C B; G\<turnstile>B \<preceq>C C|] ==> G\<turnstile>A \<preceq>C C"
    by (blast intro: rtrancl_trans)

    lemma subcls_trans: "[|G\<turnstile>A \<prec>C B; G\<turnstile>B \<prec>C C|] ==> G\<turnstile>A \<prec>C C"
    by (blast intro: trancl_trans)

    lemma SXcpt_subcls_Throwable_lemma:
    "[|class G (SXcpt xn) = Some xc;
      super xc = (if xn = Throwable then Object else  SXcpt Throwable)|]
    ==> G\<turnstile>SXcpt xn\<preceq>C SXcpt Throwable"
    apply (case_tac "xn = Throwable")
    apply  simp_all
    apply (drule subcls_direct)
    apply (auto dest: sym)
    done

    lemma subcls_ObjectI: "[|is_class G C; ws_prog G|] ==> G\<turnstile>C\<preceq>C Object"
    apply (erule ws_subcls1_induct)
    apply clarsimp
    apply (case_tac "C = Object")
    apply  (fast intro: r_into_rtrancl [THEN rtrancl_trans])+
    done

    lemma subclseq_ObjectD [dest!]: "G\<turnstile>Object\<preceq>C C ==> C = Object"
    apply (erule rtrancl_induct)
    apply  (auto dest: subcls1D)
    done

    lemma subcls_ObjectD [dest!]: "G\<turnstile>Object\<prec>C C ==> False"
    apply (erule trancl_induct)
    apply  (auto dest: subcls1D)
    done

    lemma subcls_ObjectI1 [intro!]:
     "[|C ≠ Object;is_class G C;ws_prog G|] ==> G\<turnstile>C \<prec>C Object"
    apply (drule (1) subcls_ObjectI)
    apply (auto intro: rtrancl_into_trancl3)
    done

    lemma subcls_is_class: "(C,D) ∈ (subcls1 G)^+ ==> is_class G C"
    apply (erule trancl_trans_induct)
    apply (auto dest!: subcls1D)
    done

    lemma subcls_is_class2 [rule_format (no_asm)]:
     "G\<turnstile>C\<preceq>C D ==> is_class G D --> is_class G C"
    apply (erule rtrancl_induct)
    apply (drule_tac [2] subcls1D)
    apply  auto
    done

    lemma single_inheritance:
    "[|G\<turnstile>A \<prec>C1 B; G\<turnstile>A \<prec>C1 C|] ==> B = C"
    by (auto simp add: subcls1_def)

    lemma subcls_compareable:
    "[|G\<turnstile>A \<preceq>C X; G\<turnstile>A \<preceq>C Y
     |] ==> G\<turnstile>X \<preceq>C Y ∨ G\<turnstile>Y \<preceq>C X"
    by (rule triangle_lemma)  (auto intro: single_inheritance)

    lemma subcls1_irrefl: "[|G\<turnstile>C \<prec>C1 D; ws_prog G |]
     ==> C ≠ D"
    proof
      assume ws: "ws_prog G" and
        subcls1: "G\<turnstile>C \<prec>C1 D" and
         eq_C_D: "C=D"
      from subcls1 obtain c
        where
          neq_C_Object: "C≠Object" and
                  clsC: "class G C = Some c" and
               super_c: "super c = D"
        by (auto simp add: subcls1_def)
      with super_c subcls1 eq_C_D
      have subcls_super_c_C: "G\<turnstile>super c \<prec>C C"
        by auto
      from ws clsC neq_C_Object
      have "¬ G\<turnstile>super c \<prec>C C"
        by (auto dest: ws_prog_cdeclD)
      from this subcls_super_c_C
      show "False"
        by (rule notE)
    qed

    lemma no_subcls_Object: "G\<turnstile>C \<prec>C D ==> C ≠ Object"
    by (erule converse_trancl_induct) (auto dest: subcls1D)

    lemma subcls_acyclic: "[|G\<turnstile>C \<prec>C D; ws_prog G|] ==> ¬ G\<turnstile>D \<prec>C C"
    proof -
      assume         ws: "ws_prog G"
      assume subcls_C_D: "G\<turnstile>C \<prec>C D"
      then show ?thesis
      proof (induct rule: converse_trancl_induct)
        fix C
        assume subcls1_C_D: "G\<turnstile>C \<prec>C1 D"
        then obtain c  where
            "C≠Object" and
            "class G C = Some c" and
            "super c = D"
          by (auto simp add: subcls1_def)
        with ws
        show "¬ G\<turnstile>D \<prec>C C"
          by (auto dest: ws_prog_cdeclD)
      next
        fix C Z
        assume subcls1_C_Z: "G\<turnstile>C \<prec>C1 Z" and
                subcls_Z_D: "G\<turnstile>Z \<prec>C D" and
               nsubcls_D_Z: "¬ G\<turnstile>D \<prec>C Z"
        show "¬ G\<turnstile>D \<prec>C C"
        proof
          assume subcls_D_C: "G\<turnstile>D \<prec>C C"
          show "False"
          proof -
            from subcls_D_C subcls1_C_Z
            have "G\<turnstile>D \<prec>C Z"
              by (auto dest: r_into_trancl trancl_trans)
            with nsubcls_D_Z
            show ?thesis
              by (rule notE)
          qed
        qed
      qed
    qed

    lemma subclseq_cases [consumes 1, case_names Eq Subcls]:
     "[|G\<turnstile>C \<preceq>C D; C = D ==> P; G\<turnstile>C \<prec>C D ==> P|] ==> P"
    by (blast intro: rtrancl_cases)

    lemma subclseq_acyclic:
     "[|G\<turnstile>C \<preceq>C D; G\<turnstile>D \<preceq>C C; ws_prog G|] ==> C=D"
    by (auto elim: subclseq_cases dest: subcls_acyclic)

    lemma subcls_irrefl: "[|G\<turnstile>C \<prec>C D; ws_prog G|]
     ==> C ≠ D"
    proof -
      assume     ws: "ws_prog G"
      assume subcls: "G\<turnstile>C \<prec>C D"
      then show ?thesis
      proof (induct rule: converse_trancl_induct)
        fix C
        assume "G\<turnstile>C \<prec>C1 D"
        with ws
        show "C≠D"
          by (blast dest: subcls1_irrefl)
      next
        fix C Z
        assume subcls1_C_Z: "G\<turnstile>C \<prec>C1 Z" and
                subcls_Z_D: "G\<turnstile>Z \<prec>C D" and
                   neq_Z_D: "Z ≠ D"
        show "C≠D"
        proof
          assume eq_C_D: "C=D"
          show "False"
          proof -
            from subcls1_C_Z eq_C_D
            have "G\<turnstile>D \<prec>C Z"
              by (auto)
            also
            from subcls_Z_D ws
            have "¬ G\<turnstile>D \<prec>C Z"
              by (rule subcls_acyclic)
            ultimately
            show ?thesis
              by - (rule notE)
          qed
        qed
      qed
    qed

    lemma invert_subclseq:
    "[|G\<turnstile>C \<preceq>C D; ws_prog G|]
     ==> ¬ G\<turnstile>D \<prec>C C"
    proof -
      assume       ws: "ws_prog G" and
         subclseq_C_D: "G\<turnstile>C \<preceq>C D"
      show ?thesis
      proof (cases "D=C")
        case True
        with ws
        show ?thesis
          by (auto dest: subcls_irrefl)
      next
        case False
        with subclseq_C_D
        have "G\<turnstile>C \<prec>C D"
          by (blast intro: rtrancl_into_trancl3)
        with ws
        show ?thesis
          by (blast dest: subcls_acyclic)
      qed
    qed

    lemma invert_subcls:
    "[|G\<turnstile>C \<prec>C D; ws_prog G|]
     ==> ¬ G\<turnstile>D \<preceq>C C"
    proof -
      assume        ws: "ws_prog G" and
            subcls_C_D: "G\<turnstile>C \<prec>C D"
      then
      have nsubcls_D_C: "¬ G\<turnstile>D \<prec>C C"
        by (blast dest: subcls_acyclic)
      show ?thesis
      proof
        assume "G\<turnstile>D \<preceq>C C"
        then show "False"
        proof (cases rule: subclseq_cases)
          case Eq
          with ws subcls_C_D
          show ?thesis
            by (auto dest: subcls_irrefl)
        next
          case Subcls
          with nsubcls_D_C
          show ?thesis
            by blast
        qed
      qed
    qed

    lemma subcls_superD:
     "[|G\<turnstile>C \<prec>C D; class G C = Some c|] ==> G\<turnstile>(super c) \<preceq>C D"
    proof -
      assume       clsC: "class G C = Some c"
      assume subcls_C_C: "G\<turnstile>C \<prec>C D"
      then obtain S where
                      "G\<turnstile>C \<prec>C1 S" and
        subclseq_S_D: "G\<turnstile>S \<preceq>C D"
        by (blast dest: tranclD)
      with clsC
      have "S=super c"
        by (auto dest: subcls1D)
      with subclseq_S_D show ?thesis by simp
    qed

    lemma subclseq_superD:
     "[|G\<turnstile>C \<preceq>C D; C≠D;class G C = Some c|] ==> G\<turnstile>(super c) \<preceq>C D"
    proof -
      assume neq_C_D: "C≠D"
      assume    clsC: "class G C = Some c"
      assume subclseq_C_D: "G\<turnstile>C \<preceq>C D"
      then show ?thesis
      proof (cases rule: subclseq_cases)
        case Eq with neq_C_D show ?thesis by contradiction
      next
        case Subcls
        with clsC show ?thesis by (blast dest: subcls_superD)
      qed
    qed

    section "implementation relation"

    defs
      --{* direct implementation, cf. 8.1.3 *}
    implmt1_def:"implmt1 G≡{(C,I). C≠Object ∧ (∃c∈class G C: I∈set (superIfs c))}"

    lemma implmt1D: "G\<turnstile>C\<leadsto>1I ==> C≠Object ∧ (∃c∈class G C: I∈set (superIfs c))"
    apply (unfold implmt1_def)
    apply auto
    done

    inductive "implmt G" intros                    --{* cf. 8.1.4 *}

      direct:         "G\<turnstile>C\<leadsto>1J              ==> G\<turnstile>C\<leadsto>J"
      subint:        "[|G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J|]  ==> G\<turnstile>C\<leadsto>J"
      subcls1:       "[|G\<turnstile>C\<prec>C1D; G\<turnstile>D\<leadsto>J |]  ==> G\<turnstile>C\<leadsto>J"

    lemma implmtD: "G\<turnstile>C\<leadsto>J ==> (∃I. G\<turnstile>C\<leadsto>1I ∧ G\<turnstile>I\<preceq>I J) ∨ (∃D. G\<turnstile>C\<prec>C1D ∧ G\<turnstile>D\<leadsto>J)"
    apply (erule implmt.induct)
    apply fast+
    done

    lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I ==> R"
    by (auto dest!: implmtD implmt1D subcls1D)

    lemma subcls_implmt [rule_format (no_asm)]: "G\<turnstile>A\<preceq>C B ==> G\<turnstile>B\<leadsto>K --> G\<turnstile>A\<leadsto>K"
    apply (erule rtrancl_induct)
    apply  (auto intro: implmt.subcls1)
    done

    lemma implmt_subint2: "[| G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K|] ==> G\<turnstile>A\<leadsto>K"
    apply (erule make_imp, erule implmt.induct)
    apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)
    done

    lemma implmt_is_class: "G\<turnstile>C\<leadsto>I ==> is_class G C"
    apply (erule implmt.induct)
    apply (blast dest: implmt1D subcls1D)+
    done

    section "widening relation"

    inductive "widen G" intros
     --{*widening, viz. method invocation conversion, cf. 5.3
                                i.e. kind of syntactic subtyping *}
      refl:    "G\<turnstile>T\<preceq>T" --{*identity conversion, cf. 5.1.1 *}
      subint:  "G\<turnstile>I\<preceq>I J  ==> G\<turnstile>Iface I\<preceq> Iface J" --{*wid.ref.conv.,cf. 5.1.4 *}
      int_obj: "G\<turnstile>Iface I\<preceq> Class Object"
      subcls:  "G\<turnstile>C\<preceq>C D  ==> G\<turnstile>Class C\<preceq> Class D"
      implmt:  "G\<turnstile>C\<leadsto>I   ==> G\<turnstile>Class C\<preceq> Iface I"
      null:    "G\<turnstile>NT\<preceq> RefT R"
      arr_obj: "G\<turnstile>T.[]\<preceq> Class Object"
      array:   "G\<turnstile>RefT S\<preceq>RefT T ==> G\<turnstile>RefT S.[]\<preceq> RefT T.[]"

    declare widen.refl [intro!]
    declare widen.intros [simp]

    (* too strong in general:
    lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T ==> T = PrimT x"
    *)
    lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T ==> (∃y. T = PrimT y)"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    (* too strong in general:
    lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x ==> S = PrimT x"
    *)
    lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x ==> ∃y. S = PrimT y"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    text {*
       These widening lemmata hold in Bali but are to strong for ordinary
       Java. They  would not work for real Java Integral Types, like short,
       long, int. These lemmata are just for documentation and are not used.
     *}

    lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T ==> T = PrimT x"
    by (ind_cases "G\<turnstile>S\<preceq>T") simp_all

    lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x ==> S = PrimT x"
    by (ind_cases "G\<turnstile>S\<preceq>T") simp_all

    text {* Specialized versions for booleans also would work for real Java *}

    lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T ==> T = PrimT Boolean"
    by (ind_cases "G\<turnstile>S\<preceq>T") simp_all

    lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean ==> S = PrimT Boolean"
    by (ind_cases "G\<turnstile>S\<preceq>T") simp_all

    lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> ∃t. T=RefT t"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> ∃t. S=RefT t"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T ==> T=Class Object ∨ (∃J. T=Iface J)"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J ==> S = NT ∨ (∃I. S = Iface I) ∨ (∃D. S = Class D)"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J ==> G\<turnstile>I\<preceq>I J"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"
    apply (rule iffI)
    apply  (erule widen_Iface_Iface)
    apply (erule widen.subint)
    done

    lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==>  (∃D. T=Class D) ∨ (∃I. T=Iface I)"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Class2: "G\<turnstile>S\<preceq> Class C ==> C = Object ∨ S = NT ∨ (∃D. S = Class D)"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm ==> G\<turnstile>C\<preceq>C cm"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>C cm"
    apply (rule iffI)
    apply  (erule widen_Class_Class)
    apply (erule widen.subcls)
    done

    lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I ==> G\<turnstile>C\<leadsto>I"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"
    apply (rule iffI)
    apply  (erule widen_Class_Iface)
    apply (erule widen.implmt)
    done

    lemma widen_Array: "G\<turnstile>S.[]\<preceq>T ==> T=Class Object ∨ (∃T'. T=T'.[] ∧ G\<turnstile>S\<preceq>T')"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] ==> S = NT ∨ (∃S'. S=S'.[] ∧ G\<turnstile>S'\<preceq>T)"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T ==> T=Class Object ∨ T=PrimT t.[]"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_ArrayRefT:
      "G\<turnstile>RefT t.[]\<preceq>T ==> T=Class Object ∨ (∃s. T=RefT s.[] ∧ G\<turnstile>RefT t\<preceq>RefT s)"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_ArrayRefT_ArrayRefT_eq [simp]:
      "G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'"
    apply (rule iffI)
    apply (drule widen_ArrayRefT)
    apply simp
    apply (erule widen.array)
    done

    lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] ==> G\<turnstile>T\<preceq>T'"
    apply (drule widen_Array)
    apply auto
    done

    lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C ==> C=Object"
    by (auto dest: widen_Array)

    lemma widen_NT2: "G\<turnstile>S\<preceq>NT ==> S = NT"
    apply (ind_cases "G\<turnstile>S\<preceq>T")
    by auto

    lemma widen_Object:"[|isrtype G T;ws_prog G|] ==> G\<turnstile>RefT T \<preceq> Class Object"
    apply (case_tac T)
    apply (auto)
    apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>C Object")
    apply (auto intro: subcls_ObjectI)
    done

    lemma widen_trans_lemma [rule_format (no_asm)]:
      "[|G\<turnstile>S\<preceq>U; ∀C. is_class G C --> G\<turnstile>C\<preceq>C Object|] ==> ∀T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T"
    apply (erule widen.induct)
    apply        safe
    prefer      5 apply (drule widen_RefT) apply clarsimp
    apply      (frule_tac [1] widen_Iface)
    apply      (frule_tac [2] widen_Class)
    apply      (frule_tac [3] widen_Class)
    apply      (frule_tac [4] widen_Iface)
    apply      (frule_tac [5] widen_Class)
    apply      (frule_tac [6] widen_Array)
    apply      safe
    apply            (rule widen.int_obj)
    prefer          6 apply (drule implmt_is_class) apply simp
    apply (tactic "ALLGOALS (etac thin_rl)")
    prefer         6 apply simp
    apply          (rule_tac [9] widen.arr_obj)
    apply         (rotate_tac [9] -1)
    apply         (frule_tac [9] widen_RefT)
    apply         (auto elim!: rtrancl_trans subcls_implmt implmt_subint2)
    done

    lemma ws_widen_trans: "[|G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G|] ==> G\<turnstile>S\<preceq>T"
    by (auto intro: widen_trans_lemma subcls_ObjectI)

    lemma widen_antisym_lemma [rule_format (no_asm)]: "[|G\<turnstile>S\<preceq>T;
     ∀I J. G\<turnstile>I\<preceq>I J ∧ G\<turnstile>J\<preceq>I I --> I = J;
     ∀C D. G\<turnstile>C\<preceq>C D ∧ G\<turnstile>D\<preceq>C C --> C = D;
     ∀I  . G\<turnstile>Object\<leadsto>I        --> False|] ==> G\<turnstile>T\<preceq>S --> S = T"
    apply (erule widen.induct)
    apply (auto dest: widen_Iface widen_NT2 widen_Class)
    done

    lemmas subint_antisym =
           subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
    lemmas subcls_antisym =
           subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]

    lemma widen_antisym: "[|G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G|] ==> S=T"
    by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD]
                                       subcls_antisym [THEN antisymD])

    lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T ==> T=Class Object"
    apply (frule widen_Class)
    apply (fast dest: widen_Class_Class widen_Class_Iface)
    done

    constdefs
      widens :: "prog => [ty list, ty list] => bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
     "G\<turnstile>Ts[\<preceq>]Ts' ≡ list_all2 (λT T'. G\<turnstile>T\<preceq>T') Ts Ts'"

    lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
    apply (unfold widens_def)
    apply auto
    done

    lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T ∧ G\<turnstile>Ss[\<preceq>]Ts)"
    apply (unfold widens_def)
    apply auto
    done

    section "narrowing relation"

    (* all properties of narrowing and casting conversions we actually need *)
    (* these can easily be proven from the definitions below *)
    (*
    rules
      cast_RefT2   "G\<turnstile>S\<preceq>? RefT R   ==> ∃t. S=RefT t"
      cast_PrimT2  "G\<turnstile>S\<preceq>? PrimT pt ==> ∃t. S=PrimT t ∧ G\<turnstile>PrimT t\<preceq>PrimT pt"
    *)

    (* more detailed than necessary for type-safety, see above rules. *)
    inductive "narrow G" intros (* narrowing reference conversion, cf. 5.1.5 *)

      subcls:  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>     Class D\<succ>Class C"
      implmt:  "¬G\<turnstile>C\<leadsto>I ==> G\<turnstile>     Class C\<succ>Iface I"
      obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
      int_cls: "G\<turnstile>     Iface I\<succ>Class C"
      subint:  "imethds G I hidings imethds G J entails
               (λ(md, mh   ) (md',mh').  G\<turnstile>mrt mh\<preceq>mrt mh') ==>
               ¬G\<turnstile>I\<preceq>I J               ==> G\<turnstile>     Iface I\<succ>Iface J"
      array:   "G\<turnstile>RefT S\<succ>RefT T     ==> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"

    (*unused*)
    lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T ==> ∃t. T=RefT t"
    apply (ind_cases "G\<turnstile>S\<succ>T")
    by auto

    lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R ==> ∃t. S=RefT t"
    apply (ind_cases "G\<turnstile>S\<succ>T")
    by auto

    (*unused*)
    lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T ==> ∃t. T=PrimT t"
    apply (ind_cases "G\<turnstile>S\<succ>T")
    by auto

    lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt ==>
                                      ∃t. S=PrimT t ∧ G\<turnstile>PrimT t\<preceq>PrimT pt"
    apply (ind_cases "G\<turnstile>S\<succ>T")
    by auto

    text {*
       These narrowing lemmata hold in Bali but are to strong for ordinary
       Java. They  would not work for real Java Integral Types, like short,
       long, int. These lemmata are just for documentation and are not used.
     *}
    lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T ==> T=PrimT pt"
    by (ind_cases "G\<turnstile>S\<succ>T") simp_all

    lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt ==> S=PrimT pt"
    by (ind_cases "G\<turnstile>S\<succ>T") simp_all

    text {* Specialized versions for booleans also would work for real Java *}

    lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T ==> T=PrimT Boolean"
    by (ind_cases "G\<turnstile>S\<succ>T") simp_all

    lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean ==> S=PrimT Boolean"
    by (ind_cases "G\<turnstile>S\<succ>T") simp_all

    section "casting relation"

    inductive "cast G" intros --{* casting conversion, cf. 5.5 *}

      widen:   "G\<turnstile>S\<preceq>T ==> G\<turnstile>S\<preceq>? T"
      narrow:  "G\<turnstile>S\<succ>T ==> G\<turnstile>S\<preceq>? T"

    (*unused*)
    lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T ==> ∃t. T=RefT t"
    apply (ind_cases "G\<turnstile>S\<preceq>? T")
    by (auto dest: widen_RefT narrow_RefT)

    lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R ==> ∃t. S=RefT t"
    apply (ind_cases "G\<turnstile>S\<preceq>? T")
    by (auto dest: widen_RefT2 narrow_RefT2)

    (*unused*)
    lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T ==> ∃t. T=PrimT t"
    apply (ind_cases "G\<turnstile>S\<preceq>? T")
    by (auto dest: widen_PrimT narrow_PrimT)

    lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt ==> ∃t. S=PrimT t ∧ G\<turnstile>PrimT t\<preceq>PrimT pt"
    apply (ind_cases "G\<turnstile>S\<preceq>? T")
    by (auto dest: widen_PrimT2 narrow_PrimT2)

    lemma cast_Boolean:
      assumes bool_cast: "G\<turnstile>PrimT Boolean\<preceq>? T"
      shows "T=PrimT Boolean"
    using bool_cast
    proof (cases)
      case widen
      hence "G\<turnstile>PrimT Boolean\<preceq> T"
        by simp
      thus ?thesis by  (rule widen_Boolean)
    next
      case narrow
      hence "G\<turnstile>PrimT Boolean\<succ>T"
        by simp
      thus ?thesis by (rule narrow_Boolean)
    qed

    lemma cast_Boolean2:
      assumes bool_cast: "G\<turnstile>S\<preceq>? PrimT Boolean"
      shows "S = PrimT Boolean"
    using bool_cast
    proof (cases)
      case widen
      hence "G\<turnstile>S\<preceq> PrimT Boolean"
        by simp
      thus ?thesis by  (rule widen_Boolean2)
    next
      case narrow
      hence "G\<turnstile>S\<succ>PrimT Boolean"
        by simp
      thus ?thesis by (rule narrow_Boolean2)
    qed

    end

## subclass and subinterface relations

lemmas subcls_direct:

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

lemmas subcls_direct:

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

lemma subcls_direct1:

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

lemma subcls1I1:

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

lemma subcls_direct2:

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

lemma subclseq_trans:

      [| G|-A<=:C B; G|-B<=:C C |] ==> G|-A<=:C C

lemma subcls_trans:

      [| G|-A<:C B; G|-B<:C C |] ==> G|-A<:C C

lemma SXcpt_subcls_Throwable_lemma:

      [| class G (SXcpt xn) = Some xc;
         super xc = (if xn = Throwable then Object else SXcpt Throwable) |]
      ==> G|-SXcpt xn<=:C SXcpt Throwable

lemma subcls_ObjectI:

      [| is_class G C; ws_prog G |] ==> G|-C<=:C Object

lemma subclseq_ObjectD:

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

lemma subcls_ObjectD:

      G|-Object<:C C ==> False

lemma subcls_ObjectI1:

      [| C ≠ Object; is_class G C; ws_prog G |] ==> G|-C<:C Object

lemma subcls_is_class:

      G|-C<:C D ==> is_class G C

lemma subcls_is_class2:

      [| G|-C<=:C D; is_class G D |] ==> is_class G C

lemma single_inheritance:

      [| G|-A<:C1B; G|-A<:C1C |] ==> B = C

lemma subcls_compareable:

      [| G|-A<=:C X; G|-A<=:C Y |] ==> G|-X<=:C Y ∨ G|-Y<=:C X

lemma subcls1_irrefl:

      [| G|-C<:C1D; ws_prog G |] ==> C ≠ D

lemma no_subcls_Object:

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

lemma subcls_acyclic:

      [| G|-C<:C D; ws_prog G |] ==> (D, C) ∉ (subcls1 G)+

lemma subclseq_cases:

      [| G|-C<=:C D; C = D ==> P; G|-C<:C D ==> P |] ==> P

lemma subclseq_acyclic:

      [| G|-C<=:C D; G|-D<=:C C; ws_prog G |] ==> C = D

lemma subcls_irrefl:

      [| G|-C<:C D; ws_prog G |] ==> C ≠ D

lemma invert_subclseq:

      [| G|-C<=:C D; ws_prog G |] ==> (D, C) ∉ (subcls1 G)+

lemma invert_subcls:

      [| G|-C<:C D; ws_prog G |] ==> (D, C) ∉ (subcls1 G)*

lemma subcls_superD:

      [| G|-C<:C D; class G C = Some c |] ==> G|-super c<=:C D

lemma subclseq_superD:

      [| G|-C<=:C D; C ≠ D; class G C = Some c |] ==> G|-super c<=:C D

## implementation relation

lemma implmt1D:

      G|-C~>1I ==> C ≠ Object ∧ (? c:class G C: I ∈ set (superIfs c))

lemma implmtD:

      G|-C~>J ==> (∃I. G|-C~>1I ∧ G|-I<=:I J) ∨ (∃D. G|-C<:C1D ∧ G|-D~>J)

lemma implmt_ObjectE:

      G|-Object~>I ==> R

lemma subcls_implmt:

      [| G|-A<=:C B; G|-B~>K |] ==> G|-A~>K

lemma implmt_subint2:

      [| G|-A~>J; G|-J<=:I K |] ==> G|-A~>K

lemma implmt_is_class:

      G|-C~>I ==> is_class G C

## widening relation

lemma widen_PrimT:

      G|-PrimT x<=:T ==> ∃y. T = PrimT y

lemma widen_PrimT2:

      G|-S<=:PrimT x ==> ∃y. S = PrimT y

lemma widen_PrimT_strong:

      G|-PrimT x<=:T ==> T = PrimT x

lemma widen_PrimT2_strong:

      G|-S<=:PrimT x ==> S = PrimT x

lemma widen_Boolean:

      G|-PrimT Boolean<=:T ==> T = PrimT Boolean

lemma widen_Boolean2:

      G|-S<=:PrimT Boolean ==> S = PrimT Boolean

lemma widen_RefT:

      G|-RefT R<=:T ==> ∃t. T = RefT t

lemma widen_RefT2:

      G|-S<=:RefT R ==> ∃t. S = RefT t

lemma widen_Iface:

      G|-Iface I<=:T ==> T = Class Object ∨ (∃J. T = Iface J)

lemma widen_Iface2:

      G|-S<=:Iface J ==> S = NT ∨ (∃I. S = Iface I) ∨ (∃D. S = Class D)

lemma widen_Iface_Iface:

      G|-Iface I<=:Iface J ==> G|-I<=:I J

lemma widen_Iface_Iface_eq:

      G|-Iface I<=:Iface J = G|-I<=:I J

lemma widen_Class:

      G|-Class C<=:T ==> (∃D. T = Class D) ∨ (∃I. T = Iface I)

lemma widen_Class2:

      G|-S<=:Class C ==> C = Object ∨ S = NT ∨ (∃D. S = Class D)

lemma widen_Class_Class:

      G|-Class C<=:Class cm ==> G|-C<=:C cm

lemma widen_Class_Class_eq:

      G|-Class C<=:Class cm = G|-C<=:C cm

lemma widen_Class_Iface:

      G|-Class C<=:Iface I ==> G|-C~>I

lemma widen_Class_Iface_eq:

      G|-Class C<=:Iface I = G|-C~>I

lemma widen_Array:

      G|-S.[]<=:T ==> T = Class Object ∨ (∃T'. T = T'.[] ∧ G|-S<=:T')

lemma widen_Array2:

      G|-S<=:T.[] ==> S = NT ∨ (∃S'. S = S'.[] ∧ G|-S'<=:T)

lemma widen_ArrayPrimT:

      G|-PrimT t.[]<=:T ==> T = Class Object ∨ T = PrimT t.[]

lemma widen_ArrayRefT:

      G|-RefT t.[]<=:T ==> T = Class Object ∨ (∃s. T = RefT s.[] ∧ G|-RefT t<=:RefT s)

lemma widen_ArrayRefT_ArrayRefT_eq:

      G|-RefT T.[]<=:RefT T'.[] = G|-RefT T<=:RefT T'

lemma widen_Array_Array:

      G|-T.[]<=:T'.[] ==> G|-T<=:T'

lemma widen_Array_Class:

      G|-S.[]<=:Class C ==> C = Object

lemma widen_NT2:

      G|-S<=:NT ==> S = NT

lemma widen_Object:

      [| isrtype G T; ws_prog G |] ==> G|-RefT T<=:Class Object

lemma widen_trans_lemma:

      [| G|-S<=:U; ∀C. is_class G C --> G|-C<=:C Object; G|-U<=:T |] ==> G|-S<=:T

lemma ws_widen_trans:

      [| G|-S<=:U; G|-U<=:T; ws_prog G |] ==> G|-S<=:T

lemma widen_antisym_lemma:

      [| G|-S<=:T; ∀I J. G|-I<=:I J ∧ G|-J<=:I I --> I = J;
         ∀C D. G|-C<=:C D ∧ G|-D<=:C C --> C = D; ∀I. G|-Object~>I --> False;
         G|-T<=:S |]
      ==> S = T

lemmas subint_antisym:

      ws_prog G ==> antisym ((subint1 G)*)

lemmas subint_antisym:

      ws_prog G ==> antisym ((subint1 G)*)

lemmas subcls_antisym:

      ws_prog G ==> antisym ((subcls1 G)*)

lemmas subcls_antisym:

      ws_prog G ==> antisym ((subcls1 G)*)

lemma widen_antisym:

      [| G|-S<=:T; G|-T<=:S; ws_prog G |] ==> S = T

lemma widen_ObjectD:

      G|-Class Object<=:T ==> T = Class Object

lemma widens_Nil:

      G\<turnstile>[][\<preceq>][]

lemma widens_Cons:

      G\<turnstile>(S # Ss)[\<preceq>](T # Ts) =
      (G|-S<=:T ∧ G\<turnstile>Ss[\<preceq>]Ts)

## narrowing relation

lemma narrow_RefT:

      G|-RefT R:>T ==> ∃t. T = RefT t

lemma narrow_RefT2:

      G|-S:>RefT R ==> ∃t. S = RefT t

lemma narrow_PrimT:

      G|-PrimT pt:>T ==> ∃t. T = PrimT t

lemma narrow_PrimT2:

      G|-S:>PrimT pt ==> ∃t. S = PrimT t ∧ G|-PrimT t<=:PrimT pt

lemma narrow_PrimT_strong:

      G|-PrimT pt:>T ==> T = PrimT pt

lemma narrow_PrimT2_strong:

      G|-S:>PrimT pt ==> S = PrimT pt

lemma narrow_Boolean:

      G|-PrimT Boolean:>T ==> T = PrimT Boolean

lemma narrow_Boolean2:

      G|-S:>PrimT Boolean ==> S = PrimT Boolean

## casting relation

lemma cast_RefT:

      G|-RefT R<=:? T ==> ∃t. T = RefT t

lemma cast_RefT2:

      G|-S<=:? RefT R ==> ∃t. S = RefT t

lemma cast_PrimT:

      G|-PrimT pt<=:? T ==> ∃t. T = PrimT t

lemma cast_PrimT2:

      G|-S<=:? PrimT pt ==> ∃t. S = PrimT t ∧ G|-PrimT t<=:PrimT pt

lemma cast_Boolean:

      G|-PrimT Boolean<=:? T ==> T = PrimT Boolean

lemma cast_Boolean2:

      G|-S<=:? PrimT Boolean ==> S = PrimT Boolean