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