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