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