src/HOL/Bali/TypeRel.thy
author wenzelm
Mon Jul 26 17:41:26 2010 +0200 (2010-07-26)
changeset 37956 ee939247b2fb
parent 35416 d8d7d1b785af
child 38541 9cfafdb56749
permissions -rw-r--r--
modernized/unified some specifications;
     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 (*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" --{* direct implementation *}
    36   --{* direct implementation, cf. 8.1.3 *}
    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" ("_|-_<:I1_" [71,71,71] 70)
    42   where "G|-I <:I1 J == (I,J) \<in> subint1 G"
    43 
    44 abbreviation
    45   subint_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
    46   where "G|-I <=:I J == (I,J) \<in>(subint1 G)^*" --{* cf. 9.1.3 *}
    47 
    48 abbreviation
    49   implmt1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
    50   where "G|-C ~>1 I == (C,I) \<in> implmt1 G"
    51 
    52 notation (xsymbols)
    53   subint1_syntax  ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70) and
    54   subint_syntax  ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70) and
    55   implmt1_syntax   ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
    56 
    57 
    58 section "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, standard]
    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 [consumes 1, case_names Eq Subcls]:
   204  "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; C = D \<Longrightarrow> P; G\<turnstile>C \<prec>\<^sub>C D \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   205 by (blast intro: rtrancl_cases)
   206 
   207 lemma subclseq_acyclic: 
   208  "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; G\<turnstile>D \<preceq>\<^sub>C C; ws_prog G\<rbrakk> \<Longrightarrow> C=D"
   209 by (auto elim: subclseq_cases dest: subcls_acyclic)
   210 
   211 lemma subcls_irrefl: "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
   212  \<Longrightarrow> C \<noteq> D"
   213 proof -
   214   assume     ws: "ws_prog G"
   215   assume subcls: "G\<turnstile>C \<prec>\<^sub>C D"
   216   then show ?thesis
   217   proof (induct rule: converse_trancl_induct)
   218     fix C
   219     assume "G\<turnstile>C \<prec>\<^sub>C1 D"
   220     with ws 
   221     show "C\<noteq>D" 
   222       by (blast dest: subcls1_irrefl)
   223   next
   224     fix C Z
   225     assume subcls1_C_Z: "G\<turnstile>C \<prec>\<^sub>C1 Z" and
   226             subcls_Z_D: "G\<turnstile>Z \<prec>\<^sub>C D" and
   227                neq_Z_D: "Z \<noteq> D"
   228     show "C\<noteq>D"
   229     proof
   230       assume eq_C_D: "C=D"
   231       show "False"
   232       proof -
   233         from subcls1_C_Z eq_C_D 
   234         have "G\<turnstile>D \<prec>\<^sub>C Z"
   235           by (auto)
   236         also
   237         from subcls_Z_D ws   
   238         have "\<not> G\<turnstile>D \<prec>\<^sub>C Z"
   239           by (rule subcls_acyclic)
   240         ultimately 
   241         show ?thesis 
   242           by - (rule notE)
   243       qed
   244     qed
   245   qed
   246 qed
   247 
   248 lemma invert_subclseq:
   249 "\<lbrakk>G\<turnstile>C \<preceq>\<^sub>C D; ws_prog G\<rbrakk>
   250  \<Longrightarrow> \<not> G\<turnstile>D \<prec>\<^sub>C C"
   251 proof -
   252   assume       ws: "ws_prog G" and
   253      subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D"
   254   show ?thesis
   255   proof (cases "D=C")
   256     case True
   257     with ws 
   258     show ?thesis 
   259       by (auto dest: subcls_irrefl)
   260   next
   261     case False
   262     with subclseq_C_D 
   263     have "G\<turnstile>C \<prec>\<^sub>C D"
   264       by (blast intro: rtrancl_into_trancl3) 
   265     with ws 
   266     show ?thesis 
   267       by (blast dest: subcls_acyclic)
   268   qed
   269 qed
   270 
   271 lemma invert_subcls:
   272 "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; ws_prog G\<rbrakk>
   273  \<Longrightarrow> \<not> G\<turnstile>D \<preceq>\<^sub>C C"
   274 proof -
   275   assume        ws: "ws_prog G" and
   276         subcls_C_D: "G\<turnstile>C \<prec>\<^sub>C D"
   277   then 
   278   have nsubcls_D_C: "\<not> G\<turnstile>D \<prec>\<^sub>C C"
   279     by (blast dest: subcls_acyclic)
   280   show ?thesis
   281   proof
   282     assume "G\<turnstile>D \<preceq>\<^sub>C C"
   283     then show "False"
   284     proof (cases rule: subclseq_cases)
   285       case Eq
   286       with ws subcls_C_D
   287       show ?thesis 
   288         by (auto dest: subcls_irrefl)
   289     next
   290       case Subcls
   291       with nsubcls_D_C
   292       show ?thesis
   293         by blast
   294     qed
   295   qed
   296 qed
   297 
   298 lemma subcls_superD:
   299  "\<lbrakk>G\<turnstile>C \<prec>\<^sub>C D; class G C = Some c\<rbrakk> \<Longrightarrow> G\<turnstile>(super c) \<preceq>\<^sub>C D"
   300 proof -
   301   assume       clsC: "class G C = Some c"
   302   assume subcls_C_C: "G\<turnstile>C \<prec>\<^sub>C D"
   303   then obtain S where 
   304                   "G\<turnstile>C \<prec>\<^sub>C1 S" and
   305     subclseq_S_D: "G\<turnstile>S \<preceq>\<^sub>C D"
   306     by (blast dest: tranclD)
   307   with clsC 
   308   have "S=super c" 
   309     by (auto dest: subcls1D)
   310   with subclseq_S_D show ?thesis by simp
   311 qed
   312  
   313 
   314 lemma subclseq_superD:
   315  "\<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"
   316 proof -
   317   assume neq_C_D: "C\<noteq>D"
   318   assume    clsC: "class G C = Some c"
   319   assume subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" 
   320   then show ?thesis
   321   proof (cases rule: subclseq_cases)
   322     case Eq with neq_C_D show ?thesis by contradiction
   323   next
   324     case Subcls
   325     with clsC show ?thesis by (blast dest: subcls_superD)
   326   qed
   327 qed
   328 
   329 section "implementation relation"
   330 
   331 lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
   332 apply (unfold implmt1_def)
   333 apply auto
   334 done
   335 
   336 inductive --{* implementation, cf. 8.1.4 *}
   337   implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
   338   for G :: prog
   339 where
   340   direct:         "G\<turnstile>C\<leadsto>1J     \<spacespace>\<spacespace>     \<Longrightarrow> G\<turnstile>C\<leadsto>J"
   341 | subint:        "\<lbrakk>G\<turnstile>C\<leadsto>1I; G\<turnstile>I\<preceq>I J\<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
   342 | subcls1:       "\<lbrakk>G\<turnstile>C\<prec>\<^sub>C1D; G\<turnstile>D\<leadsto>J \<rbrakk>  \<Longrightarrow> G\<turnstile>C\<leadsto>J"
   343 
   344 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)" 
   345 apply (erule implmt.induct)
   346 apply fast+
   347 done
   348 
   349 lemma implmt_ObjectE [elim!]: "G\<turnstile>Object\<leadsto>I \<Longrightarrow> R"
   350 by (auto dest!: implmtD implmt1D subcls1D)
   351 
   352 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"
   353 apply (erule rtrancl_induct)
   354 apply  (auto intro: implmt.subcls1)
   355 done
   356 
   357 lemma implmt_subint2: "\<lbrakk> G\<turnstile>A\<leadsto>J; G\<turnstile>J\<preceq>I K\<rbrakk> \<Longrightarrow> G\<turnstile>A\<leadsto>K"
   358 apply (erule rev_mp, erule implmt.induct)
   359 apply (auto dest: implmt.subint rtrancl_trans implmt.subcls1)
   360 done
   361 
   362 lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C"
   363 apply (erule implmt.induct)
   364 apply (auto dest: implmt1D subcls1D)
   365 done
   366 
   367 
   368 section "widening relation"
   369 
   370 inductive
   371  --{*widening, viz. method invocation conversion, cf. 5.3
   372                             i.e. kind of syntactic subtyping *}
   373   widen :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>_" [71,71,71] 70)
   374   for G :: prog
   375 where
   376   refl:    "G\<turnstile>T\<preceq>T" --{*identity conversion, cf. 5.1.1 *}
   377 | subint:  "G\<turnstile>I\<preceq>I J  \<Longrightarrow> G\<turnstile>Iface I\<preceq> Iface J" --{*wid.ref.conv.,cf. 5.1.4 *}
   378 | int_obj: "G\<turnstile>Iface I\<preceq> Class Object"
   379 | subcls:  "G\<turnstile>C\<preceq>\<^sub>C D  \<Longrightarrow> G\<turnstile>Class C\<preceq> Class D"
   380 | implmt:  "G\<turnstile>C\<leadsto>I   \<Longrightarrow> G\<turnstile>Class C\<preceq> Iface I"
   381 | null:    "G\<turnstile>NT\<preceq> RefT R"
   382 | arr_obj: "G\<turnstile>T.[]\<preceq> Class Object"
   383 | array:   "G\<turnstile>RefT S\<preceq>RefT T \<Longrightarrow> G\<turnstile>RefT S.[]\<preceq> RefT T.[]"
   384 
   385 declare widen.refl [intro!]
   386 declare widen.intros [simp]
   387 
   388 (* too strong in general:
   389 lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
   390 *)
   391 lemma widen_PrimT: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> (\<exists>y. T = PrimT y)"
   392 apply (ind_cases "G\<turnstile>PrimT x\<preceq>T")
   393 by auto
   394 
   395 (* too strong in general:
   396 lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
   397 *)
   398 lemma widen_PrimT2: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> \<exists>y. S = PrimT y"
   399 apply (ind_cases "G\<turnstile>S\<preceq>PrimT x")
   400 by auto
   401 
   402 text {* 
   403    These widening lemmata hold in Bali but are to strong for ordinary
   404    Java. They  would not work for real Java Integral Types, like short, 
   405    long, int. These lemmata are just for documentation and are not used.
   406  *}
   407 
   408 lemma widen_PrimT_strong: "G\<turnstile>PrimT x\<preceq>T \<Longrightarrow> T = PrimT x"
   409 by (ind_cases "G\<turnstile>PrimT x\<preceq>T") simp_all
   410 
   411 lemma widen_PrimT2_strong: "G\<turnstile>S\<preceq>PrimT x \<Longrightarrow> S = PrimT x"
   412 by (ind_cases "G\<turnstile>S\<preceq>PrimT x") simp_all
   413 
   414 text {* Specialized versions for booleans also would work for real Java *}
   415 
   416 lemma widen_Boolean: "G\<turnstile>PrimT Boolean\<preceq>T \<Longrightarrow> T = PrimT Boolean"
   417 by (ind_cases "G\<turnstile>PrimT Boolean\<preceq>T") simp_all
   418 
   419 lemma widen_Boolean2: "G\<turnstile>S\<preceq>PrimT Boolean \<Longrightarrow> S = PrimT Boolean"
   420 by (ind_cases "G\<turnstile>S\<preceq>PrimT Boolean") simp_all
   421 
   422 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T \<Longrightarrow> \<exists>t. T=RefT t"
   423 apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
   424 by auto
   425 
   426 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   427 apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
   428 by auto
   429 
   430 lemma widen_Iface: "G\<turnstile>Iface I\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>J. T=Iface J)"
   431 apply (ind_cases "G\<turnstile>Iface I\<preceq>T")
   432 by auto
   433 
   434 lemma widen_Iface2: "G\<turnstile>S\<preceq> Iface J \<Longrightarrow> S = NT \<or> (\<exists>I. S = Iface I) \<or> (\<exists>D. S = Class D)"
   435 apply (ind_cases "G\<turnstile>S\<preceq> Iface J")
   436 by auto
   437 
   438 lemma widen_Iface_Iface: "G\<turnstile>Iface I\<preceq> Iface J \<Longrightarrow> G\<turnstile>I\<preceq>I J"
   439 apply (ind_cases "G\<turnstile>Iface I\<preceq> Iface J")
   440 by auto
   441 
   442 lemma widen_Iface_Iface_eq [simp]: "G\<turnstile>Iface I\<preceq> Iface J = G\<turnstile>I\<preceq>I J"
   443 apply (rule iffI)
   444 apply  (erule widen_Iface_Iface)
   445 apply (erule widen.subint)
   446 done
   447 
   448 lemma widen_Class: "G\<turnstile>Class C\<preceq>T \<Longrightarrow>  (\<exists>D. T=Class D) \<or> (\<exists>I. T=Iface I)"
   449 apply (ind_cases "G\<turnstile>Class C\<preceq>T")
   450 by auto
   451 
   452 lemma widen_Class2: "G\<turnstile>S\<preceq> Class C \<Longrightarrow> C = Object \<or> S = NT \<or> (\<exists>D. S = Class D)"
   453 apply (ind_cases "G\<turnstile>S\<preceq> Class C")
   454 by auto
   455 
   456 lemma widen_Class_Class: "G\<turnstile>Class C\<preceq> Class cm \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C cm"
   457 apply (ind_cases "G\<turnstile>Class C\<preceq> Class cm")
   458 by auto
   459 
   460 lemma widen_Class_Class_eq [simp]: "G\<turnstile>Class C\<preceq> Class cm = G\<turnstile>C\<preceq>\<^sub>C cm"
   461 apply (rule iffI)
   462 apply  (erule widen_Class_Class)
   463 apply (erule widen.subcls)
   464 done
   465 
   466 lemma widen_Class_Iface: "G\<turnstile>Class C\<preceq> Iface I \<Longrightarrow> G\<turnstile>C\<leadsto>I"
   467 apply (ind_cases "G\<turnstile>Class C\<preceq> Iface I")
   468 by auto
   469 
   470 lemma widen_Class_Iface_eq [simp]: "G\<turnstile>Class C\<preceq> Iface I = G\<turnstile>C\<leadsto>I"
   471 apply (rule iffI)
   472 apply  (erule widen_Class_Iface)
   473 apply (erule widen.implmt)
   474 done
   475 
   476 lemma widen_Array: "G\<turnstile>S.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>T'. T=T'.[] \<and> G\<turnstile>S\<preceq>T')"
   477 apply (ind_cases "G\<turnstile>S.[]\<preceq>T")
   478 by auto
   479 
   480 lemma widen_Array2: "G\<turnstile>S\<preceq>T.[] \<Longrightarrow> S = NT \<or> (\<exists>S'. S=S'.[] \<and> G\<turnstile>S'\<preceq>T)"
   481 apply (ind_cases "G\<turnstile>S\<preceq>T.[]")
   482 by auto
   483 
   484 
   485 lemma widen_ArrayPrimT: "G\<turnstile>PrimT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> T=PrimT t.[]"
   486 apply (ind_cases "G\<turnstile>PrimT t.[]\<preceq>T")
   487 by auto
   488 
   489 lemma widen_ArrayRefT: 
   490   "G\<turnstile>RefT t.[]\<preceq>T \<Longrightarrow> T=Class Object \<or> (\<exists>s. T=RefT s.[] \<and> G\<turnstile>RefT t\<preceq>RefT s)"
   491 apply (ind_cases "G\<turnstile>RefT t.[]\<preceq>T")
   492 by auto
   493 
   494 lemma widen_ArrayRefT_ArrayRefT_eq [simp]: 
   495   "G\<turnstile>RefT T.[]\<preceq>RefT T'.[] = G\<turnstile>RefT T\<preceq>RefT T'"
   496 apply (rule iffI)
   497 apply (drule widen_ArrayRefT)
   498 apply simp
   499 apply (erule widen.array)
   500 done
   501 
   502 lemma widen_Array_Array: "G\<turnstile>T.[]\<preceq>T'.[] \<Longrightarrow> G\<turnstile>T\<preceq>T'"
   503 apply (drule widen_Array)
   504 apply auto
   505 done
   506 
   507 lemma widen_Array_Class: "G\<turnstile>S.[] \<preceq> Class C \<Longrightarrow> C=Object"
   508 by (auto dest: widen_Array)
   509 
   510 
   511 lemma widen_NT2: "G\<turnstile>S\<preceq>NT \<Longrightarrow> S = NT"
   512 apply (ind_cases "G\<turnstile>S\<preceq>NT")
   513 by auto
   514 
   515 lemma widen_Object:"\<lbrakk>isrtype G T;ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>RefT T \<preceq> Class Object"
   516 apply (case_tac T)
   517 apply (auto)
   518 apply (subgoal_tac "G\<turnstile>qtname_ext_type\<preceq>\<^sub>C Object")
   519 apply (auto intro: subcls_ObjectI)
   520 done
   521 
   522 lemma widen_trans_lemma [rule_format (no_asm)]: 
   523   "\<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"
   524 apply (erule widen.induct)
   525 apply        safe
   526 prefer      5 apply (drule widen_RefT) apply clarsimp
   527 apply      (frule_tac [1] widen_Iface)
   528 apply      (frule_tac [2] widen_Class)
   529 apply      (frule_tac [3] widen_Class)
   530 apply      (frule_tac [4] widen_Iface)
   531 apply      (frule_tac [5] widen_Class)
   532 apply      (frule_tac [6] widen_Array)
   533 apply      safe
   534 apply            (rule widen.int_obj)
   535 prefer          6 apply (drule implmt_is_class) apply simp
   536 apply (tactic "ALLGOALS (etac thin_rl)")
   537 prefer         6 apply simp
   538 apply          (rule_tac [9] widen.arr_obj)
   539 apply         (rotate_tac [9] -1)
   540 apply         (frule_tac [9] widen_RefT)
   541 apply         (auto elim!: rtrancl_trans subcls_implmt implmt_subint2)
   542 done
   543 
   544 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"
   545 by (auto intro: widen_trans_lemma subcls_ObjectI)
   546 
   547 lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T;  
   548  \<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J;  
   549  \<forall>C D. G\<turnstile>C\<preceq>\<^sub>C D \<and> G\<turnstile>D\<preceq>\<^sub>C C \<longrightarrow> C = D;  
   550  \<forall>I  . G\<turnstile>Object\<leadsto>I        \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T"
   551 apply (erule widen.induct)
   552 apply (auto dest: widen_Iface widen_NT2 widen_Class)
   553 done
   554 
   555 lemmas subint_antisym = 
   556        subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
   557 lemmas subcls_antisym = 
   558        subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
   559 
   560 lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
   561 by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 
   562                                    subcls_antisym [THEN antisymD])
   563 
   564 lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object"
   565 apply (frule widen_Class)
   566 apply (fast dest: widen_Class_Class widen_Class_Iface)
   567 done
   568 
   569 definition
   570   widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
   571   where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
   572 
   573 lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
   574 apply (unfold widens_def)
   575 apply auto
   576 done
   577 
   578 lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)"
   579 apply (unfold widens_def)
   580 apply auto
   581 done
   582 
   583 
   584 section "narrowing relation"
   585 
   586 (* all properties of narrowing and casting conversions we actually need *)
   587 (* these can easily be proven from the definitions below *)
   588 (*
   589 rules
   590   cast_RefT2   "G\<turnstile>S\<preceq>? RefT R   \<Longrightarrow> \<exists>t. S=RefT t" 
   591   cast_PrimT2  "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   592 *)
   593 
   594 (* more detailed than necessary for type-safety, see above rules. *)
   595 inductive --{* narrowing reference conversion, cf. 5.1.5 *}
   596   narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
   597   for G :: prog
   598 where
   599   subcls:  "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile>     Class D\<succ>Class C"
   600 | implmt:  "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile>     Class C\<succ>Iface I"
   601 | obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
   602 | int_cls: "G\<turnstile>     Iface I\<succ>Class C"
   603 | subint:  "imethds G I hidings imethds G J entails 
   604            (\<lambda>(md, mh   ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
   605            \<not>G\<turnstile>I\<preceq>I J         \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
   606 | array:   "G\<turnstile>RefT S\<succ>RefT T   \<spacespace>\<Longrightarrow> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"
   607 
   608 (*unused*)
   609 lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
   610 apply (ind_cases "G\<turnstile>RefT R\<succ>T")
   611 by auto
   612 
   613 lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   614 apply (ind_cases "G\<turnstile>S\<succ>RefT R")
   615 by auto
   616 
   617 (*unused*)
   618 lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
   619 by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   620 
   621 lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>  
   622                                   \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   623 by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   624 
   625 text {* 
   626    These narrowing lemmata hold in Bali but are to strong for ordinary
   627    Java. They  would not work for real Java Integral Types, like short, 
   628    long, int. These lemmata are just for documentation and are not used.
   629  *}
   630 lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt"
   631 by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   632 
   633 lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt"
   634 by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   635 
   636 text {* Specialized versions for booleans also would work for real Java *}
   637 
   638 lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean"
   639 by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
   640 
   641 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
   642 by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
   643 
   644 section "casting relation"
   645 
   646 inductive --{* casting conversion, cf. 5.5 *}
   647   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   648   for G :: prog
   649 where
   650   widen:   "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
   651 | narrow:  "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
   652 
   653 (*unused*)
   654 lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"
   655 apply (ind_cases "G\<turnstile>RefT R\<preceq>? T")
   656 by (auto dest: widen_RefT narrow_RefT)
   657 
   658 lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   659 apply (ind_cases "G\<turnstile>S\<preceq>? RefT R")
   660 by (auto dest: widen_RefT2 narrow_RefT2)
   661 
   662 (*unused*)
   663 lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"
   664 apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T")
   665 by (auto dest: widen_PrimT narrow_PrimT)
   666 
   667 lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   668 apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt")
   669 by (auto dest: widen_PrimT2 narrow_PrimT2)
   670 
   671 lemma cast_Boolean: 
   672   assumes bool_cast: "G\<turnstile>PrimT Boolean\<preceq>? T" 
   673   shows "T=PrimT Boolean"
   674 using bool_cast 
   675 proof (cases)
   676   case widen 
   677   hence "G\<turnstile>PrimT Boolean\<preceq> T"
   678     by simp
   679   thus ?thesis by  (rule widen_Boolean)
   680 next
   681   case narrow
   682   hence "G\<turnstile>PrimT Boolean\<succ>T"
   683     by simp
   684   thus ?thesis by (rule narrow_Boolean)
   685 qed
   686 
   687 lemma cast_Boolean2: 
   688   assumes bool_cast: "G\<turnstile>S\<preceq>? PrimT Boolean" 
   689   shows "S = PrimT Boolean"
   690 using bool_cast 
   691 proof (cases)
   692   case widen 
   693   hence "G\<turnstile>S\<preceq> PrimT Boolean"
   694     by simp
   695   thus ?thesis by  (rule widen_Boolean2)
   696 next
   697   case narrow
   698   hence "G\<turnstile>S\<succ>PrimT Boolean"
   699     by simp
   700   thus ?thesis by (rule narrow_Boolean2)
   701 qed
   702 
   703 end