src/HOL/MicroJava/J/TypeRel.thy
changeset 22271 51a80e238b29
parent 20970 c2a342e548a9
child 22597 284b2183d070
equal deleted inserted replaced
22270:4ccb7e6be929 22271:51a80e238b29
     6 
     6 
     7 header {* \isaheader{Relations between Java Types} *}
     7 header {* \isaheader{Relations between Java Types} *}
     8 
     8 
     9 theory TypeRel imports Decl begin
     9 theory TypeRel imports Decl begin
    10 
    10 
    11 consts
    11 -- "direct subclass, cf. 8.1.3"
    12   subcls1 :: "'c prog => (cname \<times> cname) set"  -- "subclass"
    12 inductive2
    13   widen   :: "'c prog => (ty    \<times> ty   ) set"  -- "widening"
       
    14   cast    :: "'c prog => (ty    \<times> ty   ) set"  -- "casting"
       
    15 
       
    16 syntax (xsymbols)
       
    17   subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    13   subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
       
    14   for G :: "'c prog"
       
    15 where
       
    16   subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
       
    17 
       
    18 abbreviation
    18   subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
    19   subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
    19   widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
    20   where "G\<turnstile>C \<preceq>C  D \<equiv> (subcls1 G)^** C D"
    20   cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
       
    21 
       
    22 syntax
       
    23   subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
       
    24   subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _"  [71,71,71] 70)
       
    25   widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _"   [71,71,71] 70)
       
    26   cast    :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <=? _"  [71,71,71] 70)
       
    27 
       
    28 translations
       
    29   "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
       
    30   "G\<turnstile>C \<preceq>C  D" == "(C,D) \<in> (subcls1 G)^*"
       
    31   "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
       
    32   "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
       
    33 
       
    34 -- "direct subclass, cf. 8.1.3"
       
    35 inductive "subcls1 G" intros
       
    36   subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
       
    37   
    21   
    38 lemma subcls1D: 
    22 lemma subcls1D: 
    39   "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
    23   "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
    40 apply (erule subcls1.elims)
    24 apply (erule subcls1.cases)
    41 apply auto
    25 apply auto
    42 done
    26 done
    43 
    27 
    44 lemma subcls1_def2: 
    28 lemma subcls1_def2: 
    45   "subcls1 G = 
    29   "subcls1 G = member2
    46      (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    30      (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    47   by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    31   by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I)
    48 
    32 
    49 lemma finite_subcls1: "finite (subcls1 G)"
    33 lemma finite_subcls1: "finite (Collect2 (subcls1 G))"
    50 apply(subst subcls1_def2)
    34 apply(simp add: subcls1_def2)
    51 apply(rule finite_SigmaI [OF finite_is_class])
    35 apply(rule finite_SigmaI [OF finite_is_class])
    52 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
    36 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
    53 apply  auto
    37 apply  auto
    54 done
    38 done
    55 
    39 
    56 lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ ==> is_class G C"
    40 lemma subcls_is_class: "(subcls1 G)^++ C D ==> is_class G C"
    57 apply (unfold is_class_def)
    41 apply (unfold is_class_def)
    58 apply(erule trancl_trans_induct)
    42 apply(erule trancl_trans_induct')
    59 apply (auto dest!: subcls1D)
    43 apply (auto dest!: subcls1D)
    60 done
    44 done
    61 
    45 
    62 lemma subcls_is_class2 [rule_format (no_asm)]: 
    46 lemma subcls_is_class2 [rule_format (no_asm)]: 
    63   "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
    47   "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
    64 apply (unfold is_class_def)
    48 apply (unfold is_class_def)
    65 apply (erule rtrancl_induct)
    49 apply (erule rtrancl_induct')
    66 apply  (drule_tac [2] subcls1D)
    50 apply  (drule_tac [2] subcls1D)
    67 apply  auto
    51 apply  auto
    68 done
    52 done
    69 
    53 
    70 constdefs
    54 constdefs
    71   class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
    55   class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
    72     (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    56     (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    73   "class_rec G == wfrec ((subcls1 G)^-1)
    57   "class_rec G == wfrec (Collect2 ((subcls1 G)^--1))
    74     (\<lambda>r C t f. case class G C of
    58     (\<lambda>r C t f. case class G C of
    75          None \<Rightarrow> arbitrary
    59          None \<Rightarrow> arbitrary
    76        | Some (D,fs,ms) \<Rightarrow> 
    60        | Some (D,fs,ms) \<Rightarrow> 
    77            f C fs ms (if C = Object then t else r D t f))"
    61            f C fs ms (if C = Object then t else r D t f))"
    78 
    62 
    79 lemma class_rec_lemma: "wf ((subcls1 G)^-1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
    63 lemma class_rec_lemma: "wfP ((subcls1 G)^--1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
    80  class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
    64  class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
    81   by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
    65   by (simp add: class_rec_def wfrec [to_pred]
       
    66     cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
    82 
    67 
    83 definition
    68 definition
    84   "wf_class G = wf ((subcls1 G)^-1)"
    69   "wf_class G = wfP ((subcls1 G)^--1)"
    85 
    70 
    86 lemma class_rec_func [code func]:
    71 lemma class_rec_func [code func]:
    87   "class_rec G C t f = (if wf_class G then
    72   "class_rec G C t f = (if wf_class G then
    88     (case class G C
    73     (case class G C
    89       of None \<Rightarrow> arbitrary
    74       of None \<Rightarrow> arbitrary
    91     else class_rec G C t f)"
    76     else class_rec G C t f)"
    92 proof (cases "wf_class G")
    77 proof (cases "wf_class G")
    93   case False then show ?thesis by auto
    78   case False then show ?thesis by auto
    94 next
    79 next
    95   case True
    80   case True
    96   from `wf_class G` have wf: "wf ((subcls1 G)^-1)"
    81   from `wf_class G` have wf: "wfP ((subcls1 G)^--1)"
    97     unfolding wf_class_def .
    82     unfolding wf_class_def .
    98   show ?thesis
    83   show ?thesis
    99   proof (cases "class G C")
    84   proof (cases "class G C")
   100     case None
    85     case None
   101     with wf show ?thesis
    86     with wf show ?thesis
   102       by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]])
    87       by (simp add: class_rec_def wfrec [to_pred]
       
    88         cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
   103   next
    89   next
   104     case (Some x) show ?thesis
    90     case (Some x) show ?thesis
   105     proof (cases x)
    91     proof (cases x)
   106       case (fields D fs ms)
    92       case (fields D fs ms)
   107       then have is_some: "class G C = Some (D, fs, ms)" using Some by simp
    93       then have is_some: "class G C = Some (D, fs, ms)" using Some by simp
   119 
   105 
   120 -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
   106 -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
   121 defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
   107 defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
   122                            ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
   108                            ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
   123 
   109 
   124 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   110 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==>
   125   method (G,C) = (if C = Object then empty else method (G,D)) ++  
   111   method (G,C) = (if C = Object then empty else method (G,D)) ++  
   126   map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
   112   map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
   127 apply (unfold method_def)
   113 apply (unfold method_def)
   128 apply (simp split del: split_if)
   114 apply (simp split del: split_if)
   129 apply (erule (1) class_rec_lemma [THEN trans]);
   115 apply (erule (1) class_rec_lemma [THEN trans]);
   133 
   119 
   134 -- "list of fields of a class, including inherited and hidden ones"
   120 -- "list of fields of a class, including inherited and hidden ones"
   135 defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
   121 defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
   136                            map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   122                            map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   137 
   123 
   138 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   124 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==>
   139  fields (G,C) = 
   125  fields (G,C) = 
   140   map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
   126   map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
   141 apply (unfold fields_def)
   127 apply (unfold fields_def)
   142 apply (simp split del: split_if)
   128 apply (simp split del: split_if)
   143 apply (erule (1) class_rec_lemma [THEN trans]);
   129 apply (erule (1) class_rec_lemma [THEN trans]);
   154 apply simp
   140 apply simp
   155 done
   141 done
   156 
   142 
   157 
   143 
   158 -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
   144 -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
   159 inductive "widen G" intros 
   145 inductive2
       
   146   widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
       
   147   for G :: "'c prog"
       
   148 where
   160   refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
   149   refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
   161   subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
   150 | subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
   162   null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
   151 | null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
   163 
   152 
   164 -- "casting conversion, cf. 5.5 / 5.1.5"
   153 -- "casting conversion, cf. 5.5 / 5.1.5"
   165 -- "left out casts on primitve types"
   154 -- "left out casts on primitve types"
   166 inductive "cast G" intros
   155 inductive2
       
   156   cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
       
   157   for G :: "'c prog"
       
   158 where
   167   widen:  "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
   159   widen:  "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
   168   subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
   160 | subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
   169 
   161 
   170 lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
   162 lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
   171 apply (rule iffI)
   163 apply (rule iffI)
   172 apply (erule widen.elims)
   164 apply (erule widen.cases)
   173 apply auto
   165 apply auto
   174 done
   166 done
   175 
   167 
   176 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
   168 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
   177 apply (ind_cases "G\<turnstile>S\<preceq>T")
   169 apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
   178 apply auto
   170 apply auto
   179 done
   171 done
   180 
   172 
   181 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
   173 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
   182 apply (ind_cases "G\<turnstile>S\<preceq>T")
   174 apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
   183 apply auto
   175 apply auto
   184 done
   176 done
   185 
   177 
   186 lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
   178 lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
   187 apply (ind_cases "G\<turnstile>S\<preceq>T")
   179 apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
   188 apply auto
   180 apply auto
   189 done
   181 done
   190 
   182 
   191 lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
   183 lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
   192 apply (rule iffI)
   184 apply (rule iffI)
   193 apply (ind_cases "G\<turnstile>S\<preceq>T")
   185 apply (ind_cases2 "G\<turnstile>Class C\<preceq>NT")
   194 apply auto
   186 apply auto
   195 done
   187 done
   196 
   188 
   197 lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
   189 lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
   198 apply (rule iffI)
   190 apply (rule iffI)
   199 apply (ind_cases "G\<turnstile>S\<preceq>T")
   191 apply (ind_cases2 "G\<turnstile>Class C \<preceq> Class D")
   200 apply (auto elim: widen.subcls)
   192 apply (auto elim: widen.subcls)
   201 done
   193 done
   202 
   194 
   203 lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
   195 lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
   204 by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
   196 by (ind_cases2 "G \<turnstile> T \<preceq> NT",  auto)
   205 
   197 
   206 lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
   198 lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
   207 apply (rule iffI)
   199 apply (rule iffI)
   208 apply (erule cast.elims)
   200 apply (erule cast.cases)
   209 apply auto
   201 apply auto
   210 done
   202 done
   211 
   203 
   212 lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT"
   204 lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT"
   213 apply (erule cast.cases)
   205 apply (erule cast.cases)
   221   proof induct
   213   proof induct
   222     case (refl T T') thus "G\<turnstile>T\<preceq>T'" .
   214     case (refl T T') thus "G\<turnstile>T\<preceq>T'" .
   223   next
   215   next
   224     case (subcls C D T)
   216     case (subcls C D T)
   225     then obtain E where "T = Class E" by (blast dest: widen_Class)
   217     then obtain E where "T = Class E" by (blast dest: widen_Class)
   226     with subcls show "G\<turnstile>Class C\<preceq>T" by (auto elim: rtrancl_trans)
   218     with subcls show "G\<turnstile>Class C\<preceq>T" by auto
   227   next
   219   next
   228     case (null R RT)
   220     case (null R RT)
   229     then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
   221     then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
   230     thus "G\<turnstile>NT\<preceq>RT" by auto
   222     thus "G\<turnstile>NT\<preceq>RT" by auto
   231   qed
   223   qed