src/HOL/MicroJava/Comp/LemmasComp.thy
author haftmann
Sat Mar 15 08:31:33 2014 +0100 (2014-03-15)
changeset 56154 f0a927235162
parent 55524 f41ef840f09d
child 58184 db1381d811ab
permissions -rw-r--r--
more complete set of lemmas wrt. image and composition
     1 (*  Title:      HOL/MicroJava/Comp/LemmasComp.thy
     2     Author:     Martin Strecker
     3 *)
     4 
     5 (* Lemmas for compiler correctness proof *)
     6 
     7 theory LemmasComp
     8 imports TranslComp
     9 begin
    10 
    11 
    12 declare split_paired_All [simp del]
    13 declare split_paired_Ex [simp del]
    14 
    15 
    16 (**********************************************************************)
    17 (* misc lemmas *)
    18 
    19 
    20 
    21 lemma split_pairs: "(\<lambda>(a,b). (F a b)) (ab) = F (fst ab) (snd ab)"
    22 proof -
    23   have "(\<lambda>(a,b). (F a b)) (fst ab,snd ab) = F (fst ab) (snd ab)"
    24     by (simp add: split_def)
    25   then show ?thesis by simp
    26 qed
    27 
    28 
    29 lemma c_hupd_conv: 
    30   "c_hupd h' (xo, (h,l)) = (xo, (if xo = None then h' else h),l)"
    31 by (simp add: c_hupd_def)
    32 
    33 lemma gl_c_hupd [simp]: "(gl (c_hupd h xs)) = (gl xs)"
    34 by (simp add: gl_def c_hupd_def split_pairs)
    35 
    36 lemma c_hupd_xcpt_invariant [simp]: "gx (c_hupd h' (xo, st)) = xo"
    37 by (cases st) (simp only: c_hupd_conv gx_conv)
    38 
    39 (* not added to simpset because of interference with c_hupd_conv *)
    40 lemma c_hupd_hp_invariant: "gh (c_hupd hp (None, st)) = hp"
    41 by (cases st) (simp add: c_hupd_conv gh_def)
    42 
    43 
    44 lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow>
    45   unique (map f xs) = unique xs"
    46 proof (induct xs)
    47   case Nil show ?case by simp
    48 next
    49   case (Cons a list)
    50   show ?case
    51   proof
    52     assume fst_eq: "\<forall>x\<in>set (a # list). fst x = fst (f x)"
    53 
    54     have fst_set: "(fst a \<in> fst ` set list) = (fst (f a) \<in> fst ` f ` set list)" 
    55     proof 
    56       assume as: "fst a \<in> fst ` set list" 
    57       then obtain x where fst_a_x: "x\<in>set list \<and> fst a = fst x" 
    58         by (auto simp add: image_iff)
    59       then have "fst (f a) = fst (f x)" by (simp add: fst_eq)
    60       with as show "(fst (f a) \<in> fst ` f ` set list)" by (simp add: fst_a_x)
    61     next
    62       assume as: "fst (f a) \<in> fst ` f ` set list"
    63       then obtain x where fst_a_x: "x\<in>set list \<and> fst (f a) = fst (f x)"
    64         by (auto simp add: image_iff)
    65       then have "fst a = fst x" by (simp add: fst_eq)
    66       with as show "fst a \<in> fst ` set list" by (simp add: fst_a_x)
    67     qed
    68 
    69     with fst_eq Cons 
    70     show "unique (map f (a # list)) = unique (a # list)"
    71       by (simp add: unique_def fst_set image_comp)
    72   qed
    73 qed
    74 
    75 lemma comp_unique: "unique (comp G) = unique G"
    76 apply (simp add: comp_def)
    77 apply (rule unique_map_fst)
    78 apply (simp add: compClass_def split_beta)
    79 done
    80 
    81 
    82 (**********************************************************************)
    83 (* invariance of properties under compilation *)
    84 
    85 lemma comp_class_imp:
    86   "(class G C = Some(D, fs, ms)) \<Longrightarrow> 
    87   (class (comp G) C = Some(D, fs, map (compMethod G C) ms))"
    88 apply (simp add: class_def comp_def compClass_def)
    89 apply (rule HOL.trans)
    90 apply (rule map_of_map2)
    91 apply auto
    92 done
    93 
    94 lemma comp_class_None: 
    95 "(class G C = None) = (class (comp G) C = None)"
    96 apply (simp add: class_def comp_def compClass_def)
    97 apply (simp add: map_of_in_set)
    98 apply (simp add: image_comp [THEN sym] o_def split_beta)
    99 done
   100 
   101 lemma comp_is_class: "is_class (comp G) C = is_class G C"
   102 by (cases "class G C") (auto simp: is_class_def comp_class_None dest: comp_class_imp)
   103 
   104 
   105 lemma comp_is_type: "is_type (comp G) T = is_type G T"
   106   apply (cases T)
   107   apply simp
   108   apply (induct G)
   109   apply simp
   110   apply (simp only: comp_is_class)
   111   apply (simp add: comp_is_class)
   112   apply (simp only: comp_is_class)
   113   done
   114 
   115 lemma comp_classname: "is_class G C 
   116   \<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))"
   117 by (cases "class G C") (auto simp: is_class_def dest: comp_class_imp)
   118 
   119 lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
   120 by (auto simp add: subcls1_def2 comp_classname comp_is_class)
   121 
   122 lemma comp_widen: "widen (comp G) = widen G"
   123   apply (simp add: fun_eq_iff)
   124   apply (intro allI iffI)
   125   apply (erule widen.cases) 
   126   apply (simp_all add: comp_subcls1 widen.null)
   127   apply (erule widen.cases) 
   128   apply (simp_all add: comp_subcls1 widen.null)
   129   done
   130 
   131 lemma comp_cast: "cast (comp G) = cast G"
   132   apply (simp add: fun_eq_iff)
   133   apply (intro allI iffI)
   134   apply (erule cast.cases) 
   135   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   136   apply (rule cast.widen) apply (simp add: comp_widen)
   137   apply (erule cast.cases)
   138   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   139   apply (rule cast.widen) apply (simp add: comp_widen)
   140   done
   141 
   142 lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G"
   143   by (simp add: fun_eq_iff cast_ok_def comp_widen)
   144 
   145 
   146 lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)"
   147 by (simp add: compClass_def split_beta)
   148 
   149 lemma compClass_fst_snd [simp]: "(fst (snd (compClass G C))) = (fst (snd C))"
   150 by (simp add: compClass_def split_beta)
   151 
   152 lemma compClass_fst_snd_snd [simp]: "(fst (snd (snd (compClass G C)))) = (fst (snd (snd C)))"
   153 by (simp add: compClass_def split_beta)
   154 
   155 lemma comp_wf_fdecl [simp]: "wf_fdecl (comp G) fd = wf_fdecl G fd"
   156 by (cases fd) (simp add: wf_fdecl_def comp_is_type)
   157 
   158 
   159 lemma compClass_forall [simp]: "
   160   (\<forall>x\<in>set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) =
   161   (\<forall>x\<in>set (snd (snd (snd C))). P (fst x) (fst (snd x)))"
   162 by (simp add: compClass_def compMethod_def split_beta)
   163 
   164 lemma comp_wf_mhead: "wf_mhead (comp G) S rT =  wf_mhead G S rT"
   165 by (simp add: wf_mhead_def split_beta comp_is_type)
   166 
   167 lemma comp_ws_cdecl: "
   168   ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C"
   169 apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1)
   170 apply (simp (no_asm_simp) add: comp_wf_mhead)
   171 apply (simp add: compClass_def compMethod_def split_beta unique_map_fst)
   172 done
   173 
   174 
   175 lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G"
   176 apply (simp add: wf_syscls_def comp_def compClass_def split_beta)
   177 apply (simp add: image_comp)
   178 apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
   179   (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
   180 apply simp
   181 apply (simp add: fun_eq_iff split_beta)
   182 done
   183 
   184 
   185 lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G"
   186 apply (rule sym)
   187 apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
   188 apply (simp add: comp_wf_syscls)
   189 apply (auto simp add: comp_ws_cdecl [THEN sym] TranslComp.comp_def)
   190 done
   191 
   192 
   193 lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow> 
   194 class_rec (comp G) C t f = 
   195   class_rec G C t (\<lambda> C' fs' ms' r'. f C' fs' (map (compMethod G C') ms') r')"
   196 apply (rule_tac a = C in  wf_induct) apply assumption
   197 apply (subgoal_tac "wf ((subcls1 (comp G))^-1)")
   198 apply (subgoal_tac "(class G x = None) \<or> (\<exists> D fs ms. (class G x = Some (D, fs, ms)))")
   199 apply (erule disjE)
   200 
   201   (* case class G x = None *)
   202 apply (simp (no_asm_simp) add: class_rec_def comp_subcls1
   203   wfrec [where r="(subcls1 G)^-1", simplified])
   204 apply (simp add: comp_class_None)
   205 
   206   (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
   207 apply (erule exE)+
   208 apply (frule comp_class_imp)
   209 apply (frule_tac G="comp G" and C=x and t=t and f=f in class_rec_lemma)
   210   apply assumption
   211 apply (frule_tac G=G and C=x and t=t 
   212    and f="(\<lambda>C' fs' ms'. f C' fs' (map (compMethod G C') ms'))" in class_rec_lemma)
   213   apply assumption
   214 apply (simp only:)
   215 
   216 apply (case_tac "x = Object")
   217   apply simp
   218   apply (frule subcls1I, assumption)
   219     apply (drule_tac x=D in spec, drule mp, simp)
   220     apply simp
   221 
   222   (* subgoals *)
   223 apply (case_tac "class G x")
   224 apply auto
   225 apply (simp add: comp_subcls1)
   226 done
   227 
   228 lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow> 
   229   fields (comp G,C) = fields (G,C)" 
   230 by (simp add: fields_def comp_class_rec)
   231 
   232 lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow> 
   233   field (comp G,C) = field (G,C)" 
   234 by (simp add: TypeRel.field_def comp_fields)
   235 
   236 
   237 
   238 lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk>  ws_prog G;
   239   \<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2);
   240    \<forall> C fs ms r1 r2. (R r1 r2) \<longrightarrow> (R (f1 C fs ms r1) (f2 C fs ms r2)) \<rbrakk>
   241   \<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow> 
   242   R (class_rec G C t1 f1) (class_rec G C t2 f2)"
   243 apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *)
   244 apply (rule_tac a = C in  wf_induct) apply assumption
   245 apply (intro strip)
   246 apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))")
   247   apply (erule exE)+
   248 apply (frule_tac C=x and t=t1 and f=f1 in class_rec_lemma)
   249   apply assumption
   250 apply (frule_tac C=x and t=t2 and f=f2 in class_rec_lemma)
   251   apply assumption
   252 apply (simp only:)
   253 
   254 apply (case_tac "x = Object")
   255   apply simp
   256   apply (frule subcls1I, assumption)
   257     apply (drule_tac x=D in spec, drule mp, simp)
   258     apply simp
   259     apply (subgoal_tac "(\<exists>D' rT' mb'. class G D = Some (D', rT', mb'))")
   260     apply blast
   261 
   262   (* subgoals *)
   263 
   264 apply (frule class_wf_struct) apply assumption
   265 apply (simp add: ws_cdecl_def is_class_def)
   266 
   267 apply (simp add: subcls1_def2 is_class_def)
   268 apply auto
   269 done
   270 
   271 
   272 abbreviation (input)
   273   "mtd_mb == snd o snd"
   274 
   275 lemma map_of_map:
   276   "map_of (map (\<lambda>(k, v). (k, f v)) xs) k = map_option f (map_of xs k)"
   277   by (simp add: map_of_map)
   278 
   279 lemma map_of_map_fst: "\<lbrakk> inj f;
   280   \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk>
   281   \<Longrightarrow>  map_of (map g xs) k 
   282   = map_option (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
   283 apply (induct xs)
   284 apply simp
   285 apply simp
   286 apply (case_tac "k = fst a")
   287 apply simp
   288 apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
   289 apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
   290 apply (erule conjE)+
   291 apply (drule_tac s ="fst (f a)" and t="fst a" in sym)
   292 apply simp
   293 apply (simp add: surjective_pairing)
   294 done
   295 
   296 lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
   297   ((method (comp G, C) S) = 
   298   map_option (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
   299              (method (G, C) S))"
   300 apply (simp add: method_def)
   301 apply (frule wf_subcls1)
   302 apply (simp add: comp_class_rec)
   303 apply (simp add: split_iter split_compose map_map [symmetric] del: map_map)
   304 apply (rule_tac R="%x y. ((x S) = (map_option (\<lambda>(D, rT, b). 
   305   (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   306   in class_rec_relation)
   307 apply assumption
   308 
   309 apply (intro strip)
   310 apply simp
   311 
   312 apply (rule trans)
   313 
   314 apply (rule_tac f="(\<lambda>(s, m). (s, Object, m))" and
   315   g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" 
   316   in map_of_map_fst)
   317 defer                           (* inj \<dots> *)
   318 apply (simp add: inj_on_def split_beta) 
   319 apply (simp add: split_beta compMethod_def)
   320 apply (simp add: map_of_map [symmetric])
   321 apply (simp add: split_beta)
   322 apply (simp add: Fun.comp_def split_beta)
   323 apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
   324                     (fst x, Object,
   325                      snd (compMethod G Object
   326                            (inv (\<lambda>(s\<Colon>sig, m\<Colon>ty \<times> vname list \<times> fdecl list \<times> stmt \<times> expr).
   327                                     (s, Object, m))
   328                              (S, Object, snd x)))))
   329   = (\<lambda>x. (fst x, Object, fst (snd x),
   330                         snd (snd (compMethod G Object (S, snd x)))))")
   331 apply (simp only:)
   332 apply (simp add: fun_eq_iff)
   333 apply (intro strip)
   334 apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
   335 apply (simp only:)
   336 apply (simp add: compMethod_def split_beta)
   337 apply (rule inv_f_eq) 
   338 defer
   339 defer
   340 
   341 apply (intro strip)
   342 apply (simp add: map_add_Some_iff map_of_map)
   343 apply (simp add: map_add_def)
   344 apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
   345 apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
   346   and k=S in map_of_map_fst) 
   347 apply (simp add: split_beta) 
   348 apply (simp add: compMethod_def split_beta)
   349 apply (case_tac "(map_of (map (\<lambda>(s, m). (s, Ca, m)) ms) S)")
   350 apply simp
   351 apply simp apply (simp add: split_beta map_of_map) apply (erule exE) apply (erule conjE)+
   352 apply (drule_tac t=a in sym)
   353 apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Ca, m)) (S, a)) = (S, snd a)")
   354 apply simp
   355 apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
   356    prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta)
   357 apply (simp add: map_of_map2)
   358 apply (simp (no_asm_simp) add: compMethod_def split_beta)
   359 
   360   -- "remaining subgoals"
   361 apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def)
   362 done
   363 
   364 
   365 
   366 lemma comp_wf_mrT: "\<lbrakk> ws_prog G; is_class G D\<rbrakk> \<Longrightarrow> 
   367   wf_mrT (TranslComp.comp G) (C, D, fs, map (compMethod G a) ms) =
   368   wf_mrT G (C, D, fs, ms)"
   369 apply (simp add: wf_mrT_def compMethod_def split_beta)
   370 apply (simp add: comp_widen)
   371 apply (rule iffI)
   372 apply (intro strip)
   373 apply simp
   374 apply (drule bspec) apply assumption
   375 apply (drule_tac x=D' in spec) apply (drule_tac x=rT' in spec) apply (drule mp)
   376 prefer 2 apply assumption
   377 apply (simp add: comp_method [of G D])
   378 apply (erule exE)+
   379 apply (simp add: split_paired_all)
   380 apply (intro strip)
   381 apply (simp add: comp_method)
   382 apply auto
   383 done
   384 
   385 
   386 (**********************************************************************)
   387   (* DIVERSE OTHER LEMMAS *)
   388 (**********************************************************************)
   389 
   390 lemma max_spec_preserves_length:
   391   "max_spec G C (mn, pTs) = {((md,rT),pTs')} 
   392   \<Longrightarrow> length pTs = length pTs'"
   393 apply (frule max_spec2mheads)
   394 apply (erule exE)+
   395 apply (simp add: list_all2_iff)
   396 done
   397 
   398 
   399 lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)"
   400 apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)")
   401 apply blast
   402 apply (rule ty_expr_ty_exprs_wt_stmt.induct)
   403 apply auto
   404 done
   405 
   406 
   407 lemma max_spec_preserves_method_rT [simp]:
   408   "max_spec G C (mn, pTs) = {((md,rT),pTs')}
   409   \<Longrightarrow> method_rT (the (method (G, C) (mn, pTs'))) = rT"
   410 apply (frule max_spec2mheads)
   411 apply (erule exE)+
   412 apply (simp add: method_rT_def)
   413 done
   414 
   415   (**********************************************************************************)
   416 
   417 declare compClass_fst [simp del]
   418 declare compClass_fst_snd [simp del]
   419 declare compClass_fst_snd_snd [simp del]
   420 
   421 declare split_paired_All [simp add]
   422 declare split_paired_Ex [simp add]
   423 
   424 end