src/HOL/Bali/TypeRel.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45605 a89b4bc311a5
child 46212 d86ef6b96097
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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]
    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:
   516   assumes "isrtype G T" and "ws_prog G"
   517   shows "G\<turnstile>RefT T \<preceq> Class Object"
   518 proof (cases T)
   519   case (ClassT C) with assms have "G\<turnstile>C\<preceq>\<^sub>C Object" by (auto intro: subcls_ObjectI)
   520   with ClassT show ?thesis by auto
   521 qed simp_all
   522 
   523 lemma widen_trans_lemma [rule_format (no_asm)]: 
   524   "\<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"
   525 apply (erule widen.induct)
   526 apply        safe
   527 prefer      5 apply (drule widen_RefT) apply clarsimp
   528 apply      (frule_tac [1] widen_Iface)
   529 apply      (frule_tac [2] widen_Class)
   530 apply      (frule_tac [3] widen_Class)
   531 apply      (frule_tac [4] widen_Iface)
   532 apply      (frule_tac [5] widen_Class)
   533 apply      (frule_tac [6] widen_Array)
   534 apply      safe
   535 apply            (rule widen.int_obj)
   536 prefer          6 apply (drule implmt_is_class) apply simp
   537 apply (tactic "ALLGOALS (etac thin_rl)")
   538 prefer         6 apply simp
   539 apply          (rule_tac [9] widen.arr_obj)
   540 apply         (rotate_tac [9] -1)
   541 apply         (frule_tac [9] widen_RefT)
   542 apply         (auto elim!: rtrancl_trans subcls_implmt implmt_subint2)
   543 done
   544 
   545 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"
   546 by (auto intro: widen_trans_lemma subcls_ObjectI)
   547 
   548 lemma widen_antisym_lemma [rule_format (no_asm)]: "\<lbrakk>G\<turnstile>S\<preceq>T;  
   549  \<forall>I J. G\<turnstile>I\<preceq>I J \<and> G\<turnstile>J\<preceq>I I \<longrightarrow> I = J;  
   550  \<forall>C D. G\<turnstile>C\<preceq>\<^sub>C D \<and> G\<turnstile>D\<preceq>\<^sub>C C \<longrightarrow> C = D;  
   551  \<forall>I  . G\<turnstile>Object\<leadsto>I        \<longrightarrow> False\<rbrakk> \<Longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T"
   552 apply (erule widen.induct)
   553 apply (auto dest: widen_Iface widen_NT2 widen_Class)
   554 done
   555 
   556 lemmas subint_antisym = 
   557        subint1_acyclic [THEN acyclic_impl_antisym_rtrancl]
   558 lemmas subcls_antisym = 
   559        subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl]
   560 
   561 lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
   562 by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD] 
   563                                    subcls_antisym [THEN antisymD])
   564 
   565 lemma widen_ObjectD [dest!]: "G\<turnstile>Class Object\<preceq>T \<Longrightarrow> T=Class Object"
   566 apply (frule widen_Class)
   567 apply (fast dest: widen_Class_Class widen_Class_Iface)
   568 done
   569 
   570 definition
   571   widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
   572   where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
   573 
   574 lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
   575 apply (unfold widens_def)
   576 apply auto
   577 done
   578 
   579 lemma widens_Cons [simp]: "G\<turnstile>(S#Ss)[\<preceq>](T#Ts) = (G\<turnstile>S\<preceq>T \<and> G\<turnstile>Ss[\<preceq>]Ts)"
   580 apply (unfold widens_def)
   581 apply auto
   582 done
   583 
   584 
   585 section "narrowing relation"
   586 
   587 (* all properties of narrowing and casting conversions we actually need *)
   588 (* these can easily be proven from the definitions below *)
   589 (*
   590 rules
   591   cast_RefT2   "G\<turnstile>S\<preceq>? RefT R   \<Longrightarrow> \<exists>t. S=RefT t" 
   592   cast_PrimT2  "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   593 *)
   594 
   595 (* more detailed than necessary for type-safety, see above rules. *)
   596 inductive --{* narrowing reference conversion, cf. 5.1.5 *}
   597   narrow :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<succ>_" [71,71,71] 70)
   598   for G :: prog
   599 where
   600   subcls:  "G\<turnstile>C\<preceq>\<^sub>C D \<Longrightarrow> G\<turnstile>     Class D\<succ>Class C"
   601 | implmt:  "\<not>G\<turnstile>C\<leadsto>I \<Longrightarrow> G\<turnstile>     Class C\<succ>Iface I"
   602 | obj_arr: "G\<turnstile>Class Object\<succ>T.[]"
   603 | int_cls: "G\<turnstile>     Iface I\<succ>Class C"
   604 | subint:  "imethds G I hidings imethds G J entails 
   605            (\<lambda>(md, mh   ) (md',mh').\<spacespace>G\<turnstile>mrt mh\<preceq>mrt mh') \<Longrightarrow>
   606            \<not>G\<turnstile>I\<preceq>I J         \<spacespace>\<spacespace>\<spacespace>\<Longrightarrow> G\<turnstile>     Iface I\<succ>Iface J"
   607 | array:   "G\<turnstile>RefT S\<succ>RefT T   \<spacespace>\<Longrightarrow> G\<turnstile>   RefT S.[]\<succ>RefT T.[]"
   608 
   609 (*unused*)
   610 lemma narrow_RefT: "G\<turnstile>RefT R\<succ>T \<Longrightarrow> \<exists>t. T=RefT t"
   611 apply (ind_cases "G\<turnstile>RefT R\<succ>T")
   612 by auto
   613 
   614 lemma narrow_RefT2: "G\<turnstile>S\<succ>RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   615 apply (ind_cases "G\<turnstile>S\<succ>RefT R")
   616 by auto
   617 
   618 (*unused*)
   619 lemma narrow_PrimT: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> \<exists>t. T=PrimT t"
   620 by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   621 
   622 lemma narrow_PrimT2: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow>  
   623                                   \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   624 by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   625 
   626 text {* 
   627    These narrowing lemmata hold in Bali but are to strong for ordinary
   628    Java. They  would not work for real Java Integral Types, like short, 
   629    long, int. These lemmata are just for documentation and are not used.
   630  *}
   631 lemma narrow_PrimT_strong: "G\<turnstile>PrimT pt\<succ>T \<Longrightarrow> T=PrimT pt"
   632 by (ind_cases "G\<turnstile>PrimT pt\<succ>T")
   633 
   634 lemma narrow_PrimT2_strong: "G\<turnstile>S\<succ>PrimT pt \<Longrightarrow> S=PrimT pt"
   635 by (ind_cases "G\<turnstile>S\<succ>PrimT pt")
   636 
   637 text {* Specialized versions for booleans also would work for real Java *}
   638 
   639 lemma narrow_Boolean: "G\<turnstile>PrimT Boolean\<succ>T \<Longrightarrow> T=PrimT Boolean"
   640 by (ind_cases "G\<turnstile>PrimT Boolean\<succ>T")
   641 
   642 lemma narrow_Boolean2: "G\<turnstile>S\<succ>PrimT Boolean \<Longrightarrow> S=PrimT Boolean"
   643 by (ind_cases "G\<turnstile>S\<succ>PrimT Boolean")
   644 
   645 section "casting relation"
   646 
   647 inductive --{* casting conversion, cf. 5.5 *}
   648   cast :: "prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" ("_\<turnstile>_\<preceq>? _" [71,71,71] 70)
   649   for G :: prog
   650 where
   651   widen:   "G\<turnstile>S\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
   652 | narrow:  "G\<turnstile>S\<succ>T \<Longrightarrow> G\<turnstile>S\<preceq>? T"
   653 
   654 (*unused*)
   655 lemma cast_RefT: "G\<turnstile>RefT R\<preceq>? T \<Longrightarrow> \<exists>t. T=RefT t"
   656 apply (ind_cases "G\<turnstile>RefT R\<preceq>? T")
   657 by (auto dest: widen_RefT narrow_RefT)
   658 
   659 lemma cast_RefT2: "G\<turnstile>S\<preceq>? RefT R \<Longrightarrow> \<exists>t. S=RefT t"
   660 apply (ind_cases "G\<turnstile>S\<preceq>? RefT R")
   661 by (auto dest: widen_RefT2 narrow_RefT2)
   662 
   663 (*unused*)
   664 lemma cast_PrimT: "G\<turnstile>PrimT pt\<preceq>? T \<Longrightarrow> \<exists>t. T=PrimT t"
   665 apply (ind_cases "G\<turnstile>PrimT pt\<preceq>? T")
   666 by (auto dest: widen_PrimT narrow_PrimT)
   667 
   668 lemma cast_PrimT2: "G\<turnstile>S\<preceq>? PrimT pt \<Longrightarrow> \<exists>t. S=PrimT t \<and> G\<turnstile>PrimT t\<preceq>PrimT pt"
   669 apply (ind_cases "G\<turnstile>S\<preceq>? PrimT pt")
   670 by (auto dest: widen_PrimT2 narrow_PrimT2)
   671 
   672 lemma cast_Boolean: 
   673   assumes bool_cast: "G\<turnstile>PrimT Boolean\<preceq>? T" 
   674   shows "T=PrimT Boolean"
   675 using bool_cast 
   676 proof (cases)
   677   case widen 
   678   hence "G\<turnstile>PrimT Boolean\<preceq> T"
   679     by simp
   680   thus ?thesis by  (rule widen_Boolean)
   681 next
   682   case narrow
   683   hence "G\<turnstile>PrimT Boolean\<succ>T"
   684     by simp
   685   thus ?thesis by (rule narrow_Boolean)
   686 qed
   687 
   688 lemma cast_Boolean2: 
   689   assumes bool_cast: "G\<turnstile>S\<preceq>? PrimT Boolean" 
   690   shows "S = PrimT Boolean"
   691 using bool_cast 
   692 proof (cases)
   693   case widen 
   694   hence "G\<turnstile>S\<preceq> PrimT Boolean"
   695     by simp
   696   thus ?thesis by  (rule widen_Boolean2)
   697 next
   698   case narrow
   699   hence "G\<turnstile>S\<succ>PrimT Boolean"
   700     by simp
   701   thus ?thesis by (rule narrow_Boolean2)
   702 qed
   703 
   704 end