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