src/HOL/Bali/TypeRel.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01)
changeset 35416 d8d7d1b785af
parent 35069 09154b995ed8
child 37956 ee939247b2fb
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
     1 (*  Title:      HOL/Bali/TypeRel.thy
     2     Author:     David von Oheimb
     3 *)
     4 header {* The relations between Java types *}
     5 
     6 theory TypeRel imports Decl begin
     7 
     8 text {*
     9 simplifications:
    10 \begin{itemize}
    11 \item subinterface, subclass and widening relation includes identity
    12 \end{itemize}
    13 improvements over Java Specification 1.0:
    14 \begin{itemize}
    15 \item narrowing reference conversion also in cases where the return types of a 
    16       pair of methods common to both types are in widening (rather identity) 
    17       relation
    18 \item one could add similar constraints also for other cases
    19 \end{itemize}
    20 design issues:
    21 \begin{itemize}
    22 \item the type relations do not require @{text is_type} for their arguments
    23 \item the subint1 and subcls1 relations imply @{text is_iface}/@{text is_class}
    24       for their first arguments, which is required for their finiteness
    25 \end{itemize}
    26 *}
    27 
    28 consts
    29 
    30 (*subint1, in Decl.thy*)                     (* direct subinterface       *)
    31 (*subint , by translation*)                  (* subinterface (+ identity) *)
    32 (*subcls1, in Decl.thy*)                     (* direct subclass           *)
    33 (*subcls , by translation*)                  (*        subclass           *)
    34 (*subclseq, by translation*)                 (* subclass + identity       *)
    35   implmt1   :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
    36 
    37 abbreviation
    38   subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
    39   where "G|-I <:I1 J == (I,J) \<in> subint1 G"
    40 
    41 abbreviation
    42   subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
    43   where "G|-I <=:I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
    44 
    45 abbreviation
    46   implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
    47   where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
    48 
    49 notation (xsymbols)
    50   subint1_syntax  ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70) and
    51   subint_syntax  ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70) and
    52   implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
    53 
    54 
    55 section "subclass and subinterface relations"
    56 
    57   (* direct subinterface in Decl.thy, cf. 9.1.3 *)
    58   (* direct subclass     in Decl.thy, cf. 8.1.3 *)
    59 
    60 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]
    61 
    62 lemma subcls_direct1:
    63  "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D"
    64 apply (auto dest: subcls_direct)
    65 done
    66 
    67 lemma subcls1I1:
    68  "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C1 D"
    69 apply (auto dest: subcls1I)
    70 done
    71 
    72 lemma subcls_direct2:
    73  "\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>\<^sub>C D"
    74 apply (auto dest: subcls1I1)
    75 done
    76 
    77 lemma subclseq_trans: "\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C B; G\<turnstile>B \<preceq>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<preceq>\<^sub>C C"
    78 by (blast intro: rtrancl_trans)
    79 
    80 lemma subcls_trans: "\<lbrakk>G\<turnstile>A \<prec>\<^sub>C B; G\<turnstile>B \<prec>\<^sub>C C\<rbrakk> \<Longrightarrow> G\<turnstile>A \<prec>\<^sub>C C"
    81 by (blast intro: trancl_trans)
    82 
    83 lemma SXcpt_subcls_Throwable_lemma: 
    84 "\<lbrakk>class G (SXcpt xn) = Some xc;
    85   super xc = (if xn = Throwable then Object else  SXcpt Throwable)\<rbrakk> 
    86 \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
    87 apply (case_tac "xn = Throwable")
    88 apply  simp_all
    89 apply (drule subcls_direct)
    90 apply (auto dest: sym)
    91 done
    92 
    93 lemma subcls_ObjectI: "\<lbrakk>is_class G C; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object"
    94 apply (erule ws_subcls1_induct)
    95 apply clarsimp
    96 apply (case_tac "C = Object")
    97 apply  (fast intro: r_into_rtrancl [THEN rtrancl_trans])+
    98 done
    99 
   100 lemma subclseq_ObjectD [dest!]: "G\<turnstile>Object\<preceq>\<^sub>C C \<Longrightarrow> C = Object"
   101 apply (erule rtrancl_induct)
   102 apply  (auto dest: subcls1D)
   103 done
   104 
   105 lemma subcls_ObjectD [dest!]: "G\<turnstile>Object\<prec>\<^sub>C C \<Longrightarrow> False"
   106 apply (erule trancl_induct)
   107 apply  (auto dest: subcls1D)
   108 done
   109 
   110 lemma subcls_ObjectI1 [intro!]: 
   111  "\<lbrakk>C \<noteq> Object;is_class G C;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>C \<prec>\<^sub>C Object" 
   112 apply (drule (1) subcls_ObjectI)
   113 apply (auto intro: rtrancl_into_trancl3)
   114 done
   115 
   116 lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ \<Longrightarrow> is_class G C"
   117 apply (erule trancl_trans_induct)
   118 apply (auto dest!: subcls1D)
   119 done
   120 
   121 lemma subcls_is_class2 [rule_format (no_asm)]: 
   122  "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
   123 apply (erule rtrancl_induct)
   124 apply (drule_tac [2] subcls1D)
   125 apply  auto
   126 done
   127 
   128 lemma single_inheritance: 
   129 "\<lbrakk>G\<turnstile>A \<prec>\<^sub>C1 B; G\<turnstile>A \<prec>\<^sub>C1 C\<rbrakk> \<Longrightarrow> B = C"
   130 by (auto simp add: subcls1_def)
   131   
   132 lemma subcls_compareable:
   133 "\<lbrakk>G\<turnstile>A \<preceq>\<^sub>C X; G\<turnstile>A \<preceq>\<^sub>C Y 
   134  \<rbrakk> \<Longrightarrow> G\<turnstile>X \<preceq>\<^sub>C Y \<or> G\<turnstile>Y \<preceq>\<^sub>C X"
   135 by (rule triangle_lemma)  (auto intro: single_inheritance) 
   136 
   137 lemma subcls1_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C1 D; ws_prog G \<rbrakk>
   138  \<Longrightarrow> C \<noteq> D"
   139 proof 
   140   assume ws: "ws_prog G" and
   141     subcls1: "G\<turnstile>C \<prec>\<^sub>C1 D" and
   142      eq_C_D: "C=D"
   143   from subcls1 obtain c 
   144     where
   145       neq_C_Object: "C\<noteq>Object" and
   146               clsC: "class G C = Some c" and
   147            super_c: "super c = D"
   148     by (auto simp add: subcls1_def)
   149   with super_c subcls1 eq_C_D 
   150   have subcls_super_c_C: "G\<turnstile>super c \<prec>\<^sub>C C"
   151     by auto
   152   from ws clsC neq_C_Object 
   153   have "\<not> G\<turnstile>super c \<prec>\<^sub>C C"
   154     by (auto dest: ws_prog_cdeclD)
   155   from this subcls_super_c_C 
   156   show "False"
   157     by (rule notE)
   158 qed
   159 
   160 lemma no_subcls_Object: "G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> C \<noteq> Object"
   161 by (erule converse_trancl_induct) (auto dest: subcls1D)
   162 
   163 lemma subcls_acyclic: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk> \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"
   164 proof -
   165   assume         ws: "ws_prog G"
   166   assume subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"
   167   then show ?thesis
   168   proof (induct rule: converse_trancl_induct)
   169     fix C
   170     assume subcls1_C_D: "G\<turnstile>C \<prec>\<^sub>C1 D"
   171     then obtain c  where
   172         "C\<noteq>Object" and
   173         "class G C = Some c" and
   174         "super c = D"
   175       by (auto simp add: subcls1_def)
   176     with ws 
   177     show "\<not> G\<turnstile>D \<prec>\<^sub>C C"
   178       by (auto dest: ws_prog_cdeclD)
   179   next
   180     fix C Z
   181     assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C1 Z" and
   182             subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and
   183            nsubcls_D_Z: "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
   184     show "\<not> G\<turnstile>D \<prec>\<^sub>C C"
   185     proof
   186       assume subcls_D_C: "G\<turnstile>D \<prec>\<^sub>C C"
   187       show "False"
   188       proof -
   189         from subcls_D_C subcls1_C_Z
   190         have "G\<turnstile>D \<prec>\<^sub>C Z"
   191           by (auto dest: r_into_trancl trancl_trans)
   192         with nsubcls_D_Z
   193         show ?thesis
   194           by (rule notE)
   195       qed
   196     qed
   197   qed  
   198 qed
   199 
   200 lemma subclseq_cases [consumes 1, case_names Eq Subcls]:
   201  "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   202 by (blast intro: rtrancl_cases)
   203 
   204 lemma subclseq_acyclic: 
   205  "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D"
   206 by (auto elim: subclseq_cases dest: subcls_acyclic)
   207 
   208 lemma subcls_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
   209  \<Longrightarrow> C \<noteq> D"
   210 proof -
   211   assume     ws: "ws_prog G"
   212   assume subcls: "G\<turnstile>C \<prec>\<^sub>C D"
   213   then show ?thesis
   214   proof (induct rule: converse_trancl_induct)
   215     fix C
   216     assume "G\<turnstile>C \<prec>\<^sub>C1 D"
   217     with ws 
   218     show "C\<noteq>D" 
   219       by (blast dest: subcls1_irrefl)
   220   next
   221     fix C Z
   222     assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C1 Z" and
   223             subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and
   224                neq_Z_D: "Z \<noteq> D"
   225     show "C\<noteq>D"
   226     proof
   227       assume eq_C_D: "C=D"
   228       show "False"
   229       proof -
   230         from subcls1_C_Z eq_C_D 
   231         have "G\<turnstile>D \<prec>\<^sub>C Z"
   232           by (auto)
   233         also
   234         from subcls_Z_D ws   
   235         have "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
   236           by (rule subcls_acyclic)
   237         ultimately 
   238         show ?thesis 
   239           by - (rule notE)
   240       qed
   241     qed
   242   qed
   243 qed
   244 
   245 lemma invert_subclseq:
   246 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; ws_prog G\<rbrakk>
   247  \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"
   248 proof -
   249   assume       ws: "ws_prog G" and
   250      subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D"
   251   show ?thesis
   252   proof (cases "D=C")
   253     case True
   254     with ws 
   255     show ?thesis 
   256       by (auto dest: subcls_irrefl)
   257   next
   258     case False
   259     with subclseq_C_D 
   260     have "G\<turnstile>C \<prec>\<^sub>C D"
   261       by (blast intro: rtrancl_into_trancl3) 
   262     with ws 
   263     show ?thesis 
   264       by (blast dest: subcls_acyclic)
   265   qed
   266 qed
   267 
   268 lemma invert_subcls:
   269 "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
   270  \<Longrightarrow> \<not> G\<turnstile>D \<preceq>\<^sub>C C"
   271 proof -
   272   assume        ws: "ws_prog G" and
   273         subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"
   274   then 
   275   have nsubcls_D_C: "\<not> G\<turnstile>D \<prec>\<^sub>C C"
   276     by (blast dest: subcls_acyclic)
   277   show ?thesis
   278   proof
   279     assume "G\<turnstile>D \<preceq>\<^sub>C C"
   280     then show "False"
   281     proof (cases rule: subclseq_cases)
   282       case Eq
   283       with ws subcls_C_D
   284       show ?thesis 
   285         by (auto dest: subcls_irrefl)
   286     next
   287       case Subcls
   288       with nsubcls_D_C
   289       show ?thesis
   290         by blast
   291     qed
   292   qed
   293 qed
   294 
   295 lemma subcls_superD:
   296  "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D"
   297 proof -
   298   assume       clsC: "class G C = Some c"
   299   assume subcls_C_C: "G\<turnstile>C \<prec>\<^sub>C D"
   300   then obtain S where 
   301                   "G\<turnstile>C \<prec>\<^sub>C1 S" and
   302     subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D"
   303     by (blast dest: tranclD)
   304   with clsC 
   305   have "S=super c" 
   306     by (auto dest: subcls1D)
   307   with subclseq_S_D show ?thesis by simp
   308 qed
   309  
   310 
   311 lemma subclseq_superD:
   312  "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C\<noteq>D;class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D"
   313 proof -
   314   assume neq_C_D: "C\<noteq>D"
   315   assume    clsC: "class G C = Some c"
   316   assume subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" 
   317   then show ?thesis
   318   proof (cases rule: subclseq_cases)
   319     case Eq with neq_C_D show ?thesis by contradiction
   320   next
   321     case Subcls
   322     with clsC show ?thesis by (blast dest: subcls_superD)
   323   qed
   324 qed
   325 
   326 section "implementation relation"
   327 
   328 defs
   329   --{* direct implementation, cf. 8.1.3 *}
   330 implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
   331 
   332 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
   333 apply (unfold implmt1_def)
   334 apply auto
   335 done
   336 
   337 
   338 inductive --{* implementation, cf. 8.1.4 *}
   339   implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   340   for G :: prog
   341 where
   342   direct:         "G\<turnstile>C\<leadsto>1J     \<spacespace>\<spacespace>     \<Longrightarrow> G\<turnstile>C\<leadsto>J"
   343 | subint:        "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
   344 | subcls1:       "\<lbrakk>G\<turnstile>C\<prec>\<^sub>C1D; G\<turnstile>D\<leadsto>J \<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
   345 
   346 lemma implmtD: "G\<turnstile>C\<leadsto>J \<Longrightarrow> (\<exists>I. G\<turnstile>C\<leadsto>1I \<and> G\<turnstile>I\<preceq>I J) \<or> (\<exists>D. G\<turnstile>C\<prec>\<^sub>C1D \<and> G\<turnstile>D\<leadsto>J)" 
   347 apply (erule implmt.induct)
   348 apply fast+
   349 done
   350 
   351 lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R"
   352 by (auto dest!: implmtD implmt1D subcls1D)
   353 
   354 lemma subcls_implmt [rule_format (no_asm)]: "G\<turnstile>A\<preceq>\<^sub>C B \<Longrightarrow> G\<turnstile>B\<leadsto>K \<longrightarrow> G\<turnstile>A\<leadsto>K"
   355 apply (erule rtrancl_induct)
   356 apply  (auto intro: implmt.subcls1)
   357 done
   358 
   359 lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K"
   360 apply (erule rev_mp, erule implmt.induct)
   361 apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)
   362 done
   363 
   364 lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C"
   365 apply (erule implmt.induct)
   366 apply (auto dest: implmt1D subcls1D)
   367 done
   368 
   369 
   370 section "widening relation"
   371 
   372 inductive
   373  --{*widening, viz. method invocation conversion, cf. 5.3
   374                             i.e. kind of syntactic subtyping *}
   375   widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
   376   for G :: prog
   377 where
   378   refl:    "G\<turnstile>T\<preceq>T" --{*identity conversion, cf. 5.1.1 *}
   379 | subint:  "G\<turnstile>I\<preceq>I J  \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J" --{*wid.ref.conv.,cf. 5.1.4 *}
   380 | int_obj: "G\<turnstile>Iface I\<preceq> Class Object"
   381 | subcls:  "G\<turnstile>C\<preceq>\<^sub>C D  \<Longrightarrow> G\<turnstile>Class C\<preceq> Class D"
   382 | implmt:  "G\<turnstile>C\<leadsto>I   \<Longrightarrow> G\<turnstile>Class C\<preceq> Iface I"
   383 | null:    "G\<turnstile>NT\<preceq> RefT R"
   384 | arr_obj: "G\<turnstile>T.[]\<preceq> Class Object"
   385 | array:   "G\<turnstile>RefT S\<preceq>RefT T \<Longrightarrow> G\<turnstile>RefT S.[]\<preceq> RefT T.[]"
   386 
   387 declare widen.refl [intro!]
   388 declare widen.intros [simp]
   389 
   390 (* too strong in general:
   391 lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
   392 *)
   393 lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)"
   394 apply (ind_cases "G\<turnstile>PrimT x\<preceq>T")
   395 by auto
   396 
   397 (* too strong in general:
   398 lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
   399 *)
   400 lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
   401 apply (ind_cases "G\<turnstile>S\<preceq>PrimT x")
   402 by auto
   403 
   404 text {* 
   405    These widening lemmata hold in Bali but are to strong for ordinary
   406    Java. They  would not work for real Java Integral Types, like short, 
   407    long, int. These lemmata are just for documentation and are not used.
   408  *}
   409 
   410 lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
   411 by (ind_cases "G\<turnstile>PrimT x\<preceq>T") simp_all
   412 
   413 lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
   414 by (ind_cases "G\<turnstile>S\<preceq>PrimT x") simp_all
   415 
   416 text {* Specialized versions for booleans also would work for real Java *}
   417 
   418 lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean"
   419 by (ind_cases "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
   420 
   421 lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean"
   422 by (ind_cases "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
   423 
   424 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"
   425 apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
   426 by auto
   427 
   428 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   429 apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
   430 by auto
   431 
   432 lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
   433 apply (ind_cases "G\<turnstile>Iface I\<preceq>T")
   434 by auto
   435 
   436 lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)"
   437 apply (ind_cases "G\<turnstile>S\<preceq> Iface J")
   438 by auto
   439 
   440 lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"
   441 apply (ind_cases "G\<turnstile>Iface I\<preceq> Iface J")
   442 by auto
   443 
   444 lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"
   445 apply (rule iffI)
   446 apply  (erule widen_Iface_Iface)
   447 apply (erule widen.subint)
   448 done
   449 
   450 lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow>  (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
   451 apply (ind_cases "G\<turnstile>Class C\<preceq>T")
   452 by auto
   453 
   454 lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"
   455 apply (ind_cases "G\<turnstile>S\<preceq> Class C")
   456 by auto
   457 
   458 lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm"
   459 apply (ind_cases "G\<turnstile>Class C\<preceq> Class cm")
   460 by auto
   461 
   462 lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm"
   463 apply (rule iffI)
   464 apply  (erule widen_Class_Class)
   465 apply (erule widen.subcls)
   466 done
   467 
   468 lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"
   469 apply (ind_cases "G\<turnstile>Class C\<preceq> Iface I")
   470 by auto
   471 
   472 lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"
   473 apply (rule iffI)
   474 apply  (erule widen_Class_Iface)
   475 apply (erule widen.implmt)
   476 done
   477 
   478 lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
   479 apply (ind_cases "G\<turnstile>S.[]\<preceq>T")
   480 by auto
   481 
   482 lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
   483 apply (ind_cases "G\<turnstile>S\<preceq>T.[]")
   484 by auto
   485 
   486 
   487 lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
   488 apply (ind_cases "G\<turnstile>PrimT t.[]\<preceq>T")
   489 by auto
   490 
   491 lemma widen_ArrayRefT: 
   492   "G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
   493 apply (ind_cases "G\<turnstile>RefT t.[]\<preceq>T")
   494 by auto
   495 
   496 lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 
   497   "G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'"
   498 apply (rule iffI)
   499 apply (drule widen_ArrayRefT)
   500 apply simp
   501 apply (erule widen.array)
   502 done
   503 
   504 lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'"
   505 apply (drule widen_Array)
   506 apply auto
   507 done
   508 
   509 lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C \<Longrightarrow> C=Object"
   510 by (auto dest: widen_Array)
   511 
   512 
   513 lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
   514 apply (ind_cases "G\<turnstile>S\<preceq>NT")
   515 by auto
   516 
   517 lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
   518 apply (case_tac T)
   519 apply (auto)
   520 apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object")
   521 apply (auto intro: subcls_ObjectI)
   522 done
   523 
   524 lemma widen_trans_lemma [rule_format (no_asm)]: 
   525   "\<lbrakk>G\<turnstile>S\<preceq>U; \<forall>C. is_class G C \<longrightarrow> G\<turnstile>C\<preceq>\<^sub>C Object\<rbrakk> \<Longrightarrow> \<forall>T. G\<turnstile>U\<preceq>T \<longrightarrow> G\<turnstile>S\<preceq>T"
   526 apply (erule widen.induct)
   527 apply        safe
   528 prefer      5 apply (drule widen_RefT) apply clarsimp
   529 apply      (frule_tac [1] widen_Iface)
   530 apply      (frule_tac [2] widen_Class)
   531 apply      (frule_tac [3] widen_Class)
   532 apply      (frule_tac [4] widen_Iface)
   533 apply      (frule_tac [5] widen_Class)
   534 apply      (frule_tac [6] widen_Array)
   535 apply      safe
   536 apply            (rule widen.int_obj)
   537 prefer          6 apply (drule implmt_is_class) apply simp
   538 apply (tactic "ALLGOALS (etac thin_rl)")
   539 prefer         6 apply simp
   540 apply          (rule_tac [9] widen.arr_obj)
   541 apply         (rotate_tac [9] -1)
   542 apply         (frule_tac [9] widen_RefT)
   543 apply         (auto elim!: rtrancl_trans subcls_implmt implmt_subint2)
   544 done
   545 
   546 lemma ws_widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   547 by (auto intro: widen_trans_lemma subcls_ObjectI)
   548 
   549 lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T;  
   550  \<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J;  
   551  \<forall>C D. G\<turnstile>C\<preceq>\<^sub>C D \<and> G\<turnstile>D\<preceq>\<^sub>C C \<longrightarrow> C = D;  
   552  \<forall>I  . G\<turnstile>Object\<leadsto>I        \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T"
   553 apply (erule widen.induct)
   554 apply (auto dest: widen_Iface widen_NT2 widen_Class)
   555 done
   556 
   557 lemmas subint_antisym = 
   558        subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
   559 lemmas subcls_antisym = 
   560        subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
   561 
   562 lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
   563 by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 
   564                                    subcls_antisym [THEN antisymD])
   565 
   566 lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object"
   567 apply (frule widen_Class)
   568 apply (fast dest: widen_Class_Class widen_Class_Iface)
   569 done
   570 
   571 definition widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) where
   572  "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
   573 
   574 lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
   575 apply (unfold widens_def)
   576 apply auto
   577 done
   578 
   579 lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)"
   580 apply (unfold widens_def)
   581 apply auto
   582 done
   583 
   584 
   585 section "narrowing relation"
   586 
   587 (* all properties of narrowing and casting conversions we actually need *)
   588 (* these can easily be proven from the definitions below *)
   589 (*
   590 rules
   591   cast_RefT2   "G\<turnstile>S\<preceq>? RefT R   \<Longrightarrow> \<exists>t. S=RefT t" 
   592   cast_PrimT2  "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   593 *)
   594 
   595 (* more detailed than necessary for type-safety, see above rules. *)
   596 inductive --{* narrowing reference conversion, cf. 5.1.5 *}
   597   narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
   598   for G :: prog
   599 where
   600   subcls:  "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile>     Class D\<succ>Class C"
   601 | implmt:  "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile>     Class C\<succ>Iface I"
   602 | obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
   603 | int_cls: "G\<turnstile>     Iface I\<succ>Class C"
   604 | subint:  "imethds G I hidings imethds G J entails 
   605            (\<lambda>(md, mh   ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
   606            \<not>G\<turnstile>I\<preceq>I J         \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
   607 | array:   "G\<turnstile>RefT S\<succ>RefT T   \<spacespace>\<Longrightarrow> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"
   608 
   609 (*unused*)
   610 lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
   611 apply (ind_cases "G\<turnstile>RefT R\<succ>T")
   612 by auto
   613 
   614 lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   615 apply (ind_cases "G\<turnstile>S\<succ>RefT R")
   616 by auto
   617 
   618 (*unused*)
   619 lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
   620 by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   621 
   622 lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>  
   623                                   \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   624 by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   625 
   626 text {* 
   627    These narrowing lemmata hold in Bali but are to strong for ordinary
   628    Java. They  would not work for real Java Integral Types, like short, 
   629    long, int. These lemmata are just for documentation and are not used.
   630  *}
   631 lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt"
   632 by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   633 
   634 lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt"
   635 by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   636 
   637 text {* Specialized versions for booleans also would work for real Java *}
   638 
   639 lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean"
   640 by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
   641 
   642 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
   643 by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
   644 
   645 section "casting relation"
   646 
   647 inductive --{* casting conversion, cf. 5.5 *}
   648   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   649   for G :: prog
   650 where
   651   widen:   "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
   652 | narrow:  "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
   653 
   654 (*unused*)
   655 lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"
   656 apply (ind_cases "G\<turnstile>RefT R\<preceq>? T")
   657 by (auto dest: widen_RefT narrow_RefT)
   658 
   659 lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   660 apply (ind_cases "G\<turnstile>S\<preceq>? RefT R")
   661 by (auto dest: widen_RefT2 narrow_RefT2)
   662 
   663 (*unused*)
   664 lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"
   665 apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T")
   666 by (auto dest: widen_PrimT narrow_PrimT)
   667 
   668 lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   669 apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt")
   670 by (auto dest: widen_PrimT2 narrow_PrimT2)
   671 
   672 lemma cast_Boolean: 
   673   assumes bool_cast: "G\<turnstile>PrimT Boolean\<preceq>? T" 
   674   shows "T=PrimT Boolean"
   675 using bool_cast 
   676 proof (cases)
   677   case widen 
   678   hence "G\<turnstile>PrimT Boolean\<preceq> T"
   679     by simp
   680   thus ?thesis by  (rule widen_Boolean)
   681 next
   682   case narrow
   683   hence "G\<turnstile>PrimT Boolean\<succ>T"
   684     by simp
   685   thus ?thesis by (rule narrow_Boolean)
   686 qed
   687 
   688 lemma cast_Boolean2: 
   689   assumes bool_cast: "G\<turnstile>S\<preceq>? PrimT Boolean" 
   690   shows "S = PrimT Boolean"
   691 using bool_cast 
   692 proof (cases)
   693   case widen 
   694   hence "G\<turnstile>S\<preceq> PrimT Boolean"
   695     by simp
   696   thus ?thesis by  (rule widen_Boolean2)
   697 next
   698   case narrow
   699   hence "G\<turnstile>S\<succ>PrimT Boolean"
   700     by simp
   701   thus ?thesis by (rule narrow_Boolean2)
   702 qed
   703 
   704 end