src/HOL/MicroJava/BV/JType.thy
author kleing
Tue Jan 15 22:22:05 2002 +0100 (2002-01-15)
changeset 12773 a47f51daa6dc
parent 12516 d09d0f160888
child 12911 704713ca07ea
permissions -rw-r--r--
use exec_lub instead of some_lub
kleing@12516
     1
(*  Title:      HOL/MicroJava/BV/JType.thy
kleing@10497
     2
    ID:         $Id$
kleing@10812
     3
    Author:     Tobias Nipkow, Gerwin Klein
kleing@10497
     4
    Copyright   2000 TUM
kleing@10497
     5
*)
kleing@10497
     6
kleing@12516
     7
header "The Java Type System as Semilattice"
kleing@10497
     8
kleing@10497
     9
theory JType = WellForm + Err:
kleing@10497
    10
kleing@10497
    11
constdefs
kleing@12773
    12
  super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname"
kleing@12773
    13
  "super G C == fst (the (class G C))"
kleing@12773
    14
kleing@12773
    15
lemma superI:
kleing@12773
    16
  "(C,D) \<in> subcls1 G \<Longrightarrow> super G C = D"
kleing@12773
    17
  by (unfold super_def) (auto dest: subcls1D)
kleing@12773
    18
kleing@12773
    19
constdefs
kleing@10497
    20
  is_ref :: "ty => bool"
kleing@10497
    21
  "is_ref T == case T of PrimT t => False | RefT r => True"
kleing@10497
    22
kleing@10497
    23
  sup :: "'c prog => ty => ty => ty err"
kleing@10497
    24
  "sup G T1 T2 ==
