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