src/HOL/MicroJava/J/TypeRel.thy
changeset 11026 a50365d21144
parent 10613 78b1d6c3ee9c
child 11070 cc421547e744
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Feb 01 20:51:48 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Feb 01 20:53:13 2001 +0100
     1.3 @@ -6,18 +6,18 @@
     1.4  The relations between Java types
     1.5  *)
     1.6  
     1.7 -TypeRel = Decl +
     1.8 +theory TypeRel = Decl:
     1.9  
    1.10  consts
    1.11 -  subcls1 :: "'c prog => (cname \\<times> cname) set"  (* subclass *)
    1.12 -  widen   :: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
    1.13 -  cast    :: "'c prog => (cname \\<times> cname) set"  (* casting *)
    1.14 +  subcls1 :: "'c prog => (cname \<times> cname) set"  (* subclass *)
    1.15 +  widen   :: "'c prog => (ty    \<times> ty   ) set"  (* widening *)
    1.16 +  cast    :: "'c prog => (cname \<times> cname) set"  (* casting *)
    1.17  
    1.18  syntax
    1.19 -  subcls1 :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<prec>C1 _" [71,71,71] 70)
    1.20 -  subcls  :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>C _" [71,71,71] 70)
    1.21 -  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \\<turnstile> _ \\<preceq> _" [71,71,71] 70)
    1.22 -  cast    :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>? _" [71,71,71] 70)
    1.23 +  subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    1.24 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
    1.25 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
    1.26 +  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
    1.27  
    1.28  syntax (HTML)
    1.29    subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
    1.30 @@ -26,58 +26,215 @@
    1.31    cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
    1.32  
    1.33  translations
    1.34 -  "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.35 -  "G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    1.36 -  "G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.37 -  "G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
    1.38 +  "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
    1.39 +  "G\<turnstile>C \<preceq>C  D" == "(C,D) \<in> (subcls1 G)^*"
    1.40 +  "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
    1.41 +  "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
    1.42  
    1.43  defs
    1.44  
    1.45    (* direct subclass, cf. 8.1.3 *)
    1.46 - subcls1_def"subcls1 G \\<equiv> {(C,D). C\\<noteq>Object \\<and> (\\<exists>c. class G C=Some c \\<and> fst c=D)}"
    1.47 + subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class G C=Some c \<and> fst c=D)}"
    1.48    
    1.49 +lemma subcls1D: 
    1.50 +  "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
    1.51 +apply (unfold subcls1_def)
    1.52 +apply auto
    1.53 +done
    1.54 +
    1.55 +lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
    1.56 +apply (unfold subcls1_def)
    1.57 +apply auto
    1.58 +done
    1.59 +
    1.60 +lemma subcls1_def2: 
    1.61 +"subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    1.62 +apply (unfold subcls1_def is_class_def)
    1.63 +apply auto
    1.64 +done
    1.65 +
    1.66 +lemma finite_subcls1: "finite (subcls1 G)"
    1.67 +apply(subst subcls1_def2)
    1.68 +apply(rule finite_SigmaI [OF finite_is_class])
    1.69 +apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
    1.70 +apply  auto
    1.71 +done
    1.72 +
    1.73 +lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ ==> is_class G C"
    1.74 +apply (unfold is_class_def)
    1.75 +apply(erule trancl_trans_induct)
    1.76 +apply (auto dest!: subcls1D)
    1.77 +done
    1.78 +
    1.79 +lemma subcls_is_class2 [rule_format (no_asm)]: "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
    1.80 +apply (unfold is_class_def)
    1.81 +apply (erule rtrancl_induct)
    1.82 +apply  (drule_tac [2] subcls1D)
    1.83 +apply  auto
    1.84 +done
    1.85 +
    1.86 +consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
    1.87 +        'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.88 +recdef class_rec "same_fst (\<lambda>G. wf ((subcls1 G)^-1)) (\<lambda>G. (subcls1 G)^-1)"
    1.89 +      "class_rec (G,C) = (\<lambda>t f. case class G C of None \<Rightarrow> arbitrary 
    1.90 +                         | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then 
    1.91 +      f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
    1.92 +recdef_tc class_rec_tc: class_rec
    1.93 +  apply (unfold same_fst_def)
    1.94 +  apply (auto intro: subcls1I)
    1.95 +  done
    1.96 +
    1.97 +lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
    1.98 + class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
    1.99 +  apply (rule class_rec_tc [THEN class_rec.simps 
   1.100 +              [THEN trans [THEN fun_cong [THEN fun_cong]]]])
   1.101 +  apply (rule ext, rule ext)
   1.102 +  apply auto
   1.103 +  done
   1.104 +
   1.105  consts
   1.106  
   1.107 -  method	:: "'c prog \\<times> cname => ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
   1.108 -  field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
   1.109 -  fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
   1.110 -
   1.111 -constdefs       (* auxiliary relation for recursive definitions below *)
   1.112 -
   1.113 -  subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
   1.114 - "subcls1_rel == {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
   1.115 +  method :: "'c prog \<times> cname => ( sig   \<leadsto> cname \<times> ty \<times> 'c)" (* ###curry *)
   1.116 +  field  :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty     )" (* ###curry *)
   1.117 +  fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
   1.118  
   1.119  (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
   1.120 -recdef method "subcls1_rel"
   1.121 - "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
   1.122 -                   | Some (D,fs,ms) => (if C = Object then empty else 
   1.123 -                                           if is_class G D then method (G,D) 
   1.124 -                                                           else arbitrary) ++
   1.125 -                                           map_of (map (\\<lambda>(s,  m ). 
   1.126 -                                                        (s,(C,m))) ms))
   1.127 -                  else arbitrary)"
   1.128 +defs method_def: "method \<equiv> \<lambda>(G,C). class_rec (G,C) empty (\<lambda>C fs ms ts.
   1.129 +                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
   1.130 +
   1.131 +lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   1.132 +  method (G,C) = (if C = Object then empty else method (G,D)) ++  
   1.133 +  map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
   1.134 +apply (unfold method_def)
   1.135 +apply (simp split del: split_if)
   1.136 +apply (erule (1) class_rec_lemma [THEN trans]);
   1.137 +apply auto
   1.138 +done
   1.139 +
   1.140  
   1.141  (* list of fields of a class, including inherited and hidden ones *)
   1.142 -recdef fields  "subcls1_rel"
   1.143 - "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
   1.144 -                   | Some (D,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
   1.145 -                                           (if C = Object then [] else 
   1.146 -                                           if is_class G D then fields (G,D) 
   1.147 -                                                           else arbitrary))
   1.148 -                  else arbitrary)"
   1.149 -defs
   1.150 +defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec (G,C) []    (\<lambda>C fs ms ts.
   1.151 +                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   1.152 +
   1.153 +lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   1.154 + fields (G,C) = 
   1.155 +  map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
   1.156 +apply (unfold fields_def)
   1.157 +apply (simp split del: split_if)
   1.158 +apply (erule (1) class_rec_lemma [THEN trans]);
   1.159 +apply auto
   1.160 +done
   1.161 +
   1.162 +
   1.163 +defs field_def: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
   1.164 +
   1.165 +lemma field_fields: 
   1.166 +"field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
   1.167 +apply (unfold field_def)
   1.168 +apply (rule table_of_remap_SomeD)
   1.169 +apply simp
   1.170 +done
   1.171 +
   1.172 +
   1.173 +inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3
   1.174 +			     i.e. sort of syntactic subtyping *)
   1.175 +  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
   1.176 +  subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
   1.177 +  null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
   1.178  
   1.179 -  field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
   1.180 +inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *)
   1.181 +                          (* left out casts on primitve types    *)
   1.182 +  widen:  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
   1.183 +  subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
   1.184 +
   1.185 +lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
   1.186 +apply (rule iffI)
   1.187 +apply (erule widen.elims)
   1.188 +apply auto
   1.189 +done
   1.190 +
   1.191 +lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
   1.192 +apply (ind_cases "G\<turnstile>S\<preceq>T")
   1.193 +apply auto
   1.194 +done
   1.195 +
   1.196 +lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
   1.197 +apply (ind_cases "G\<turnstile>S\<preceq>T")
   1.198 +apply auto
   1.199 +done
   1.200 +
   1.201 +lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
   1.202 +apply (ind_cases "G\<turnstile>S\<preceq>T")
   1.203 +apply auto
   1.204 +done
   1.205 +
   1.206 +lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
   1.207 +apply (rule iffI)
   1.208 +apply (ind_cases "G\<turnstile>S\<preceq>T")
   1.209 +apply auto
   1.210 +done
   1.211  
   1.212 -inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
   1.213 -			     i.e. sort of syntactic subtyping *)
   1.214 -  refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
   1.215 -  subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D"
   1.216 -  null	             "G\\<turnstile>     NT \\<preceq> RefT R"
   1.217 +lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
   1.218 +apply (rule iffI)
   1.219 +apply (ind_cases "G\<turnstile>S\<preceq>T")
   1.220 +apply (auto elim: widen.subcls)
   1.221 +done
   1.222 +
   1.223 +lemma widen_trans [rule_format (no_asm)]: "G\<turnstile>S\<preceq>U ==> \<forall>T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T"
   1.224 +apply (erule widen.induct)
   1.225 +apply   safe
   1.226 +apply  (frule widen_Class)
   1.227 +apply  (frule_tac [2] widen_RefT)
   1.228 +apply  safe
   1.229 +apply(erule (1) rtrancl_trans)
   1.230 +done
   1.231 +
   1.232 +ML {* InductAttrib.print_global_rules(the_context()) *}
   1.233 +ML {* set show_tags *}
   1.234  
   1.235 -inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
   1.236 -                         (* left out casts on primitve types    *)
   1.237 -  widen	 "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D"
   1.238 -  subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D"
   1.239 +(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   1.240 +proof -
   1.241 +  assume "G\<turnstile>S\<preceq>U"
   1.242 +  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
   1.243 +  proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1])
   1.244 +    case refl
   1.245 +    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
   1.246 +      (* fix T' show "PROP ?P T T".*)
   1.247 +  next
   1.248 +    case subcls
   1.249 +    fix T assume "G\<turnstile>Class D\<preceq>T"
   1.250 +    then obtain E where "T = Class E" by (blast dest: widen_Class)
   1.251 +    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
   1.252 +  next
   1.253 +    case null
   1.254 +    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
   1.255 +    then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
   1.256 +    thus "G\<turnstile>NT\<preceq>RT" by auto
   1.257 +  qed
   1.258 +qed
   1.259 +*)
   1.260 +
   1.261 +theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   1.262 +proof -
   1.263 +  assume "G\<turnstile>S\<preceq>U"
   1.264 +  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
   1.265 +  proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *)
   1.266 +    case refl
   1.267 +    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
   1.268 +      (* fix T' show "PROP ?P T T".*)
   1.269 +  next
   1.270 +    case subcls
   1.271 +    fix T assume "G\<turnstile>Class D\<preceq>T"
   1.272 +    then obtain E where "T = Class E" by (blast dest: widen_Class)
   1.273 +    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
   1.274 +  next
   1.275 +    case null
   1.276 +    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
   1.277 +    then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
   1.278 +    thus "G\<turnstile>NT\<preceq>RT" by auto
   1.279 +  qed
   1.280 +qed
   1.281 +
   1.282 +
   1.283  
   1.284  end