kleing@12516
    25
  case T1 of PrimT P1 => (case T2 of PrimT P2 => 
kleing@12516
    26
                         (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
kleing@10497
    27
           | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => 
kleing@10497
    28
  (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
kleing@10497
    29
            | ClassT C => (case R2 of NullT => OK (Class C) 
kleing@12773
    30
                           | ClassT D => OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
kleing@10497
    31
kleing@10497
    32
  subtype :: "'c prog => ty => ty => bool"
kleing@11085
    33
  "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
kleing@10497
    34
kleing@10497
    35
  is_ty :: "'c prog => ty => bool"
kleing@10497
    36
  "is_ty G T == case T of PrimT P => True | RefT R =>
kleing@10497
    37
               (case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)"
kleing@10497
    38
kleing@12773
    39
kleing@10497
    40
translations
kleing@10497
    41
  "types G" == "Collect (is_type G)"
kleing@10497
    42
kleing@10497
    43
constdefs
kleing@10497
    44
  esl :: "'c prog => ty esl"
kleing@10497
    45
  "esl G == (types G, subtype G, sup G)"
kleing@10497
    46
kleing@11085
    47
lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
kleing@10497
    48
  by (auto elim: widen.elims)
kleing@10497
    49
kleing@11085
    50
lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
kleing@10497
    51
  by (auto elim: widen.elims)
kleing@10497
    52
kleing@10497
    53
lemma is_tyI:
kleing@10497
    54
  "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
kleing@10630
    55
  by (auto simp add: is_ty_def intro: subcls_C_Object 
kleing@10497
    56
           split: ty.splits ref_ty.splits)
kleing@10497
    57
kleing@10497
    58
lemma is_type_conv: 
kleing@10497
    59
  "wf_prog wf_mb G ==> is_type G T = is_ty G T"
kleing@10497
    60
proof
kleing@10497
    61
  assume "is_type G T" "wf_prog wf_mb G" 
kleing@10497
    62
  thus "is_ty G T"
kleing@10497
    63
    by (rule is_tyI)
kleing@10497
    64
next
kleing@10497
    65
  assume wf: "wf_prog wf_mb G" and
kleing@10497
    66
         ty: "is_ty G T"
kleing@10497
    67
kleing@10497
    68
  show "is_type G T"
kleing@10497
    69
  proof (cases T)
kleing@10497
    70
    case PrimT
kleing@10497
    71
    thus ?thesis by simp
kleing@10497
    72
  next
kleing@10497
    73
    fix R assume R: "T = RefT R"
kleing@10497
    74
    with wf
kleing@11085
    75
    have "R = ClassT Object \<Longrightarrow> ?thesis" by simp
kleing@10497
    76
    moreover    
kleing@10497
    77
    from R wf ty
kleing@11085
    78
    have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
berghofe@12443
    79
     by (auto simp add: is_ty_def is_class_def split_tupled_all
berghofe@12443
    80
               elim!: subcls1.elims
kleing@10497
    81
               elim: converse_rtranclE
berghofe@12443
    82
               split: ref_ty.splits)
kleing@10497
    83
    ultimately    
kleing@10497
    84
    show ?thesis by blast
kleing@10497
    85
  qed
kleing@10497
    86
qed
kleing@10497
    87
kleing@10497
    88
lemma order_widen:
kleing@10497
    89
  "acyclic (subcls1 G) ==> order (subtype G)"
kleing@10497
    90
  apply (unfold order_def lesub_def subtype_def)
kleing@10497
    91
  apply (auto intro: widen_trans)
kleing@10497
    92
  apply (case_tac x)
kleing@10497
    93
   apply (case_tac y)
kleing@10497
    94
    apply (auto simp add: PrimT_PrimT)
kleing@10497
    95
   apply (case_tac y)
kleing@10497
    96
    apply simp
kleing@10497
    97
  apply simp
kleing@10497
    98
  apply (case_tac ref_ty)
kleing@10497
    99
   apply (case_tac ref_tya)
kleing@10497
   100
    apply simp
kleing@10497
   101
   apply simp
kleing@10497
   102
  apply (case_tac ref_tya)
kleing@10497
   103
   apply simp
kleing@10497
   104
  apply simp
kleing@10497
   105
  apply (auto dest: acyclic_impl_antisym_rtrancl antisymD)  
kleing@10497
   106
  done
kleing@10497
   107
kleing@10592
   108
lemma wf_converse_subcls1_impl_acc_subtype:
kleing@10592
   109
  "wf ((subcls1 G)^-1) ==> acc (subtype G)"
kleing@10592
   110
apply (unfold acc_def lesssub_def)
kleing@10592
   111
apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
kleing@10592
   112
 apply blast
kleing@10592
   113
apply (drule wf_trancl)
kleing@10592
   114
apply (simp add: wf_eq_minimal)
kleing@10592
   115
apply clarify
kleing@10592
   116
apply (unfold lesub_def subtype_def)
kleing@10592
   117
apply (rename_tac M T) 
kleing@10592
   118
apply (case_tac "EX C. Class C : M")
kleing@10592
   119
 prefer 2
kleing@10592
   120
 apply (case_tac T)
kleing@10592
   121
  apply (fastsimp simp add: PrimT_PrimT2)
kleing@10592
   122
 apply simp
kleing@10592
   123
 apply (subgoal_tac "ref_ty = NullT")
kleing@10592
   124
  apply simp
kleing@10592
   125
  apply (rule_tac x = NT in bexI)
kleing@10592
   126
   apply (rule allI)
kleing@10592
   127
   apply (rule impI, erule conjE)
kleing@10592
   128
   apply (drule widen_RefT)
kleing@10592
   129
   apply clarsimp
kleing@10592
   130
   apply (case_tac t)
kleing@10592
   131
    apply simp
kleing@10592
   132
   apply simp
kleing@10592
   133
  apply simp
kleing@10592
   134
 apply (case_tac ref_ty)
kleing@10592
   135
  apply simp
kleing@10592
   136
 apply simp
kleing@10592
   137
apply (erule_tac x = "{C. Class C : M}" in allE)
kleing@10592
   138
apply auto
kleing@10592
   139
apply (rename_tac D)
kleing@10592
   140
apply (rule_tac x = "Class D" in bexI)
kleing@10592
   141
 prefer 2
kleing@10592
   142
 apply assumption
kleing@10592
   143
apply clarify 
kleing@10592
   144
apply (frule widen_RefT)
kleing@10592
   145
apply (erule exE)
kleing@10592
   146
apply (case_tac t)
kleing@10592
   147
 apply simp
kleing@10592
   148
apply simp
kleing@10592
   149
apply (insert rtrancl_r_diff_Id [symmetric, standard, of "(subcls1 G)"])
kleing@10592
   150
apply simp
kleing@10592
   151
apply (erule rtranclE)
kleing@10592
   152
 apply blast
kleing@10592
   153
apply (drule rtrancl_converseI)
kleing@10592
   154
apply (subgoal_tac "((subcls1 G)-Id)^-1 = ((subcls1 G)^-1 - Id)")
kleing@10592
   155
 prefer 2
kleing@10592
   156
 apply blast
kleing@10592
   157
apply simp 
kleing@10592
   158
apply (blast intro: rtrancl_into_trancl2)
kleing@10592
   159
done 
kleing@10592
   160
kleing@10497
   161
lemma closed_err_types:
nipkow@10797
   162
  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
kleing@10497
   163
  ==> closed (err (types G)) (lift2 (sup G))"
kleing@10497
   164
  apply (unfold closed_def plussub_def lift2_def sup_def)
kleing@10497
   165
  apply (auto split: err.split)
kleing@10497
   166
  apply (drule is_tyI, assumption)
kleing@10497
   167
  apply (auto simp add: is_ty_def is_type_conv simp del: is_type.simps 
kleing@12773
   168
              split: ty.split ref_ty.split)  
kleing@12773
   169
  apply (blast dest!: is_lub_exec_lub is_lubD is_ubD intro!: is_ubI superI)
kleing@10497
   170
  done
kleing@10497
   171
kleing@10497
   172
kleing@10896
   173
lemma sup_subtype_greater:
kleing@10896
   174
  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
kleing@10896
   175
      is_type G t1; is_type G t2; sup G t1 t2 = OK s |] 
kleing@11085
   176
  ==> subtype G t1 s \<and> subtype G t2 s"
kleing@10497
   177
proof -
kleing@10896
   178
  assume wf_prog:       "wf_prog wf_mb G"
nipkow@10797
   179
  assume single_valued: "single_valued (subcls1 G)" 
kleing@10896
   180
  assume acyclic:       "acyclic (subcls1 G)"
kleing@10896
   181
 
kleing@10497
   182
  { fix c1 c2
kleing@10497
   183
    assume is_class: "is_class G c1" "is_class G c2"
kleing@10497
   184
    with wf_prog 
kleing@10497
   185
    obtain 
kleing@11085
   186
      "G \<turnstile> c1 \<preceq>C Object"
kleing@11085
   187
      "G \<turnstile> c2 \<preceq>C Object"
kleing@10497
   188
      by (blast intro: subcls_C_Object)
nipkow@10797
   189
    with wf_prog single_valued
kleing@10497
   190
    obtain u where
kleing@10896
   191
      "is_lub ((subcls1 G)^* ) c1 c2 u"      
nipkow@10797
   192
      by (blast dest: single_valued_has_lubs)
kleing@12773
   193
    moreover
kleing@12773
   194
    note acyclic
kleing@12773
   195
    moreover
kleing@12773
   196
    have "\<forall>x y. (x, y) \<in> subcls1 G \<longrightarrow> super G x = y"
kleing@12773
   197
      by (blast intro: superI)
kleing@12773
   198
    ultimately
kleing@12773
   199
    have "G \<turnstile> c1 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2 \<and>
kleing@12773
   200
          G \<turnstile> c2 \<preceq>C exec_lub (subcls1 G) (super G) c1 c2"
kleing@12773
   201
      by (simp add: exec_lub_conv) (blast dest: is_lubD is_ubD)
kleing@10896
   202
  } note this [simp]
kleing@10497
   203
      
kleing@10896
   204
  assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s"
kleing@10896
   205
  thus ?thesis
kleing@10896
   206
    apply (unfold sup_def subtype_def) 
kleing@10896
   207
    apply (cases s)
kleing@10896
   208
    apply (auto split: ty.split_asm ref_ty.split_asm split_if_asm)
kleing@10896
   209
    done
kleing@10896
   210
qed
kleing@10497
   211
kleing@10896
   212
lemma sup_subtype_smallest:
kleing@10896
   213
  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
kleing@10896
   214
      is_type G a; is_type G b; is_type G c; 
kleing@10896
   215
      subtype G a c; subtype G b c; sup G a b = OK d |]
kleing@10896
   216
  ==> subtype G d c"
kleing@10896
   217
proof -
kleing@10896
   218
  assume wf_prog:       "wf_prog wf_mb G"
kleing@10896
   219
  assume single_valued: "single_valued (subcls1 G)" 
kleing@10896
   220
  assume acyclic:       "acyclic (subcls1 G)"
kleing@10497
   221
kleing@10497
   222
  { fix c1 c2 D
kleing@10497
   223
    assume is_class: "is_class G c1" "is_class G c2"
kleing@11085
   224
    assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
kleing@10497
   225
    from wf_prog is_class
kleing@10497
   226
    obtain 
kleing@11085
   227
      "G \<turnstile> c1 \<preceq>C Object"
kleing@11085
   228
      "G \<turnstile> c2 \<preceq>C Object"
kleing@10497
   229
      by (blast intro: subcls_C_Object)
nipkow@10797
   230
    with wf_prog single_valued
kleing@10497
   231
    obtain u where
kleing@10497
   232
      lub: "is_lub ((subcls1 G)^* ) c1 c2 u"
nipkow@10797
   233
      by (blast dest: single_valued_has_lubs)   
kleing@10497
   234
    with acyclic
kleing@12773
   235
    have "exec_lub (subcls1 G) (super G) c1 c2 = u"
kleing@12773
   236
      by (blast intro: superI exec_lub_conv)
kleing@10497
   237
    moreover
kleing@10497
   238
    from lub le
kleing@11085
   239
    have "G \<turnstile> u \<preceq>C D" 
kleing@10497
   240
      by (simp add: is_lub_def is_ub_def)
kleing@10497
   241
    ultimately     
kleing@12773
   242
    have "G \<turnstile> exec_lub (subcls1 G) (super G) c1 c2 \<preceq>C D"
kleing@10497
   243
      by blast
kleing@10497
   244
  } note this [intro]
kleing@10497
   245
kleing@10497
   246
  have [dest!]:
kleing@11085
   247
    "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
kleing@10497
   248
    by (frule widen_Class, auto)
kleing@10497
   249
kleing@10896
   250
  assume "is_type G a" "is_type G b" "is_type G c"
kleing@10896
   251
         "subtype G a c" "subtype G b c" "sup G a b = OK d"
kleing@10896
   252
  thus ?thesis
kleing@10896
   253
    by (auto simp add: subtype_def sup_def 
kleing@10896
   254
             split: ty.split_asm ref_ty.split_asm split_if_asm)
kleing@10896
   255
qed
kleing@10896
   256
kleing@10896
   257
lemma sup_exists:
kleing@10896
   258
  "[| subtype G a c; subtype G b c; sup G a b = Err |] ==> False"
kleing@10896
   259
  by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def subtype_def
kleing@10896
   260
           split: ty.splits ref_ty.splits)
kleing@10497
   261
kleing@10896
   262
lemma err_semilat_JType_esl_lemma:
kleing@10896
   263
  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
kleing@10896
   264
  ==> err_semilat (esl G)"
kleing@10896
   265
proof -
kleing@10896
   266
  assume wf_prog:   "wf_prog wf_mb G"
kleing@10896
   267
  assume single_valued: "single_valued (subcls1 G)" 
kleing@10896
   268
  assume acyclic:   "acyclic (subcls1 G)"
kleing@10896
   269
  
kleing@10896
   270
  hence "order (subtype G)"
kleing@10896
   271
    by (rule order_widen)
kleing@10896
   272
  moreover
kleing@10896
   273
  from wf_prog single_valued acyclic
kleing@10896
   274
  have "closed (err (types G)) (lift2 (sup G))"
kleing@10896
   275
    by (rule closed_err_types)
kleing@10896
   276
  moreover
kleing@10896
   277
kleing@10896
   278
  from wf_prog single_valued acyclic 
kleing@10896
   279
  have
kleing@11085
   280
    "(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and> 
kleing@11085
   281
     (\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
kleing@10896
   282
    by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split)
kleing@10896
   283
kleing@10896
   284
  moreover    
kleing@10896
   285
kleing@10896
   286
  from wf_prog single_valued acyclic 
kleing@10497
   287
  have
kleing@11085
   288
    "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G). 
kleing@11085
   289
    x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
kleing@10896
   290
    by (unfold lift2_def plussub_def lesub_def le_def)
kleing@10896
   291
       (auto intro: sup_subtype_smallest sup_exists split: err.split)
kleing@10497
   292
kleing@10497
   293
  ultimately
kleing@10497
   294
  
kleing@10497
   295
  show ?thesis
kleing@10497
   296
    by (unfold esl_def semilat_def sl_def) auto
kleing@10497
   297
qed
kleing@10497
   298
nipkow@10797
   299
lemma single_valued_subcls1:
nipkow@10797
   300
  "wf_prog wf_mb G ==> single_valued (subcls1 G)"
berghofe@12443
   301
  by (auto simp add: wf_prog_def unique_def single_valued_def
berghofe@12443
   302
    intro: subcls1I elim!: subcls1.elims)
kleing@10497
   303
kleing@10592
   304
theorem err_semilat_JType_esl:
kleing@10592
   305
  "wf_prog wf_mb G ==> err_semilat (esl G)"
nipkow@10797
   306
  by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
kleing@10497
   307
kleing@10497
   308
end