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