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