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