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