src/HOL/MicroJava/Comp/CorrComp.thy
author ballarin
Fri Aug 29 15:19:02 2003 +0200 (2003-08-29)
changeset 14174 f3cafd2929d5
parent 14143 7544966fa07d
child 14981 e73f8140af78
permissions -rw-r--r--
Methods rule_tac etc support static (Isar) contexts.
     1 (*  Title:      HOL/MicroJava/Comp/CorrComp.thy
     2     ID:         $Id$
     3     Author:     Martin Strecker
     4     Copyright   GPL 2002
     5 *)
     6 
     7 (* Compiler correctness statement and proof *)
     8 
     9 theory CorrComp =  JTypeSafe + LemmasComp:
    10 
    11 declare wf_prog_ws_prog [simp add]
    12 
    13 (* If no exception is present after evaluation/execution, 
    14   none can have been present before *)
    15 lemma eval_evals_exec_xcpt:
    16  "((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
    17   ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
    18   ((xs,st,xs') \<in> Eval.exec G \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
    19 by (induct rule: eval_evals_exec.induct, auto)
    20 
    21 
    22 (* instance of eval_evals_exec_xcpt for eval *)
    23 lemma eval_xcpt: "(xs,ex,val,xs') \<in> Eval.eval G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
    24  (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
    25 proof-
    26   assume h1: ?H1
    27   assume h2: ?H2
    28   from h1 h2 eval_evals_exec_xcpt show "?T" by simp
    29 qed
    30 
    31 (* instance of eval_evals_exec_xcpt for evals *)
    32 lemma evals_xcpt: "(xs,exs,vals,xs') \<in> Eval.evals G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
    33  (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
    34 proof-
    35   assume h1: ?H1
    36   assume h2: ?H2
    37   from h1 h2 eval_evals_exec_xcpt show "?T" by simp
    38 qed
    39 
    40 (* instance of eval_evals_exec_xcpt for exec *)
    41 lemma exec_xcpt: "(xs,st,xs') \<in> Eval.exec G \<Longrightarrow> gx xs' = None \<Longrightarrow> gx xs = None"
    42  (is "?H1 \<Longrightarrow> ?H2 \<Longrightarrow> ?T")
    43 proof-
    44   assume h1: ?H1
    45   assume h2: ?H2
    46   from h1 h2 eval_evals_exec_xcpt show "?T" by simp
    47 qed
    48 
    49 (**********************************************************************)
    50 
    51 theorem exec_all_trans: "\<lbrakk>(exec_all G s0 s1); (exec_all G s1 s2)\<rbrakk> \<Longrightarrow> (exec_all G s0 s2)"
    52 apply (auto simp: exec_all_def elim: Transitive_Closure.rtrancl_trans)
    53 done
    54 
    55 theorem exec_all_refl: "exec_all G s s"
    56 by (simp only: exec_all_def, rule rtrancl_refl)
    57 
    58 
    59 theorem exec_instr_in_exec_all:
    60   "\<lbrakk> exec_instr i G hp stk lvars C S pc frs =  (None, hp', frs');
    61              gis (gmb G C S) ! pc = i\<rbrakk>  \<Longrightarrow>
    62        G \<turnstile> (None, hp, (stk, lvars, C, S, pc) # frs) -jvm\<rightarrow> (None, hp', frs')"
    63 apply (simp only: exec_all_def)
    64 apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
    65 apply (simp add: gis_def gmb_def)
    66 apply (case_tac frs', simp+)
    67 done
    68 
    69 theorem exec_all_one_step: "
    70   \<lbrakk> gis (gmb G C S) = pre @ (i # post); pc0 = length pre;
    71   (exec_instr i G hp0 stk0 lvars0 C S pc0 frs) = 
    72   (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs) \<rbrakk>
    73   \<Longrightarrow> 
    74   G \<turnstile> (None, hp0, (stk0,lvars0,C,S, pc0)#frs) -jvm\<rightarrow> 
    75   (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs)"
    76 apply (unfold exec_all_def)
    77 apply (rule r_into_rtrancl)
    78 apply (simp add: gis_def gmb_def split_beta)
    79 done
    80 
    81 
    82 (***********************************************************************)
    83 
    84 constdefs
    85   progression :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
    86                  aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow>
    87                  bytecode \<Rightarrow>
    88                  aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow> 
    89                  bool"
    90   ("{_,_,_} \<turnstile> {_, _, _} >- _ \<rightarrow> {_, _, _}" [61,61,61,61,61,61,90,61,61,61]60)
    91   "{G,C,S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1} ==
    92   \<forall> pre post frs.
    93   (gis (gmb G C S) = pre @ instrs @ post) \<longrightarrow>
    94    G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) -jvm\<rightarrow>
    95        (None,hp1,(os1,lvars1,C,S,(length pre) + (length instrs))#frs)"
    96 
    97 
    98 
    99 lemma progression_call: 
   100   "\<lbrakk> \<forall> pc frs.
   101   exec_instr instr G hp0 os0 lvars0 C S pc frs =
   102       (None, hp', (os', lvars', C', S', 0) # (fr pc) # frs) \<and> 
   103   gis (gmb G C' S') = instrs' @ [Return] \<and> 
   104   {G, C', S'} \<turnstile> {hp', os', lvars'} >- instrs' \<rightarrow> {hp'', os'', lvars''}  \<and>
   105   exec_instr Return G hp'' os'' lvars'' C' S' (length instrs') 
   106                                                ((fr pc) # frs) =
   107       (None, hp2, (os2, lvars2, C, S, Suc pc) # frs) \<rbrakk> \<Longrightarrow>
   108   {G, C, S} \<turnstile> {hp0, os0, lvars0} >-[instr]\<rightarrow> {hp2,os2,lvars2}"
   109 apply (simp only: progression_def)
   110 apply (intro strip)
   111 apply (drule_tac x="length pre" in spec)
   112 apply (drule_tac x="frs" in spec)
   113 apply clarify
   114 apply (rule exec_all_trans)
   115 apply (rule exec_instr_in_exec_all) apply simp
   116 apply simp
   117 apply (rule exec_all_trans)
   118 apply (simp only: append_Nil)
   119 apply (drule_tac x="[]" in spec)
   120 apply (simp only: list.simps)
   121 apply blast
   122 apply (rule exec_instr_in_exec_all)
   123 apply auto
   124 done
   125 
   126 
   127 lemma progression_transitive: 
   128   "\<lbrakk> instrs_comb = instrs0 @ instrs1; 
   129   {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs0 \<rightarrow> {hp1, os1, lvars1};
   130   {G, C, S} \<turnstile> {hp1, os1, lvars1} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk>
   131   \<Longrightarrow>
   132   {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
   133 apply (simp only: progression_def)
   134 apply (intro strip)
   135 apply (rule_tac ?s1.0 = "Norm (hp1, (os1, lvars1, C, S, 
   136                           length pre + length instrs0) # frs)"  
   137        in exec_all_trans)
   138 apply (simp only: append_assoc)
   139 apply (erule thin_rl, erule thin_rl)
   140 apply (drule_tac x="pre @ instrs0" in spec)
   141 apply (simp add: add_assoc)
   142 done
   143 
   144 lemma progression_refl: 
   145   "{G, C, S} \<turnstile> {hp0, os0, lvars0} >- [] \<rightarrow> {hp0, os0, lvars0}"
   146 apply (simp add: progression_def)
   147 apply (intro strip)
   148 apply (rule exec_all_refl)
   149 done
   150 
   151 lemma progression_one_step: "
   152   \<forall> pc frs. 
   153   (exec_instr i G hp0 os0 lvars0 C S pc frs) = 
   154   (None, hp1, (os1,lvars1,C,S, Suc pc)#frs)
   155   \<Longrightarrow> {G, C, S} \<turnstile> {hp0, os0, lvars0} >- [i] \<rightarrow> {hp1, os1, lvars1}"
   156 apply (unfold progression_def)
   157 apply (intro strip)
   158 apply simp
   159 apply (rule exec_all_one_step)
   160 apply auto
   161 done
   162 
   163 (*****)
   164 constdefs
   165   jump_fwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
   166                  aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
   167                  instr \<Rightarrow> bytecode \<Rightarrow> bool"
   168   "jump_fwd G C S hp lvars os0 os1 instr instrs ==
   169   \<forall> pre post frs.
   170   (gis (gmb G C S) = pre @ instr # instrs @ post) \<longrightarrow>
   171    exec_all G (None,hp,(os0,lvars,C,S, length pre)#frs)
   172     (None,hp,(os1,lvars,C,S,(length pre) + (length instrs) + 1)#frs)"
   173 
   174 
   175 lemma jump_fwd_one_step:
   176   "\<forall> pc frs.
   177   exec_instr instr G hp os0 lvars C S pc frs = 
   178     (None, hp, (os1, lvars, C, S, pc + (length instrs) + 1)#frs)
   179   \<Longrightarrow> jump_fwd G C S hp lvars os0 os1 instr instrs"
   180 apply (unfold jump_fwd_def)
   181 apply (intro strip)
   182 apply (rule exec_instr_in_exec_all)
   183 apply auto
   184 done
   185 
   186 
   187 lemma jump_fwd_progression_aux: 
   188   "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; 
   189      jump_fwd G C S hp lvars os0 os1 instr instrs0;
   190      {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> 
   191   \<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
   192 apply (simp only: progression_def jump_fwd_def)
   193 apply (intro strip)
   194 apply (rule_tac ?s1.0 = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
   195 apply (simp only: append_assoc)
   196 apply (subgoal_tac "pre @ (instr # instrs0 @ instrs1) @ post = pre @ instr # instrs0 @ (instrs1 @ post)")
   197 apply blast
   198 apply simp
   199 apply (erule thin_rl, erule thin_rl)
   200 apply (drule_tac x="pre @ instr # instrs0" in spec)
   201 apply (simp add: add_assoc)
   202 done
   203 
   204 
   205 lemma jump_fwd_progression:
   206   "\<lbrakk> instrs_comb = instr # instrs0 @ instrs1; 
   207   \<forall> pc frs.
   208   exec_instr instr G hp os0 lvars C S pc frs = 
   209     (None, hp, (os1, lvars, C, S, pc + (length instrs0) + 1)#frs);
   210   {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk> 
   211   \<Longrightarrow> {G, C, S}  \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
   212 apply (rule jump_fwd_progression_aux)
   213 apply assumption
   214 apply (rule jump_fwd_one_step) apply assumption+
   215 done
   216 
   217 
   218 (* note: instrs and instr reversed wrt. jump_fwd *)
   219 constdefs
   220   jump_bwd :: "jvm_prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 
   221                  aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow> 
   222                  bytecode \<Rightarrow> instr \<Rightarrow> bool"
   223   "jump_bwd G C S hp lvars os0 os1 instrs instr ==
   224   \<forall> pre post frs.
   225   (gis (gmb G C S) = pre @ instrs @ instr # post) \<longrightarrow>
   226    exec_all G (None,hp,(os0,lvars,C,S, (length pre) + (length instrs))#frs)
   227     (None,hp,(os1,lvars,C,S, (length pre))#frs)"
   228 
   229 
   230 lemma jump_bwd_one_step:
   231   "\<forall> pc frs.
   232   exec_instr instr G hp os0 lvars C S (pc + (length instrs)) frs = 
   233     (None, hp, (os1, lvars, C, S, pc)#frs)
   234   \<Longrightarrow> 
   235   jump_bwd G C S hp lvars os0 os1 instrs instr"
   236 apply (unfold jump_bwd_def)
   237 apply (intro strip)
   238 apply (rule exec_instr_in_exec_all)
   239 apply auto
   240 done
   241 
   242 lemma jump_bwd_progression: 
   243   "\<lbrakk> instrs_comb = instrs @ [instr]; 
   244   {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1};
   245   jump_bwd G C S hp1 lvars1 os1 os2 instrs instr;
   246   {G, C, S} \<turnstile> {hp1, os2, lvars1} >- instrs_comb \<rightarrow> {hp3, os3, lvars3} \<rbrakk> 
   247   \<Longrightarrow> {G, C, S}  \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp3, os3, lvars3}"
   248 apply (simp only: progression_def jump_bwd_def)
   249 apply (intro strip)
   250 apply (rule exec_all_trans, force)
   251 apply (rule exec_all_trans, force)
   252 apply (rule exec_all_trans, force)
   253 apply simp
   254 apply (rule exec_all_refl)
   255 done
   256 
   257 
   258 (**********************************************************************)
   259 
   260 (* class C with signature S is defined in program G *)
   261 constdefs class_sig_defined :: "'c prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> bool"
   262   "class_sig_defined G C S == 
   263   is_class G C \<and> (\<exists> D rT mb. (method (G, C) S = Some (D, rT, mb)))"
   264 
   265 
   266 (* The environment of a java method body 
   267   (characterized by class and signature) *)
   268 constdefs env_of_jmb :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> java_mb env"
   269   "env_of_jmb G C S == 
   270   (let (mn,pTs) = S;
   271        (D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in
   272   (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))"
   273 
   274 lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G"
   275 by (simp add: env_of_jmb_def split_beta)
   276 
   277 
   278 (**********************************************************************)
   279 
   280 
   281 lemma method_preserves [rule_format (no_asm)]:
   282   "\<lbrakk> wf_prog wf_mb G; is_class G C; 
   283   \<forall> S rT mb. \<forall> cn \<in> fst ` set G. wf_mdecl wf_mb G cn (S,rT,mb)  \<longrightarrow> (P cn S (rT,mb))\<rbrakk>
   284  \<Longrightarrow> \<forall> D. 
   285   method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))"
   286 
   287 apply (frule wf_prog_ws_prog [THEN wf_subcls1])
   288 apply (rule subcls1_induct, assumption, assumption)
   289 
   290 apply (intro strip)
   291 apply ((drule spec)+, drule_tac x="Object" in bspec)
   292 apply (simp add: wf_prog_def ws_prog_def wf_syscls_def)
   293 apply (subgoal_tac "D=Object") apply simp
   294 apply (drule mp)
   295 apply (frule_tac C=Object in method_wf_mdecl)
   296  apply simp
   297  apply assumption apply simp apply assumption apply simp
   298 
   299 apply (subst method_rec) apply simp
   300 apply force
   301 apply simp
   302 apply (simp only: map_add_def)
   303 apply (split option.split)
   304 apply (rule conjI)
   305 apply force
   306 apply (intro strip)
   307 apply (frule_tac
   308   ?P1.0 = "wf_mdecl wf_mb G Ca" and
   309   ?P2.0 = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
   310 apply (force simp: wf_cdecl_def)
   311 
   312 apply clarify
   313 
   314 apply (simp only: class_def)
   315 apply (drule map_of_SomeD)+
   316 apply (frule_tac A="set G" and f=fst in imageI, simp)
   317 apply blast
   318 apply simp
   319 done
   320 
   321 
   322 lemma method_preserves_length:
   323   "\<lbrakk> wf_java_prog G; is_class G C; 
   324   method (G, C) (mn,pTs) = Some (D, rT, pns, lvars, blk, res)\<rbrakk>
   325  \<Longrightarrow> length pns = length pTs"
   326 apply (frule_tac 
   327   P="%D (mn,pTs) (rT, pns, lvars, blk, res). length pns = length pTs"
   328   in method_preserves)
   329 apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
   330 done
   331 
   332 (**********************************************************************)
   333 
   334 constdefs wtpd_expr :: "java_mb env \<Rightarrow> expr \<Rightarrow> bool"
   335   "wtpd_expr E e == (\<exists> T. E\<turnstile>e :: T)"
   336   wtpd_exprs :: "java_mb env \<Rightarrow> (expr list) \<Rightarrow> bool"
   337   "wtpd_exprs E e == (\<exists> T. E\<turnstile>e [::] T)"
   338   wtpd_stmt :: "java_mb env \<Rightarrow> stmt \<Rightarrow> bool" 
   339   "wtpd_stmt E c == (E\<turnstile>c \<surd>)"
   340 
   341 lemma wtpd_expr_newc: "wtpd_expr E (NewC C) \<Longrightarrow> is_class (prg E) C"
   342 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
   343 
   344 lemma wtpd_expr_cast: "wtpd_expr E (Cast cn e) \<Longrightarrow> (wtpd_expr E e)"
   345 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
   346 
   347 lemma wtpd_expr_lacc: "\<lbrakk> wtpd_expr (env_of_jmb G C S) (LAcc vn);
   348   class_sig_defined G C S \<rbrakk>
   349   \<Longrightarrow> vn \<in> set (gjmb_plns (gmb G C S)) \<or> vn = This"
   350 apply (simp only: wtpd_expr_def env_of_jmb_def class_sig_defined_def galldefs)
   351 apply clarify
   352 apply (case_tac S)
   353 apply simp
   354 apply (erule ty_expr.cases)
   355 apply (auto dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
   356 apply (drule map_upds_SomeD)
   357 apply (erule disjE)
   358   apply assumption
   359   apply (drule map_of_SomeD) apply (auto dest: fst_in_set_lemma)
   360 done
   361 
   362 lemma wtpd_expr_lass: "wtpd_expr E (vn::=e)
   363   \<Longrightarrow> (vn \<noteq> This) & (wtpd_expr E (LAcc vn)) & (wtpd_expr E e)"
   364 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
   365 
   366 lemma wtpd_expr_facc: "wtpd_expr E ({fd}a..fn) 
   367   \<Longrightarrow> (wtpd_expr E a)"
   368 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
   369 
   370 lemma wtpd_expr_fass: "wtpd_expr E ({fd}a..fn:=v) 
   371   \<Longrightarrow> (wtpd_expr E ({fd}a..fn)) & (wtpd_expr E v)"
   372 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
   373 
   374 
   375 lemma wtpd_expr_binop: "wtpd_expr E (BinOp bop e1 e2)
   376   \<Longrightarrow> (wtpd_expr E e1) & (wtpd_expr E e2)"
   377 by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)
   378 
   379 lemma wtpd_exprs_cons: "wtpd_exprs E (e # es)
   380   \<Longrightarrow> (wtpd_expr E e) & (wtpd_exprs E es)"
   381 by (simp only: wtpd_exprs_def wtpd_expr_def, erule exE, erule ty_exprs.cases, auto)
   382 
   383 lemma wtpd_stmt_expr: "wtpd_stmt E (Expr e) \<Longrightarrow> (wtpd_expr E e)"
   384 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
   385 
   386 lemma wtpd_stmt_comp: "wtpd_stmt E (s1;; s2) \<Longrightarrow> 
   387    (wtpd_stmt E s1) &  (wtpd_stmt E s2)"
   388 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
   389 
   390 lemma wtpd_stmt_cond: "wtpd_stmt E (If(e) s1 Else s2) \<Longrightarrow>
   391    (wtpd_expr E e) & (wtpd_stmt E s1) &  (wtpd_stmt E s2)
   392   & (E\<turnstile>e::PrimT Boolean)"
   393 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
   394 
   395 lemma wtpd_stmt_loop: "wtpd_stmt E (While(e) s) \<Longrightarrow>
   396    (wtpd_expr E e) & (wtpd_stmt E s) & (E\<turnstile>e::PrimT Boolean)"
   397 by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)
   398 
   399 lemma wtpd_expr_call: "wtpd_expr E ({C}a..mn({pTs'}ps))
   400   \<Longrightarrow> (wtpd_expr E a) & (wtpd_exprs E ps) 
   401   & (length ps = length pTs') & (E\<turnstile>a::Class C)
   402   & (\<exists> pTs md rT. 
   403        E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
   404 apply (simp only: wtpd_expr_def wtpd_exprs_def)
   405 apply (erule exE)
   406 apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T")
   407 apply (auto simp: max_spec_preserves_length)
   408 done
   409 
   410 lemma wtpd_blk: 
   411   "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
   412   wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
   413  \<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk"
   414 apply (simp add: wtpd_stmt_def env_of_jmb_def)
   415 apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> blk \<surd> " in method_preserves)
   416 apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
   417 done
   418 
   419 lemma wtpd_res: 
   420   "\<lbrakk> method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res)); 
   421   wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
   422  \<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res"
   423 apply (simp add: wtpd_expr_def env_of_jmb_def)
   424 apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \<exists>T. (G, map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class D)) \<turnstile> res :: T " in method_preserves)
   425 apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
   426 done
   427 
   428 
   429 (**********************************************************************)
   430 
   431 
   432 (* Is there a more elegant proof? *)
   433 lemma evals_preserves_length:
   434   "G\<turnstile> xs -es[\<succ>]vs-> (None, s) \<Longrightarrow> length es = length vs"
   435 apply (subgoal_tac 
   436   "\<forall> xs'. (G \<turnstile> xk -xj\<succ>xi-> xh \<longrightarrow> True) & 
   437   (G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow>  (\<exists> s. (xs' = (None, s))) \<longrightarrow> 
   438   length es = length vs) &
   439   ((xc, xb, xa) \<in> Eval.exec G \<longrightarrow> True)")
   440 apply blast
   441 apply (rule allI)
   442 apply (rule Eval.eval_evals_exec.induct)
   443 apply auto
   444 done
   445 
   446 (***********************************************************************)
   447 
   448 (* required for translation of BinOp *)
   449 
   450 
   451 lemma progression_Eq : "{G, C, S} \<turnstile>
   452   {hp, (v2 # v1 # os), lvars} 
   453   >- [Ifcmpeq 3, LitPush (Bool False), Goto 2, LitPush (Bool True)] \<rightarrow>
   454   {hp, (Bool (v1 = v2) # os), lvars}"
   455 apply (case_tac "v1 = v2")
   456 
   457 (* case v1 = v2 *)
   458 apply (rule_tac ?instrs1.0 = "[LitPush (Bool True)]" in jump_fwd_progression)
   459 apply (auto simp: nat_add_distrib)
   460 apply (rule progression_one_step) apply simp
   461 
   462 (* case v1 \<noteq> v2 *)
   463 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified])
   464 apply auto
   465 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) 
   466 apply auto
   467 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
   468 apply (auto simp: nat_add_distrib intro: progression_refl)
   469 done
   470 
   471 
   472 (**********************************************************************)
   473 
   474 
   475 (* to avoid automatic pair splits *)
   476 
   477 declare split_paired_All [simp del] split_paired_Ex [simp del]
   478 ML_setup {*
   479 simpset_ref() := simpset() delloop "split_all_tac"
   480 *}
   481 
   482 lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; 
   483   method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
   484   distinct (gjmb_plns (gmb G C S))"
   485 apply (frule method_wf_mdecl [THEN conjunct2],  assumption, assumption)
   486 apply (case_tac S)
   487 apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs distinct_append)
   488 apply (simp add: unique_def map_of_in_set)
   489 apply blast
   490 done
   491 
   492 lemma distinct_method_if_class_sig_defined : 
   493   "\<lbrakk> wf_java_prog G; class_sig_defined G C S \<rbrakk> \<Longrightarrow> 
   494   distinct (gjmb_plns (gmb G C S))"
   495 by (auto intro: distinct_method simp: class_sig_defined_def)
   496 
   497 
   498 lemma method_yields_wf_java_mdecl: "\<lbrakk> wf_java_prog G; is_class G C;
   499   method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk>  \<Longrightarrow> 
   500   wf_java_mdecl G D (S,rT,(pns,lvars,blk,res))"
   501 apply (frule method_wf_mdecl)
   502 apply (auto simp: wf_mdecl_def)
   503 done
   504 
   505 (**********************************************************************)
   506 
   507 
   508 lemma progression_lvar_init_aux [rule_format (no_asm)]: "
   509   \<forall> zs prfx lvals lvars0. 
   510   lvars0 =  (zs @ lvars) \<longrightarrow>
   511   (disjoint_varnames pns lvars0 \<longrightarrow>
   512   (length lvars = length lvals) \<longrightarrow> 
   513   (Suc(length pns + length zs) = length prfx) \<longrightarrow> 
   514    ({cG, D, S} \<turnstile> 
   515     {h, os, (prfx @ lvals)}
   516     >- (concat (map (compInit (pns, lvars0, blk, res)) lvars)) \<rightarrow>
   517     {h, os, (prfx @ (map (\<lambda>p. (default_val (snd p))) lvars))}))"
   518 apply simp
   519 apply (induct lvars)
   520 apply (clarsimp, rule progression_refl)
   521 apply (intro strip)
   522 apply (case_tac lvals) apply simp
   523 apply (simp (no_asm_simp) )
   524 
   525 apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
   526 apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
   527 apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
   528 apply (rule progression_one_step)
   529 apply (simp (no_asm_simp) add: load_default_val_def)
   530 apply (rule conjI, simp)+ apply (rule HOL.refl)
   531 
   532 apply (rule progression_one_step)
   533 apply (simp (no_asm_simp))
   534 apply (rule conjI, simp)+
   535 apply (simp add: index_of_var2)
   536 apply (drule_tac x="zs @ [a]" in spec) (* instantiate zs *)
   537 apply (drule mp, simp)
   538 apply (drule_tac x="(prfx @ [default_val (snd a)])" in spec) (* instantiate prfx *)
   539 apply auto
   540 done
   541 
   542 lemma progression_lvar_init [rule_format (no_asm)]: 
   543   "\<lbrakk> wf_java_prog G; is_class G C;
   544   method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
   545   length pns = length pvs \<longrightarrow> 
   546   (\<forall> lvals. 
   547   length lvars = length lvals \<longrightarrow>
   548    {cG, D, S} \<turnstile>
   549    {h, os, (a' # pvs @ lvals)}
   550    >- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow>
   551    {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})"
   552 apply (simp only: compInitLvars_def)
   553 apply (frule method_yields_wf_java_mdecl, assumption, assumption)
   554 
   555 apply (simp only: wf_java_mdecl_def)
   556 apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
   557 apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd)
   558 apply (intro strip)
   559 apply (simp (no_asm_simp) only: append_Cons [THEN sym])
   560 apply (rule progression_lvar_init_aux)
   561 apply (auto simp: unique_def map_of_in_set disjoint_varnames_def)
   562 done
   563 
   564 
   565 
   566 
   567 (**********************************************************************)
   568 
   569 lemma state_ok_eval: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_expr E e;
   570   (prg E)\<turnstile>xs -e\<succ>v -> xs'\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
   571 apply (simp only: wtpd_expr_def)
   572 apply (erule exE)
   573 apply (case_tac xs', case_tac xs)
   574 apply (auto intro: eval_type_sound [THEN conjunct1])
   575 done
   576 
   577 lemma state_ok_evals: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_exprs E es;
   578   (xs,es,vs,xs') \<in> Eval.evals (prg E)\<rbrakk> \<Longrightarrow> xs'::\<preceq>E"
   579 apply (simp only: wtpd_exprs_def)
   580 apply (erule exE)
   581 apply (case_tac xs) apply (case_tac xs')
   582 apply (auto intro: evals_type_sound [THEN conjunct1])
   583 done
   584 
   585 lemma state_ok_exec: "\<lbrakk>xs::\<preceq>E; wf_java_prog (prg E); wtpd_stmt E st;
   586   (xs,st,xs') \<in> Eval.exec (prg E)\<rbrakk> \<Longrightarrow>  xs'::\<preceq>E"
   587 apply (simp only: wtpd_stmt_def)
   588 apply (case_tac xs', case_tac xs)
   589 apply (auto dest: exec_type_sound)
   590 done
   591 
   592 
   593 lemma state_ok_init: 
   594   "\<lbrakk> wf_java_prog G; (x, h, l)::\<preceq>(env_of_jmb G C S); 
   595   is_class G dynT;
   596   method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
   597   list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
   598 \<Longrightarrow>
   599 (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs))"
   600 apply (frule wf_prog_ws_prog)
   601 apply (frule method_in_md [THEN conjunct2], assumption+)
   602 apply (frule method_yields_wf_java_mdecl, assumption, assumption)
   603 apply (simp add: env_of_jmb_def gs_def conforms_def split_beta)
   604 apply (simp add: wf_java_mdecl_def)
   605 apply (rule conjI)
   606 apply (rule lconf_ext)
   607 apply (rule lconf_ext_list)
   608 apply (rule lconf_init_vars)
   609 apply (auto dest: Ball_set_table)
   610 apply (simp add: np_def xconf_raise_if)
   611 done
   612 
   613 
   614 lemma ty_exprs_list_all2 [rule_format (no_asm)]: 
   615   "(\<forall> Ts. (E \<turnstile> es [::] Ts) = list_all2 (\<lambda>e T. E \<turnstile> e :: T) es Ts)"
   616 apply (rule list.induct)
   617 apply simp
   618 apply (rule allI)
   619 apply (rule iffI)
   620   apply (ind_cases "E \<turnstile> [] [::] Ts", assumption)
   621   apply simp apply (rule WellType.Nil)
   622 apply (simp add: list_all2_Cons1)
   623 apply (rule allI)
   624 apply (rule iffI)
   625   apply (rename_tac a exs Ts)
   626   apply (ind_cases "E \<turnstile> a # exs  [::] Ts") apply blast
   627   apply (auto intro: WellType.Cons)
   628 done
   629 
   630 
   631 lemma conf_bool: "G,h \<turnstile> v::\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v = Bool b"
   632 apply (simp add: conf_def)
   633 apply (erule exE)
   634 apply (case_tac v)
   635 apply (auto elim: widen.cases)
   636 done
   637 
   638 
   639 lemma class_expr_is_class: "\<lbrakk>E \<turnstile> e :: Class C; ws_prog (prg E)\<rbrakk> 
   640   \<Longrightarrow> is_class (prg E) C"
   641 by (case_tac E, auto dest: ty_expr_is_type)
   642 
   643 
   644 lemma max_spec_widen: "max_spec G C (mn, pTs) = {((md,rT),pTs')} \<Longrightarrow> 
   645   list_all2 (\<lambda> T T'. G \<turnstile> T \<preceq> T') pTs pTs'"
   646 by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD)
   647 
   648 
   649 lemma eval_conf: "\<lbrakk>G \<turnstile> s -e\<succ>v-> s'; wf_java_prog G; s::\<preceq>E;
   650   E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk> 
   651   \<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
   652 apply (simp add: gh_def)
   653 apply (rule_tac x3="fst s" and s3="snd s"and x'3="fst s'"  
   654   in eval_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]], simplified])
   655 apply assumption+
   656 apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
   657 apply (simp only: surjective_pairing [THEN sym])
   658 apply (auto simp add: gs_def gx_def)
   659 done
   660 
   661 lemma evals_preserves_conf:
   662   "\<lbrakk> G\<turnstile> s -es[\<succ>]vs-> s'; G,gh s \<turnstile> t ::\<preceq> T; E \<turnstile>es[::]Ts;
   663   wf_java_prog G; s::\<preceq>E; 
   664   prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T"
   665 apply (subgoal_tac "gh s\<le>| gh s'")
   666 apply (frule conf_hext, assumption, assumption)
   667 apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]]) 
   668 apply (subgoal_tac "G \<turnstile> (gx s, (gh s, gl s)) -es[\<succ>]vs-> (gx s', (gh s', gl s'))")
   669 apply assumption
   670 apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym])
   671 apply (case_tac E)
   672 apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym])
   673 done
   674 
   675 lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; 
   676   wf_java_prog G; s::\<preceq>E; gx s'=None; a' \<noteq> Null; G=prg E\<rbrakk>
   677   \<Longrightarrow> (\<exists> lc. a' = Addr lc)"
   678 apply (case_tac s, case_tac s', simp)
   679 apply (frule eval_type_sound, (simp add: gs_def)+)
   680 apply (case_tac a')
   681 apply (auto simp: conf_def)
   682 done
   683 
   684 
   685 lemma dynT_subcls: 
   686   "\<lbrakk> a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; dynT = fst (the (h (the_Addr a')));
   687   is_class G dynT; ws_prog G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
   688 apply (case_tac "C = Object")
   689 apply (simp, rule subcls_C_Object, assumption+)
   690 apply simp
   691 apply (frule non_np_objD, auto)
   692 done
   693 
   694 
   695 lemma method_defined: "\<lbrakk> 
   696   m = the (method (G, dynT) (mn, pTs)); 
   697   dynT = fst (the (h a)); is_class G dynT; wf_java_prog G; 
   698   a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; a = the_Addr a';
   699   \<exists>pTsa md rT. max_spec G C (mn, pTsa) = {((md, rT), pTs)} \<rbrakk>
   700 \<Longrightarrow> (method (G, dynT) (mn, pTs)) = Some m"
   701 apply (erule exE)+
   702 apply (drule singleton_in_set, drule max_spec2appl_meths)
   703 apply (simp add: appl_methds_def)
   704 apply ((erule exE)+, (erule conjE)+, (erule exE)+)
   705 apply (drule widen_methd)
   706 apply assumption
   707 apply (rule dynT_subcls) apply assumption+ apply simp apply simp
   708 apply (erule exE)+ apply simp
   709 done
   710 
   711 
   712 
   713 (**********************************************************************)
   714 
   715 
   716 (* 1. any difference between locvars_xstate \<dots> and L ??? *)
   717 (* 2. possibly skip env_of_jmb ??? *)
   718 theorem compiler_correctness: 
   719   "wf_java_prog G \<Longrightarrow>
   720   ((xs,ex,val,xs') \<in> Eval.eval G \<longrightarrow>
   721   gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
   722   (\<forall> os CL S.
   723   (class_sig_defined G CL S) \<longrightarrow> 
   724   (wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow>
   725   (xs ::\<preceq> (env_of_jmb G CL S)) \<longrightarrow>
   726   ( {TranslComp.comp G, CL, S} \<turnstile>
   727     {gh xs, os, (locvars_xstate G CL S xs)}
   728     >- (compExpr (gmb G CL S) ex) \<rightarrow>
   729     {gh xs', val#os, locvars_xstate G CL S xs'}))) \<and> 
   730 
   731  ((xs,exs,vals,xs') \<in> Eval.evals G \<longrightarrow>
   732   gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
   733   (\<forall> os CL S.
   734   (class_sig_defined G CL S) \<longrightarrow> 
   735   (wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow>
   736   (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
   737   ( {TranslComp.comp G, CL, S} \<turnstile>
   738     {gh xs, os, (locvars_xstate G CL S xs)}
   739     >- (compExprs (gmb G CL S) exs) \<rightarrow>
   740     {gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and> 
   741 
   742   ((xs,st,xs') \<in> Eval.exec G \<longrightarrow>
   743    gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
   744   (\<forall> os CL S.
   745   (class_sig_defined G CL S) \<longrightarrow> 
   746   (wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow>
   747   (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
   748   ( {TranslComp.comp G, CL, S} \<turnstile>
   749     {gh xs, os, (locvars_xstate G CL S xs)}
   750     >- (compStmt (gmb G CL S) st) \<rightarrow>
   751     {gh xs', os, (locvars_xstate G CL S xs')})))"
   752 apply (rule Eval.eval_evals_exec.induct)
   753 
   754 (* case XcptE *)
   755 apply simp
   756 
   757 (* case NewC *) 
   758 apply clarify 
   759 apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish  wf ((subcls1 G)^-1) *)
   760 apply (simp add: c_hupd_hp_invariant)
   761 apply (rule progression_one_step)
   762 apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *)
   763 apply (simp add: locvars_xstate_def locvars_locals_def comp_fields)
   764 
   765 
   766 (* case Cast *)
   767 apply (intro allI impI)
   768 apply simp
   769 apply (frule raise_if_NoneD)
   770 apply (frule wtpd_expr_cast)
   771 apply simp
   772 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
   773 apply blast
   774 apply (rule progression_one_step)
   775 apply (simp add: raise_system_xcpt_def  gh_def comp_cast_ok)
   776 
   777 
   778 (* case Lit *)
   779 apply simp
   780 apply (intro strip)
   781 apply (rule progression_one_step)
   782 apply simp
   783 
   784 
   785 (* case BinOp *)
   786 apply (intro allI impI)
   787 apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *)
   788 apply (frule wtpd_expr_binop)
   789 (* establish (s1::\<preceq> \<dots>) *)
   790 apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp)) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst) 
   791 
   792 
   793 apply (simp (no_asm_use) only: compExpr_compExprs.simps)
   794 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
   795 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
   796 apply (case_tac bop)
   797   (*subcase bop = Eq *)  apply simp apply (rule progression_Eq)
   798   (*subcase bop = Add *) apply simp apply (rule progression_one_step) apply simp
   799 
   800 
   801 (* case LAcc *)
   802 apply simp
   803 apply (intro strip)
   804 apply (rule progression_one_step)
   805 apply (simp add: locvars_xstate_def locvars_locals_def)
   806 apply (frule wtpd_expr_lacc)
   807 apply assumption
   808 apply (simp add: gl_def)
   809 apply (erule select_at_index)
   810 
   811 
   812 (* case LAss *)
   813 apply (intro allI impI)
   814 apply (frule wtpd_expr_lass, erule conjE, erule conjE)
   815 apply (simp add: compExpr_compExprs.simps)
   816 
   817 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   818 apply blast
   819 
   820 apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
   821 apply (rule progression_one_step)
   822 apply (simp add: gh_def)
   823 apply (rule conjI, simp)+ apply simp
   824 apply (rule progression_one_step)
   825 apply (simp add: gh_def)
   826 (* the following falls out of the general scheme *)
   827 apply (frule wtpd_expr_lacc) apply assumption
   828 apply (rule update_at_index)
   829 apply (rule distinct_method_if_class_sig_defined) apply assumption
   830 apply assumption apply simp apply assumption
   831 
   832 
   833 (* case FAcc *)
   834 apply (intro allI impI)
   835    (* establish x1 = None \<and> a' \<noteq> Null *)
   836 apply (simp (no_asm_use) only: gx_conv, frule np_NoneD)
   837 apply (frule wtpd_expr_facc)
   838 
   839 apply (simp (no_asm_use) only: compExpr_compExprs.simps)
   840 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   841 apply blast
   842 apply (rule progression_one_step)
   843 apply (simp add: gh_def)
   844 apply (case_tac "(the (fst s1 (the_Addr a')))")
   845 apply (simp add: raise_system_xcpt_def)
   846 
   847 
   848 (* case FAss *)
   849 apply (intro allI impI)
   850 apply (frule wtpd_expr_fass) apply (erule conjE) apply (frule wtpd_expr_facc)
   851 apply (simp only: c_hupd_xcpt_invariant) (* establish x2 = None *)
   852    (* establish x1 = None  and  a' \<noteq> Null  *)
   853 apply (frule_tac xs="(np a' x1, s1)" in eval_xcpt)
   854 apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE)
   855 
   856 
   857   (* establish ((Norm s1)::\<preceq> \<dots>) *)
   858 apply (frule_tac e=e1 in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) 
   859    apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst) 
   860 
   861 apply (simp only: compExpr_compExprs.simps)
   862 
   863 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
   864 apply fast (* blast does not seem to work - why? *)
   865 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
   866 apply fast
   867 apply (rule_tac ?instrs0.0 = "[Dup_x1]" and ?instrs1.0 = "[Putfield fn T]" in progression_transitive, simp)
   868 
   869    (* Dup_x1 *)
   870    apply (rule progression_one_step)
   871    apply (simp add: gh_def)
   872    apply (rule conjI, simp)+ apply simp
   873 
   874 
   875    (* Putfield \<longrightarrow> still looks nasty*)
   876    apply (rule progression_one_step)
   877    apply simp
   878    apply (case_tac "(the (fst s2 (the_Addr a')))")
   879    apply (simp add: c_hupd_hp_invariant)
   880    apply (case_tac s2)
   881    apply (simp add: c_hupd_conv raise_system_xcpt_def)
   882    apply (rule locvars_xstate_par_dep, rule HOL.refl)
   883 
   884 defer (* method call *)
   885 
   886 (* case XcptEs *)
   887 apply simp
   888 
   889 (* case Nil *)
   890 apply (simp add: compExpr_compExprs.simps)
   891 apply (intro strip)
   892 apply (rule progression_refl)
   893 
   894 (* case Cons *)
   895 apply (intro allI impI)
   896 apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
   897 apply (frule wtpd_exprs_cons)
   898    (* establish ((Norm s0)::\<preceq> \<dots>) *)
   899 apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
   900 
   901 apply simp
   902 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   903 apply fast
   904 apply fast
   905 
   906 
   907 (* case Statement: exception *)
   908 apply simp
   909 
   910 (* case Skip *)
   911 apply (intro allI impI)
   912 apply simp
   913 apply (rule progression_refl)
   914 
   915 (* case Expr *)
   916 apply (intro allI impI)
   917 apply (frule wtpd_stmt_expr)
   918 apply simp
   919 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
   920 apply fast
   921 apply (rule progression_one_step)
   922 apply simp
   923 
   924 (* case Comp *)
   925 apply (intro allI impI)
   926 apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
   927 apply (frule wtpd_stmt_comp)
   928 
   929   (* establish (s1::\<preceq> \<dots>) *)
   930 apply (frule_tac st=c1 in state_ok_exec) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
   931 
   932 apply simp
   933 apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
   934 apply fast
   935 apply fast
   936 
   937 
   938 (* case Cond *)
   939 apply (intro allI impI)
   940 apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
   941 apply (frule wtpd_stmt_cond, (erule conjE)+)
   942 (* establish (s1::\<preceq> \<dots>) *)
   943 apply (frule_tac e=e in state_ok_eval) 
   944 apply (simp (no_asm_simp) only: env_of_jmb_fst)
   945 apply assumption 
   946 apply (simp (no_asm_use) only: env_of_jmb_fst) 
   947 (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
   948 apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
   949 apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
   950 apply (erule exE)
   951 
   952 apply simp
   953 apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   954 apply (rule progression_one_step,  simp)
   955 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   956 
   957 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
   958 apply fast
   959 
   960 apply (case_tac b)
   961  (* case b= True *)
   962 apply simp
   963 apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
   964 apply (rule progression_one_step) apply simp
   965 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
   966 apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
   967 apply fast
   968 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
   969 apply (simp, rule conjI, (rule HOL.refl)+)
   970 apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
   971 apply (rule progression_refl)
   972 
   973  (* case b= False *)
   974 apply simp
   975 apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
   976 apply (simp, rule conjI, (rule HOL.refl)+)
   977 apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
   978 apply fast
   979 
   980 (* case exit Loop *)
   981 apply (intro allI impI)
   982 apply (frule wtpd_stmt_loop, (erule conjE)+)
   983 
   984 (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
   985 apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
   986 apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
   987 apply (erule exE)
   988 apply (case_tac b)
   989 
   990  (* case b= True \<longrightarrow> contradiction *)
   991 apply simp
   992 
   993  (* case b= False *)
   994 apply simp
   995 
   996 apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
   997 apply (rule progression_one_step)
   998    apply simp 
   999    apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
  1000 
  1001 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
  1002 apply fast
  1003 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
  1004 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
  1005 apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
  1006 apply (rule progression_refl)
  1007 
  1008 
  1009 (* case continue Loop *)
  1010 apply (intro allI impI)
  1011 apply (frule_tac xs=s2 in exec_xcpt, assumption) (* establish (gx s2 = None) *)
  1012 apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
  1013 apply (frule wtpd_stmt_loop, (erule conjE)+)
  1014 
  1015 (* establish (s1::\<preceq> \<dots>) *)
  1016 apply (frule_tac e=e in state_ok_eval) apply (simp (no_asm_simp) only: env_of_jmb_fst) apply simp apply (simp (no_asm_use) only: env_of_jmb_fst)
  1017 (* establish (s2::\<preceq> \<dots>) *)
  1018 apply (frule_tac xs=s1 and st=c in state_ok_exec)
  1019 apply (simp (no_asm_simp) only: env_of_jmb_fst) apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
  1020 
  1021 (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
  1022 apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
  1023 apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
  1024 apply (erule exE)
  1025 
  1026 apply simp
  1027 apply (rule jump_bwd_progression) 
  1028 apply simp
  1029 apply (rule conjI, (rule HOL.refl)+)
  1030 
  1031 apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
  1032 apply (rule progression_one_step)
  1033    apply simp 
  1034    apply (rule conjI, simp)+ apply simp
  1035 
  1036 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
  1037 apply fast
  1038 
  1039 apply (case_tac b)
  1040  (* case b= True *)
  1041 apply simp
  1042 
  1043 apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
  1044 apply (rule progression_one_step) apply simp
  1045 apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
  1046 apply fast
  1047 
  1048  (* case b= False \<longrightarrow> contradiction*)
  1049 apply simp
  1050 
  1051 apply (rule jump_bwd_one_step)
  1052 apply simp
  1053 apply blast
  1054 
  1055 (*****)
  1056 (* case method call *)
  1057 
  1058 apply (intro allI impI)
  1059 
  1060 apply (frule_tac xs=s3 in eval_xcpt, simp only: gx_conv) (* establish gx s3 = None *)
  1061 apply (frule exec_xcpt, assumption, simp (no_asm_use) only: gx_conv, frule np_NoneD) (* establish x = None \<and> a' \<noteq> Null *)
  1062 apply (frule evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
  1063 
  1064 apply (frule wtpd_expr_call, (erule conjE)+)
  1065 
  1066 
  1067 (* assumptions about state_ok and is_class *)
  1068 
  1069 (* establish s1::\<preceq> (env_of_jmb G CL S) *)
  1070 apply (frule_tac xs="Norm s0" and e=e in state_ok_eval)
  1071 apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst)
  1072 
  1073 (* establish (x, h, l)::\<preceq>(env_of_jmb G CL S) *)
  1074 apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals)
  1075 apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)
  1076 
  1077 (* establish \<exists> lc. a' = Addr lc *)
  1078 apply (frule (5) eval_of_class, rule env_of_jmb_fst [THEN sym])
  1079 apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class C")
  1080 apply (subgoal_tac "is_class G dynT")
  1081 
  1082 (* establish method (G, dynT) (mn, pTs) = Some(md, rT, pns, lvars, blk, res) *)
  1083 apply (drule method_defined, assumption+)
  1084 apply (simp only: env_of_jmb_fst)
  1085 apply ((erule exE)+, erule conjE, (rule exI)+, assumption) 
  1086 
  1087 apply (subgoal_tac "is_class G md")
  1088 apply (subgoal_tac "G\<turnstile>Class dynT \<preceq> Class md")
  1089 apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)")
  1090 apply (subgoal_tac "list_all2 (conf G h) pvs pTs")
  1091 
  1092 (* establish (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs)) *)
  1093 apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class dynT")
  1094 apply (frule (2) conf_widen)
  1095 apply (frule state_ok_init, assumption+)
  1096 
  1097 apply (subgoal_tac "class_sig_defined G md (mn, pTs)")
  1098 apply (frule wtpd_blk, assumption, assumption)
  1099 apply (frule wtpd_res, assumption, assumption)
  1100 apply (subgoal_tac "s3::\<preceq>(env_of_jmb G md (mn, pTs))")
  1101 
  1102 apply (subgoal_tac "method (TranslComp.comp G, md) (mn, pTs) =
  1103           Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
  1104 prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
  1105 apply (subgoal_tac "method (TranslComp.comp G, dynT) (mn, pTs) =
  1106           Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
  1107 prefer 2 apply (simp add: wf_prog_ws_prog [THEN comp_method])
  1108  apply (simp only: fst_conv snd_conv)
  1109 
  1110 (* establish length pns = length pTs *)
  1111 apply (frule method_preserves_length, assumption, assumption) 
  1112 (* establish length pvs = length ps *)
  1113 apply (frule evals_preserves_length [THEN sym])
  1114 
  1115 (** start evaluating subexpressions **)
  1116 apply (simp (no_asm_use) only: compExpr_compExprs.simps)
  1117 
  1118   (* evaluate e *)
  1119 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
  1120 apply fast
  1121 
  1122   (* evaluate parameters *)
  1123 apply (rule_tac ?instrs0.0 = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
  1124 apply fast
  1125 
  1126   (* invokation *)
  1127 apply (rule progression_call)
  1128 apply (intro allI impI conjI)
  1129      (* execute Invoke statement *)
  1130 apply (simp (no_asm_use) only: exec_instr.simps)
  1131 apply (erule thin_rl, erule thin_rl, erule thin_rl)
  1132 apply (simp add: compMethod_def raise_system_xcpt_def)
  1133 apply (rule conjI, simp)+ apply (rule HOL.refl)
  1134 
  1135      (* get instructions of invoked method *)
  1136 apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
  1137 
  1138        (* var. initialization *)
  1139 apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
  1140 apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
  1141 apply (simp (no_asm_simp)) (* length pns = length pvs *)
  1142 apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
  1143 
  1144 
  1145        (* body statement *)
  1146 apply (rule_tac ?instrs0.0 = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
  1147 apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
  1148 apply (simp (no_asm_simp))
  1149 apply (simp only: gh_conv)
  1150 apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption)
  1151 apply (simp (no_asm_use))
  1152 apply (simp (no_asm_simp) add: gmb_def)
  1153 
  1154        (* return expression *) 
  1155 apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
  1156 apply (simp (no_asm_simp))
  1157 apply (simp only: gh_conv)
  1158 apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption)
  1159 apply (simp (no_asm_use))
  1160 apply (simp (no_asm_simp) add: gmb_def)
  1161 
  1162       (* execute return statement *)
  1163 apply (simp (no_asm_use) add: gh_def locvars_xstate_def gl_def del: drop_append)
  1164 apply (subgoal_tac "rev pvs @ a' # os = (rev (a' # pvs)) @ os")
  1165 apply (simp only: drop_append)
  1166 apply (simp (no_asm_simp))
  1167 apply (simp (no_asm_simp))
  1168 
  1169 (* show s3::\<preceq>\<dots> *)
  1170 apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))" and st=blk in state_ok_exec)
  1171 apply assumption apply (simp (no_asm_simp) only: env_of_jmb_fst) 
  1172 apply assumption apply (simp (no_asm_use) only: env_of_jmb_fst)
  1173 
  1174 (* show class_sig_defined G md (mn, pTs) *)
  1175 apply (simp (no_asm_simp) add: class_sig_defined_def)
  1176 
  1177 (* show G,h \<turnstile> a' ::\<preceq> Class dynT *)
  1178 apply (frule non_npD) apply assumption
  1179 apply (erule exE)+ apply simp
  1180 apply (rule conf_obj_AddrI) apply simp 
  1181 apply (rule conjI, (rule HOL.refl)+)
  1182 apply (rule widen_Class_Class [THEN iffD1], rule widen.refl)
  1183 
  1184 
  1185   (* show list_all2 (conf G h) pvs pTs *)
  1186 apply (erule exE)+ apply (erule conjE)+
  1187 apply (rule_tac Ts="pTsa" in conf_list_gext_widen) apply assumption
  1188 apply (subgoal_tac "((gx s1, gs s1), ps, pvs, x, h, l) \<in> evals G")
  1189 apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
  1190 apply assumption+
  1191 apply (simp only: env_of_jmb_fst) 
  1192 apply (simp add: conforms_def xconf_def gs_def)
  1193 apply simp
  1194 apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
  1195 apply (simp (no_asm_use) only: ty_exprs_list_all2) apply simp
  1196 apply simp
  1197 apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
  1198     (* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *)
  1199     apply (rule max_spec_widen, simp only: env_of_jmb_fst)
  1200 
  1201 
  1202 (* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *)
  1203 apply (frule wf_prog_ws_prog [THEN method_in_md [THEN conjunct2]], assumption+)
  1204 
  1205   (* show G\<turnstile>Class dynT \<preceq> Class md *)
  1206 apply (simp (no_asm_use) only: widen_Class_Class)
  1207 apply (rule method_wf_mdecl [THEN conjunct1], assumption+)
  1208 
  1209   (* is_class G md *)
  1210 apply (rule wf_prog_ws_prog [THEN method_in_md [THEN conjunct1]], assumption+)
  1211 
  1212   (* show is_class G dynT *)
  1213 apply (frule non_npD) apply assumption
  1214 apply (erule exE)+ apply (erule conjE)+
  1215 apply simp
  1216 apply (rule subcls_is_class2) apply assumption
  1217 apply (frule class_expr_is_class) apply (simp only: env_of_jmb_fst)
  1218 apply (rule wf_prog_ws_prog, assumption)
  1219 apply (simp only: env_of_jmb_fst)
  1220 
  1221  (* show G,h \<turnstile> a' ::\<preceq> Class C *)
  1222 apply (simp only: wtpd_exprs_def, erule exE)
  1223 apply (frule evals_preserves_conf)
  1224 apply (rule eval_conf, assumption+)
  1225 apply (rule env_of_jmb_fst, assumption+)
  1226 apply (rule env_of_jmb_fst)
  1227 apply (simp only: gh_conv)
  1228 done
  1229 
  1230 
  1231 theorem compiler_correctness_eval: "
  1232   \<lbrakk> G \<turnstile> (None,hp,loc) -ex \<succ> val-> (None,hp',loc');
  1233   wf_java_prog G;
  1234   class_sig_defined G C S;
  1235   wtpd_expr (env_of_jmb G C S) ex;
  1236   (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
  1237   {(TranslComp.comp G), C, S} \<turnstile> 
  1238     {hp, os, (locvars_locals G C S loc)}
  1239       >- (compExpr (gmb G C S) ex) \<rightarrow> 
  1240     {hp', val#os, (locvars_locals G C S loc')}"
  1241 apply (frule compiler_correctness [THEN conjunct1])
  1242 apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
  1243 done
  1244 
  1245 theorem compiler_correctness_exec: "
  1246   \<lbrakk> ((None,hp,loc), st, (None,hp',loc')) \<in> Eval.exec G;
  1247   wf_java_prog G;
  1248   class_sig_defined G C S;
  1249   wtpd_stmt (env_of_jmb G C S) st;
  1250   (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
  1251   {(TranslComp.comp G), C, S} \<turnstile> 
  1252     {hp, os, (locvars_locals G C S loc)}
  1253       >- (compStmt (gmb G C S) st) \<rightarrow>
  1254     {hp', os, (locvars_locals G C S loc')}"
  1255 apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]])
  1256 apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
  1257 done
  1258 
  1259 (**********************************************************************)
  1260 
  1261 
  1262 (* reinstall pair splits *)
  1263 declare split_paired_All [simp] split_paired_Ex [simp]
  1264 ML_setup {*
  1265 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
  1266 *}
  1267 
  1268 declare wf_prog_ws_prog [simp del]
  1269 
  1270 end