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