src/HOL/MicroJava/J/TypeRel.thy
author wenzelm
Sun Jan 16 15:53:03 2011 +0100 (2011-01-16)
changeset 41589 bbd861837ebc
parent 35416 d8d7d1b785af
child 44013 5cfc1c36ae97
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/MicroJava/J/TypeRel.thy
     2     Author:     David von Oheimb, Technische Universitaet Muenchen
     3 *)
     4 
     5 header {* \isaheader{Relations between Java Types} *}
     6 
     7 theory TypeRel imports Decl begin
     8 
     9 -- "direct subclass, cf. 8.1.3"
    10 
    11 inductive_set
    12   subcls1 :: "'c prog => (cname \<times> cname) set"
    13   and subcls1' :: "'c prog => cname \<Rightarrow> cname => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
    14   for G :: "'c prog"
    15 where
    16   "G \<turnstile> C \<prec>C1 D \<equiv> (C, D) \<in> subcls1 G"
    17   | subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G \<turnstile> C \<prec>C1 D"
    18 
    19 abbreviation
    20   subcls  :: "'c prog => cname \<Rightarrow> cname => bool" ("_ \<turnstile> _ \<preceq>C _"  [71,71,71] 70)
    21   where "G \<turnstile> C \<preceq>C D \<equiv> (C, D) \<in> (subcls1 G)^*"
    22 
    23 lemma subcls1D: 
    24   "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
    25 apply (erule subcls1.cases)
    26 apply auto
    27 done
    28 
    29 lemma subcls1_def2:
    30   "subcls1 P =
    31      (SIGMA C:{C. is_class P C}. {D. C\<noteq>Object \<and> fst (the (class P C))=D})"
    32   by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    33 
    34 lemma finite_subcls1: "finite (subcls1 G)"
    35 apply(simp add: subcls1_def2 del: mem_Sigma_iff)
    36 apply(rule finite_SigmaI [OF finite_is_class])
    37 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
    38 apply  auto
    39 done
    40 
    41 lemma subcls_is_class: "(C, D) \<in> (subcls1 G)^+  ==> is_class G C"
    42 apply (unfold is_class_def)
    43 apply(erule trancl_trans_induct)
    44 apply (auto dest!: subcls1D)
    45 done
    46 
    47 lemma subcls_is_class2 [rule_format (no_asm)]: 
    48   "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
    49 apply (unfold is_class_def)
    50 apply (erule rtrancl_induct)
    51 apply  (drule_tac [2] subcls1D)
    52 apply  auto
    53 done
    54 
    55 definition class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
    56     (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" where
    57   "class_rec G == wfrec ((subcls1 G)^-1)
    58     (\<lambda>r C t f. case class G C of
    59          None \<Rightarrow> undefined
    60        | Some (D,fs,ms) \<Rightarrow> 
    61            f C fs ms (if C = Object then t else r D t f))"
    62 
    63 lemma class_rec_lemma:
    64   assumes wf: "wf ((subcls1 G)^-1)"
    65     and cls: "class G C = Some (D, fs, ms)"
    66   shows "class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
    67 proof -
    68   from wf have step: "\<And>H a. wfrec ((subcls1 G)\<inverse>) H a =
    69     H (cut (wfrec ((subcls1 G)\<inverse>) H) ((subcls1 G)\<inverse>) a) a"
    70     by (rule wfrec)
    71   have cut: "\<And>f. C \<noteq> Object \<Longrightarrow> cut f ((subcls1 G)\<inverse>) C D = f D"
    72     by (rule cut_apply [where r="(subcls1 G)^-1", simplified, OF subcls1I, OF cls])
    73   from cls show ?thesis by (simp add: step cut class_rec_def)
    74 qed
    75 
    76 definition
    77   "wf_class G = wf ((subcls1 G)^-1)"
    78 
    79 
    80 text {* Code generator setup (FIXME!) *}
    81 
    82 consts_code
    83   "wfrec"   ("\<module>wfrec?")
    84 attach {*
    85 fun wfrec f x = f (wfrec f) x;
    86 *}
    87 
    88 consts
    89 
    90   method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
    91   field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    92   fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    93 
    94 -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
    95 defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts.
    96                            ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
    97 
    98 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
    99   method (G,C) = (if C = Object then empty else method (G,D)) ++  
   100   map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
   101 apply (unfold method_def)
   102 apply (simp split del: split_if)
   103 apply (erule (1) class_rec_lemma [THEN trans]);
   104 apply auto
   105 done
   106 
   107 
   108 -- "list of fields of a class, including inherited and hidden ones"
   109 defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C []    (\<lambda>C fs ms ts.
   110                            map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
   111 
   112 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
   113  fields (G,C) = 
   114   map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
   115 apply (unfold fields_def)
   116 apply (simp split del: split_if)
   117 apply (erule (1) class_rec_lemma [THEN trans]);
   118 apply auto
   119 done
   120 
   121 
   122 defs field_def: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
   123 
   124 lemma field_fields: 
   125 "field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
   126 apply (unfold field_def)
   127 apply (rule table_of_remap_SomeD)
   128 apply simp
   129 done
   130 
   131 
   132 -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
   133 inductive
   134   widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
   135   for G :: "'c prog"
   136 where
   137   refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T"   -- "identity conv., cf. 5.1.1"
   138 | subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
   139 | null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
   140 
   141 lemmas refl = HOL.refl
   142 
   143 -- "casting conversion, cf. 5.5 / 5.1.5"
   144 -- "left out casts on primitve types"
   145 inductive
   146   cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
   147   for G :: "'c prog"
   148 where
   149   widen:  "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D"
   150 | subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D"
   151 
   152 lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
   153 apply (rule iffI)
   154 apply (erule widen.cases)
   155 apply auto
   156 done
   157 
   158 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
   159 apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
   160 apply auto
   161 done
   162 
   163 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
   164 apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
   165 apply auto
   166 done
   167 
   168 lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
   169 apply (ind_cases "G\<turnstile>Class C\<preceq>T")
   170 apply auto
   171 done
   172 
   173 lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
   174 apply (rule iffI)
   175 apply (ind_cases "G\<turnstile>Class C\<preceq>NT")
   176 apply auto
   177 done
   178 
   179 lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
   180 apply (rule iffI)
   181 apply (ind_cases "G\<turnstile>Class C \<preceq> Class D")
   182 apply (auto elim: widen.subcls)
   183 done
   184 
   185 lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
   186 by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
   187 
   188 lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
   189 apply (rule iffI)
   190 apply (erule cast.cases)
   191 apply auto
   192 done
   193 
   194 lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT"
   195 apply (erule cast.cases)
   196 apply simp apply (erule widen.cases) 
   197 apply auto
   198 done
   199 
   200 theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   201 proof -
   202   assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
   203   proof induct
   204     case (refl T T') thus "G\<turnstile>T\<preceq>T'" .
   205   next
   206     case (subcls C D T)
   207     then obtain E where "T = Class E" by (blast dest: widen_Class)
   208     with subcls show "G\<turnstile>Class C\<preceq>T" by auto
   209   next
   210     case (null R RT)
   211     then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
   212     thus "G\<turnstile>NT\<preceq>RT" by auto
   213   qed
   214 qed
   215 
   216 end