src/HOL/MicroJava/BV/JType.thy
author kleing
Mon Nov 20 16:41:25 2000 +0100 (2000-11-20)
changeset 10497 7c6985b4de40
child 10592 fc0b575a2cf7
permissions -rw-r--r--
BCV integration (type system is semilattice)
kleing@10497
     1
(*  Title:      HOL/BCV/JType.thy
kleing@10497
     2
    ID:         $Id$
kleing@10497
     3
    Author:     Tobias Nipkow
kleing@10497
     4
    Copyright   2000 TUM
kleing@10497
     5
kleing@10497
     6
The type system of the JVM
kleing@10497
     7
*)
kleing@10497
     8
kleing@10497
     9
header "JVM Type System as Semilattice"
kleing@10497
    10
kleing@10497
    11
theory JType = WellForm + Err:
kleing@10497
    12
kleing@10497
    13
constdefs
kleing@10497
    14
  is_ref :: "ty => bool"
kleing@10497
    15
  "is_ref T == case T of PrimT t => False | RefT r => True"
kleing@10497
    16
kleing@10497
    17
  sup :: "'c prog => ty => ty => ty err"
kleing@10497
    18
  "sup G T1 T2 ==
kleing@10497
    19
  case T1 of PrimT P1 => (case T2 of PrimT P2 => (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
kleing@10497
    20
           | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => 
kleing@10497
    21
  (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
kleing@10497
    22
            | ClassT C => (case R2 of NullT => OK (Class C) 
kleing@10497
    23
                                    | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
kleing@10497
    24
kleing@10497
    25
  subtype :: "'c prog => ty => ty => bool"
kleing@10497
    26
  "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
kleing@10497
    27
kleing@10497
    28
  is_ty :: "'c prog => ty => bool"
kleing@10497
    29
  "is_ty G T == case T of PrimT P => True | RefT R =>
kleing@10497
    30
               (case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)"
kleing@10497
    31
kleing@10497
    32
translations
kleing@10497
    33
  "types G" == "Collect (is_type G)"
kleing@10497
    34
kleing@10497
    35
constdefs
kleing@10497
    36
  esl :: "'c prog => ty esl"
kleing@10497
    37
  "esl G == (types G, subtype G, sup G)"
kleing@10497
    38
kleing@10497
    39
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
kleing@10497
    40
  by (auto elim: widen.elims)
kleing@10497
    41
kleing@10497
    42
lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
kleing@10497
    43
  by (auto elim: widen.elims)
kleing@10497
    44
kleing@10497
    45
lemma is_tyI:
kleing@10497
    46
  "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
kleing@10497
    47
  by (auto simp add: is_ty_def dest: subcls_C_Object 
kleing@10497
    48
           split: ty.splits ref_ty.splits)
kleing@10497
    49
kleing@10497
    50
lemma is_type_conv: 
kleing@10497
    51
  "wf_prog wf_mb G ==> is_type G T = is_ty G T"
kleing@10497
    52
proof
kleing@10497
    53
  assume "is_type G T" "wf_prog wf_mb G" 
kleing@10497
    54
  thus "is_ty G T"
kleing@10497
    55
    by (rule is_tyI)
kleing@10497
    56
next
kleing@10497
    57
  assume wf: "wf_prog wf_mb G" and
kleing@10497
    58
         ty: "is_ty G T"
kleing@10497
    59
kleing@10497
    60
  show "is_type G T"
kleing@10497
    61
  proof (cases T)
kleing@10497
    62
    case PrimT
kleing@10497
    63
    thus ?thesis by simp
kleing@10497
    64
  next
kleing@10497
    65
    fix R assume R: "T = RefT R"
kleing@10497
    66
    with wf
kleing@10497
    67
    have "R = ClassT Object \<Longrightarrow> ?thesis" by simp
kleing@10497
    68
    moreover    
kleing@10497
    69
    from R wf ty
kleing@10497
    70
    have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
kleing@10497
    71
      by (auto simp add: is_ty_def subcls1_def is_class_def class_def 
kleing@10497
    72
               elim: converse_rtranclE
kleing@10497
    73
               split: ref_ty.splits)    
kleing@10497
    74
    ultimately    
kleing@10497
    75
    show ?thesis by blast
kleing@10497
    76
  qed
kleing@10497
    77
qed
kleing@10497
    78
kleing@10497
    79
kleing@10497
    80
lemma order_widen:
kleing@10497
    81
  "acyclic (subcls1 G) ==> order (subtype G)"
kleing@10497
    82
  apply (unfold order_def lesub_def subtype_def)
kleing@10497
    83
  apply (auto intro: widen_trans)
kleing@10497
    84
  apply (case_tac x)
kleing@10497
    85
   apply (case_tac y)
kleing@10497
    86
    apply (auto simp add: PrimT_PrimT)
kleing@10497
    87
   apply (case_tac y)
kleing@10497
    88
    apply simp
kleing@10497
    89
  apply simp
kleing@10497
    90
  apply (case_tac ref_ty)
kleing@10497
    91
   apply (case_tac ref_tya)
kleing@10497
    92
    apply simp
kleing@10497
    93
   apply simp
kleing@10497
    94
  apply (case_tac ref_tya)
kleing@10497
    95
   apply simp
kleing@10497
    96
  apply simp
kleing@10497
    97
  apply (auto dest: acyclic_impl_antisym_rtrancl antisymD)  
kleing@10497
    98
  done
kleing@10497
    99
kleing@10497
   100
lemma closed_err_types:
kleing@10497
   101
  "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] 
kleing@10497
   102
  ==> closed (err (types G)) (lift2 (sup G))"
kleing@10497
   103
  apply (unfold closed_def plussub_def lift2_def sup_def)
kleing@10497
   104
  apply (auto split: err.split)
kleing@10497
   105
  apply (drule is_tyI, assumption)
kleing@10497
   106
  apply (auto simp add: is_ty_def is_type_conv simp del: is_type.simps 
kleing@10497
   107
              split: ty.split ref_ty.split)
kleing@10497
   108
  apply (blast dest!: is_lub_some_lub is_lubD is_ubD intro!: is_ubI)
kleing@10497
   109
  done
kleing@10497
   110
kleing@10497
   111
kleing@10497
   112
lemma err_semilat_JType_esl_lemma:
kleing@10497
   113
  "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] 
kleing@10497
   114
  ==> err_semilat (esl G)"
kleing@10497
   115
proof -
kleing@10497
   116
  assume wf_prog:   "wf_prog wf_mb G"
kleing@10497
   117
  assume univalent: "univalent (subcls1 G)" 
kleing@10497
   118
  assume acyclic:   "acyclic (subcls1 G)"
kleing@10497
   119
  
kleing@10497
   120
  hence "order (subtype G)"
kleing@10497
   121
    by (rule order_widen)
kleing@10497
   122
  moreover
kleing@10497
   123
  from wf_prog univalent acyclic
kleing@10497
   124
  have "closed (err (types G)) (lift2 (sup G))"
kleing@10497
   125
    by (rule closed_err_types)
kleing@10497
   126
  moreover
kleing@10497
   127
  
kleing@10497
   128
  { fix c1 c2
kleing@10497
   129
    assume is_class: "is_class G c1" "is_class G c2"
kleing@10497
   130
    with wf_prog 
kleing@10497
   131
    obtain 
kleing@10497
   132
      "G \<turnstile> c1 \<preceq>C Object"
kleing@10497
   133
      "G \<turnstile> c2 \<preceq>C Object"
kleing@10497
   134
      by (blast intro: subcls_C_Object)
kleing@10497
   135
    with wf_prog univalent
kleing@10497
   136
    obtain u where
kleing@10497
   137
      "is_lub ((subcls1 G)^* ) c1 c2 u"
kleing@10497
   138
      by (blast dest: univalent_has_lubs)
kleing@10497
   139
    with acyclic
kleing@10497
   140
    have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
kleing@10497
   141
      by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
kleing@10497
   142
  } note this [intro]
kleing@10497
   143
      
kleing@10497
   144
  { fix t1 t2 s
kleing@10497
   145
    assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s"    
kleing@10497
   146
    hence "subtype G t1 s"
kleing@10497
   147
      by (unfold sup_def subtype_def) 
kleing@10497
   148
         (cases s, auto intro: widen.null 
kleing@10497
   149
                        split: ty.splits ref_ty.splits if_splits)
kleing@10497
   150
  } note this [intro]
kleing@10497
   151
kleing@10497
   152
  have
kleing@10497
   153
    "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y"
kleing@10497
   154
    by (auto simp add: lesub_def plussub_def le_def lift2_def split: err.split)
kleing@10497
   155
  moreover
kleing@10497
   156
kleing@10497
   157
  { fix c1 c2
kleing@10497
   158
    assume "is_class G c1" "is_class G c2"
kleing@10497
   159
    with wf_prog
kleing@10497
   160
    obtain 
kleing@10497
   161
      "G \<turnstile> c1 \<preceq>C Object"
kleing@10497
   162
      "G \<turnstile> c2 \<preceq>C Object"
kleing@10497
   163
      by (blast intro: subcls_C_Object)
kleing@10497
   164
    with wf_prog univalent
kleing@10497
   165
    obtain u where
kleing@10497
   166
      "is_lub ((subcls1 G)^* ) c2 c1 u"
kleing@10497
   167
      by (blast dest: univalent_has_lubs)
kleing@10497
   168
    with acyclic
kleing@10497
   169
    have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c2 c1"
kleing@10497
   170
      by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
kleing@10497
   171
  } note this [intro]
kleing@10497
   172
      
kleing@10497
   173
  have "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). 
kleing@10497
   174
    y <=_(le (subtype G)) x +_(lift2 (sup G)) y"
kleing@10497
   175
    by (auto simp add: lesub_def plussub_def le_def sup_def subtype_def lift2_def 
kleing@10497
   176
             split: err.split ty.splits ref_ty.splits if_splits intro: widen.null)
kleing@10497
   177
  moreover
kleing@10497
   178
    
kleing@10497
   179
  have [intro]: 
kleing@10497
   180
    "!!a b c. [| G \<turnstile> a \<preceq> c; G \<turnstile> b \<preceq> c; sup G a b = Err |] ==> False"
kleing@10497
   181
    by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def 
kleing@10497
   182
             split: ty.splits ref_ty.splits)
kleing@10497
   183
kleing@10497
   184
  { fix c1 c2 D
kleing@10497
   185
    assume is_class: "is_class G c1" "is_class G c2"
kleing@10497
   186
    assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
kleing@10497
   187
    from wf_prog is_class
kleing@10497
   188
    obtain 
kleing@10497
   189
      "G \<turnstile> c1 \<preceq>C Object"
kleing@10497
   190
      "G \<turnstile> c2 \<preceq>C Object"
kleing@10497
   191
      by (blast intro: subcls_C_Object)
kleing@10497
   192
    with wf_prog univalent
kleing@10497
   193
    obtain u where
kleing@10497
   194
      lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
kleing@10497
   195
      by (blast dest: univalent_has_lubs)   
kleing@10497
   196
    with acyclic
kleing@10497
   197
    have "some_lub ((subcls1 G)^* ) c1 c2 = u"
kleing@10497
   198
      by (rule some_lub_conv)
kleing@10497
   199
    moreover
kleing@10497
   200
    from lub le
kleing@10497
   201
    have "G \<turnstile> u \<preceq>C D" 
kleing@10497
   202
      by (simp add: is_lub_def is_ub_def)
kleing@10497
   203
    ultimately     
kleing@10497
   204
    have "G \<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \<preceq>C D"
kleing@10497
   205
      by blast
kleing@10497
   206
  } note this [intro]
kleing@10497
   207
kleing@10497
   208
  have [dest!]:
kleing@10497
   209
    "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
kleing@10497
   210
    by (frule widen_Class, auto)
kleing@10497
   211
kleing@10497
   212
  { fix a b c d
kleing@10497
   213
    assume "is_type G a" "is_type G b" "is_type G c" and
kleing@10497
   214
           "G \<turnstile> a \<preceq> c" "G \<turnstile> b \<preceq> c" and
kleing@10497
   215
           "sup G a b = OK d" 
kleing@10497
   216
    hence "G \<turnstile> d \<preceq> c"
kleing@10497
   217
      by (auto simp add: sup_def split: ty.splits ref_ty.splits if_splits)
kleing@10497
   218
  } note this [intro]
kleing@10497
   219
kleing@10497
   220
  have
kleing@10497
   221
    "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G). 
kleing@10497
   222
    x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
kleing@10497
   223
    by (simp add: lift2_def plussub_def lesub_def subtype_def le_def split: err.splits) blast
kleing@10497
   224
kleing@10497
   225
  ultimately
kleing@10497
   226
  
kleing@10497
   227
  show ?thesis
kleing@10497
   228
    by (unfold esl_def semilat_def sl_def) auto
kleing@10497
   229
qed
kleing@10497
   230
kleing@10497
   231
lemma univalent_subcls1:
kleing@10497
   232
  "wf_prog wf_mb G ==> univalent (subcls1 G)"
kleing@10497
   233
  by (unfold wf_prog_def unique_def univalent_def subcls1_def) auto
kleing@10497
   234
kleing@10497
   235
ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *}
kleing@10497
   236
kleing@10497
   237
theorem "wf_prog wf_mb G ==> err_semilat (esl G)"
kleing@10497
   238
  by (frule acyclic_subcls1, frule univalent_subcls1, rule err_semilat_JType_esl_lemma)
kleing@10497
   239
kleing@10497
   240
end