Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: CorrComp.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/Comp/CorrComp.thy
    Author:     Martin Strecker
*)

(* Compiler correctness statement and proof *)

theory CorrComp
imports "../J/JTypeSafe" LemmasComp
begin

declare wf_prog_ws_prog [simp add]

(* If no exception is present after evaluation/execution,
  none can have been present before *)
lemma eval_evals_exec_xcpt:
"(G \ xs -ex\val-> xs' \ gx xs' = None \ gx xs = None) \
  (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
  (G \<turnstile> xs -st-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
  by (induct rule: eval_evals_exec.induct) auto

(* instance of eval_evals_exec_xcpt for eval *)
lemma eval_xcpt: "G \ xs -ex\val-> xs' \ gx xs' = None \ gx xs = None"
(is "?H1 \ ?H2 \ ?T")
proof-
  assume h1: ?H1
  assume h2: ?H2
  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
qed

(* instance of eval_evals_exec_xcpt for evals *)
lemma evals_xcpt: "G \ xs -exs[\]vals-> xs' \ gx xs' = None \ gx xs = None"
(is "?H1 \ ?H2 \ ?T")
proof-
  assume h1: ?H1
  assume h2: ?H2
  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
qed

(* instance of eval_evals_exec_xcpt for exec *)
lemma exec_xcpt: "G \ xs -st-> xs' \ gx xs' = None \ gx xs = None"
(is "?H1 \ ?H2 \ ?T")
proof-
  assume h1: ?H1
  assume h2: ?H2
  from h1 h2 eval_evals_exec_xcpt show "?T" by simp
qed

(**********************************************************************)

theorem exec_all_trans: "\(exec_all G s0 s1); (exec_all G s1 s2)\ \ (exec_all G s0 s2)"
by (auto simp: exec_all_def elim: Transitive_Closure.rtrancl_trans)

theorem exec_all_refl: "exec_all G s s"
by (simp only: exec_all_def)

theorem exec_instr_in_exec_all:
  "\ exec_instr i G hp stk lvars C S pc frs = (None, hp', frs');
             gis (gmb G C S) ! pc = i\<rbrakk>  \<Longrightarrow>
       G \<turnstile> (None, hp, (stk, lvars, C, S, pc) # frs) \<midarrow>jvm\<rightarrow> (None, hp', frs')"
  apply (simp only: exec_all_def)
  apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
  apply (simp add: gis_def gmb_def)
  apply (case_tac frs', simp+)
  done

theorem exec_all_one_step: "
  \<lbrakk> gis (gmb G C S) = pre @ (i # post); pc0 = length pre;
  (exec_instr i G hp0 stk0 lvars0 C S pc0 frs) =
  (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs) \<rbrakk>
  \<Longrightarrow>
  G \<turnstile> (None, hp0, (stk0,lvars0,C,S, pc0)#frs) \<midarrow>jvm\<rightarrow>
  (None, hp1, (stk1,lvars1,C,S, Suc pc0)#frs)"
  apply (unfold exec_all_def)
  apply (rule r_into_rtrancl)
  apply (simp add: gis_def gmb_def split_beta)
  done

(***********************************************************************)

definition progression :: "jvm_prog \ cname \ sig \
                 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow>
                 bytecode \<Rightarrow>
                 aheap \<Rightarrow> opstack \<Rightarrow> locvars \<Rightarrow>
                 bool"
  ("{_,_,_} \ {_, _, _} >- _ \ {_, _, _}" [61,61,61,61,61,61,90,61,61,61]60) where
  "{G,C,S} \ {hp0, os0, lvars0} >- instrs \ {hp1, os1, lvars1} ==
  \<forall>pre post frs.
  (gis (gmb G C S) = pre @ instrs @ post) \<longrightarrow>
   G \<turnstile> (None,hp0,(os0,lvars0,C,S,length pre)#frs) \<midarrow>jvm\<rightarrow>
       (None,hp1,(os1,lvars1,C,S,(length pre) + (length instrs))#frs)"

lemma progression_call:
  "\ \pc frs.
  exec_instr instr G hp0 os0 lvars0 C S pc frs =
      (None, hp', (os', lvars', C', S', 0) # (fr pc) # frs) \
  gis (gmb G C' S') = instrs' @ [Return] \
  {G, C', S'} \<turnstile> {hp', os', lvars'} >- instrs' \<rightarrow> {hp'', os'', lvars''}  \<and>
  exec_instr Return G hp'' os'' lvars'' C' S' (length instrs')
                                               ((fr pc) # frs) =
      (None, hp2, (os2, lvars2, C, S, Suc pc) # frs) \<rbrakk> \<Longrightarrow>
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >-[instr]\<rightarrow> {hp2,os2,lvars2}"
  apply (simp only: progression_def)
  apply (intro strip)
  apply (drule_tac x="length pre" in spec)
  apply (drule_tac x="frs" in spec)
  apply clarify
  apply (rule exec_all_trans)
   apply (rule exec_instr_in_exec_all)
    apply simp
   apply simp
  apply (rule exec_all_trans)
   apply (simp only: append_Nil)
   apply (drule_tac x="[]" in spec)
   apply (simp only: list.simps list.size)
   apply blast
  apply (rule exec_instr_in_exec_all)
   apply auto
  done

lemma progression_transitive:
  "\ instrs_comb = instrs0 @ instrs1;
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs0 \<rightarrow> {hp1, os1, lvars1};
  {G, C, S} \<turnstile> {hp1, os1, lvars1} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk>
  \<Longrightarrow>
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
  apply (simp only: progression_def)
  apply (intro strip)
  apply (rule_tac ?s1.0 = "Norm (hp1, (os1, lvars1, C, S,
                           length pre + length instrs0) # frs)"
               in exec_all_trans)
   apply (simp only: append_assoc)
  apply (erule thin_rl, erule thin_rl)
  apply (drule_tac x="pre @ instrs0" in spec)
  apply (simp add: add.assoc)
  done

lemma progression_refl:
  "{G, C, S} \ {hp0, os0, lvars0} >- [] \ {hp0, os0, lvars0}"
  apply (simp add: progression_def)
  apply (intro strip)
  apply (rule exec_all_refl)
  done

lemma progression_one_step: "
  \<forall>pc frs.
  (exec_instr i G hp0 os0 lvars0 C S pc frs) =
  (None, hp1, (os1,lvars1,C,S, Suc pc)#frs)
  \<Longrightarrow> {G, C, S} \<turnstile> {hp0, os0, lvars0} >- [i] \<rightarrow> {hp1, os1, lvars1}"
  apply (unfold progression_def)
  apply (intro strip)
  apply simp
  apply (rule exec_all_one_step)
    apply auto
  done

(*****)
definition jump_fwd :: "jvm_prog \ cname \ sig \
                 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow>
                 instr \<Rightarrow> bytecode \<Rightarrow> bool" where
  "jump_fwd G C S hp lvars os0 os1 instr instrs ==
  \<forall>pre post frs.
  (gis (gmb G C S) = pre @ instr # instrs @ post) \<longrightarrow>
   exec_all G (None,hp,(os0,lvars,C,S, length pre)#frs)
    (None,hp,(os1,lvars,C,S,(length pre) + (length instrs) + 1)#frs)"

lemma jump_fwd_one_step:
  "\pc frs.
  exec_instr instr G hp os0 lvars C S pc frs =
    (None, hp, (os1, lvars, C, S, pc + (length instrs) + 1)#frs)
  \<Longrightarrow> jump_fwd G C S hp lvars os0 os1 instr instrs"
  apply (unfold jump_fwd_def)
  apply (intro strip)
  apply (rule exec_instr_in_exec_all)
   apply auto
  done

lemma jump_fwd_progression_aux:
  "\ instrs_comb = instr # instrs0 @ instrs1;
     jump_fwd G C S hp lvars os0 os1 instr instrs0;
     {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk>
  \<Longrightarrow> {G, C, S} \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
  apply (simp only: progression_def jump_fwd_def)
  apply (intro strip)
  apply (rule_tac ?s1.0 = "Norm(hp, (os1, lvars, C, S, length pre + length instrs0 + 1) # frs)" in exec_all_trans)
   apply (simp only: append_assoc)
   apply (subgoal_tac "pre @ (instr # instrs0 @ instrs1) @ post = pre @ instr # instrs0 @ (instrs1 @ post)")
    apply blast
   apply simp
  apply (erule thin_rl, erule thin_rl)
  apply (drule_tac x="pre @ instr # instrs0" in spec)
  apply (simp add: add.assoc)
  done

lemma jump_fwd_progression:
  "\ instrs_comb = instr # instrs0 @ instrs1;
  \<forall> pc frs.
  exec_instr instr G hp os0 lvars C S pc frs =
    (None, hp, (os1, lvars, C, S, pc + (length instrs0) + 1)#frs);
  {G, C, S} \<turnstile> {hp, os1, lvars} >- instrs1 \<rightarrow> {hp2, os2, lvars2} \<rbrakk>
  \<Longrightarrow> {G, C, S}  \<turnstile> {hp, os0, lvars} >- instrs_comb \<rightarrow> {hp2, os2, lvars2}"
  apply (rule jump_fwd_progression_aux)
    apply assumption
   apply (rule jump_fwd_one_step, assumption+)
  done

(* note: instrs and instr reversed wrt. jump_fwd *)
definition jump_bwd :: "jvm_prog \ cname \ sig \
                 aheap \<Rightarrow> locvars \<Rightarrow> opstack \<Rightarrow> opstack \<Rightarrow>
                 bytecode \<Rightarrow> instr \<Rightarrow> bool" where
  "jump_bwd G C S hp lvars os0 os1 instrs instr ==
  \<forall> pre post frs.
  (gis (gmb G C S) = pre @ instrs @ instr # post) \<longrightarrow>
   exec_all G (None,hp,(os0,lvars,C,S, (length pre) + (length instrs))#frs)
    (None,hp,(os1,lvars,C,S, (length pre))#frs)"

lemma jump_bwd_one_step:
  "\ pc frs.
  exec_instr instr G hp os0 lvars C S (pc + (length instrs)) frs =
    (None, hp, (os1, lvars, C, S, pc)#frs)
  \<Longrightarrow>
  jump_bwd G C S hp lvars os0 os1 instrs instr"
  apply (unfold jump_bwd_def)
  apply (intro strip)
  apply (rule exec_instr_in_exec_all)
   apply auto
  done

lemma jump_bwd_progression:
  "\ instrs_comb = instrs @ [instr];
  {G, C, S} \<turnstile> {hp0, os0, lvars0} >- instrs \<rightarrow> {hp1, os1, lvars1};
  jump_bwd G C S hp1 lvars1 os1 os2 instrs instr;
  {G, C, S} \<turnstile> {hp1, os2, lvars1} >- instrs_comb \<rightarrow> {hp3, os3, lvars3} \<rbrakk>
  \<Longrightarrow> {G, C, S}  \<turnstile> {hp0, os0, lvars0} >- instrs_comb \<rightarrow> {hp3, os3, lvars3}"
  apply (simp only: progression_def jump_bwd_def)
  apply (intro strip)
  apply (rule exec_all_trans, force)
  apply (rule exec_all_trans, force)
  apply (rule exec_all_trans, force)
  apply simp
  apply (rule exec_all_refl)
  done

(**********************************************************************)

(* class C with signature S is defined in program G *)
definition class_sig_defined :: "'c prog \ cname \ sig \ bool" where
  "class_sig_defined G C S ==
  is_class G C \<and> (\<exists> D rT mb. (method (G, C) S = Some (D, rT, mb)))"

(* The environment of a java method body
  (characterized by class and signature) *)
definition env_of_jmb :: "java_mb prog \ cname \ sig \ java_mb env" where
  "env_of_jmb G C S ==
  (let (mn,pTs) = S;
       (D,rT,(pns,lvars,blk,res)) = the(method (G, C) S) in
  (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)))"

lemma env_of_jmb_fst [simp]: "fst (env_of_jmb G C S) = G"
by (simp add: env_of_jmb_def split_beta)

(**********************************************************************)

lemma method_preserves [rule_format (no_asm)]:
  "\ wf_prog wf_mb G; is_class G C;
  \<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>
\<Longrightarrow> \<forall> D.
  method (G, C) S = Some (D, rT, mb) \<longrightarrow> (P D S (rT,mb))"

  apply (frule wf_prog_ws_prog [THEN wf_subcls1])
  apply (rule subcls1_induct, assumption, assumption)

   apply (intro strip)
   apply ((drule spec)+, drule_tac x="Object" in bspec)
    apply (simp add: wf_prog_def ws_prog_def wf_syscls_def)
   apply (subgoal_tac "D=Object") apply simp
    apply (drule mp)
     apply (frule_tac C=Object in method_wf_mdecl)
       apply simp
      apply assumption
     apply simp
    apply assumption
   apply simp

  apply (simplesubst method_rec)
    apply simp
   apply force
  apply simp
  apply (simp only: map_add_def)
  apply (split option.split)
  apply (rule conjI)
   apply force
  apply (intro strip)
  apply (frule_tac ?P1.0 = "wf_mdecl wf_mb G Ca" and
                   ?P2.0 = "%(S, (Da, rT, mb)). P Da S (rT, mb)" in map_of_map_prop)
    apply (force simp: wf_cdecl_def)

   apply clarify

   apply (simp only: class_def)
   apply (drule map_of_SomeD)+
   apply (frule_tac A="set G" and f=fst in imageI, simp)
   apply blast
  apply simp
  done

lemma method_preserves_length:
  "\ wf_java_prog G; is_class G C;
  method (G, C) (mn,pTs) = Some (D, rT, pns, lvars, blk, res)\<rbrakk>
\<Longrightarrow> length pns = length pTs"
  apply (frule_tac P="%D (mn,pTs) (rT, pns, lvars, blk, res). length pns = length pTs"
                   in method_preserves)
  apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
  done

(**********************************************************************)

definition wtpd_expr :: "java_mb env \ expr \ bool" where
  "wtpd_expr E e == (\ T. E\e :: T)"

definition wtpd_exprs :: "java_mb env \ (expr list) \ bool" where
  "wtpd_exprs E e == (\ T. E\e [::] T)"

definition wtpd_stmt :: "java_mb env \ stmt \ bool" where
  "wtpd_stmt E c == (E\c \)"

lemma wtpd_expr_newc: "wtpd_expr E (NewC C) \ is_class (prg E) C"
  by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)

lemma wtpd_expr_cast: "wtpd_expr E (Cast cn e) \ (wtpd_expr E e)"
  by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)

lemma wtpd_expr_lacc:
  "\ wtpd_expr (env_of_jmb G C S) (LAcc vn); class_sig_defined G C S \
  \<Longrightarrow> vn \<in> set (gjmb_plns (gmb G C S)) \<or> vn = This"
  apply (clarsimp simp: wtpd_expr_def env_of_jmb_def class_sig_defined_def galldefs)
  apply (case_tac S)
  apply (erule ty_expr.cases; fastforce dest: map_upds_SomeD map_of_SomeD fst_in_set_lemma)
  done

lemma wtpd_expr_lass: "wtpd_expr E (vn::=e)
  \<Longrightarrow> (vn \<noteq> This) & (wtpd_expr E (LAcc vn)) & (wtpd_expr E e)"
  by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)

lemma wtpd_expr_facc: "wtpd_expr E ({fd}a..fn)
  \<Longrightarrow> (wtpd_expr E a)"
  by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)

lemma wtpd_expr_fass: "wtpd_expr E ({fd}a..fn:=v)
  \<Longrightarrow> (wtpd_expr E ({fd}a..fn)) & (wtpd_expr E v)"
  by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)

lemma wtpd_expr_binop: "wtpd_expr E (BinOp bop e1 e2)
  \<Longrightarrow> (wtpd_expr E e1) & (wtpd_expr E e2)"
  by (simp only: wtpd_expr_def, erule exE, erule ty_expr.cases, auto)

lemma wtpd_exprs_cons: "wtpd_exprs E (e # es)
  \<Longrightarrow> (wtpd_expr E e) & (wtpd_exprs E es)"
  by (simp only: wtpd_exprs_def wtpd_expr_def, erule exE, erule ty_exprs.cases, auto)

lemma wtpd_stmt_expr: "wtpd_stmt E (Expr e) \ (wtpd_expr E e)"
  by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)

lemma wtpd_stmt_comp: "wtpd_stmt E (s1;; s2) \
   (wtpd_stmt E s1) &  (wtpd_stmt E s2)"
   by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)

lemma wtpd_stmt_cond: "wtpd_stmt E (If(e) s1 Else s2) \
   (wtpd_expr E e) & (wtpd_stmt E s1) &  (wtpd_stmt E s2)
  & (E\<turnstile>e::PrimT Boolean)"
  by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)

lemma wtpd_stmt_loop: "wtpd_stmt E (While(e) s) \
   (wtpd_expr E e) & (wtpd_stmt E s) & (E\<turnstile>e::PrimT Boolean)"
   by (simp only: wtpd_stmt_def wtpd_expr_def, erule wt_stmt.cases, auto)

lemma wtpd_expr_call: "wtpd_expr E ({C}a..mn({pTs'}ps))
  \<Longrightarrow> (wtpd_expr E a) & (wtpd_exprs E ps)
  & (length ps = length pTs') & (E\a::Class C)
  & (\<exists> pTs md rT.
       E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
  apply (simp only: wtpd_expr_def wtpd_exprs_def)
  apply (erule exE)
  apply (ind_cases "E \ {C}a..mn( {pTs'}ps) :: T" for T)
  apply (auto simp: max_spec_preserves_length)
  done

lemma wtpd_blk:
  "\ method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res));
  wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
\<Longrightarrow> wtpd_stmt (env_of_jmb G D (md, pTs)) blk"
  apply (simp add: wtpd_stmt_def env_of_jmb_def)
  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). (G, map_of lvars(pns[\]pTs)(This\Class D)) \ blk \ " in method_preserves)
     apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
  done

lemma wtpd_res:
  "\ method (G, D) (md, pTs) = Some (D, rT, (pns, lvars, blk, res));
  wf_prog wf_java_mdecl G; is_class G D \<rbrakk>
\<Longrightarrow> wtpd_expr (env_of_jmb G D (md, pTs)) res"
  apply (simp add: wtpd_expr_def env_of_jmb_def)
  apply (frule_tac P="%D (md, pTs) (rT, (pns, lvars, blk, res)). \T. (G, map_of lvars(pns[\]pTs)(This\Class D)) \ res :: T " in method_preserves)
     apply (auto simp: wf_mdecl_def wf_java_mdecl_def)
  done

(**********************************************************************)

(* Is there a more elegant proof? *)
lemma evals_preserves_length:
  "G\ xs -es[\]vs-> (None, s) \ length es = length vs"
  apply (subgoal_tac
    "\ xs'. (G \ xk -xj\xi-> xh \ True) &
    (G\<turnstile> xs -es[\<succ>]vs-> xs' \<longrightarrow>  (\<exists> s. (xs' = (None, s))) \<longrightarrow>
    length es = length vs) &
    (G \<turnstile> xc -xb-> xa \<longrightarrow> True)")
   apply blast
  apply (rule allI)
  apply (rule Eval.eval_evals_exec.induct; simp)
  done

(***********************************************************************)

(* required for translation of BinOp *)

lemma progression_Eq : "{G, C, S} \
  {hp, (v2 # v1 # os), lvars}
  >- [Ifcmpeq 3, LitPush (Bool False), Goto 2, LitPush (Bool True)] \<rightarrow>
  {hp, (Bool (v1 = v2) # os), lvars}"
  apply (case_tac "v1 = v2")

   (* case v1 = v2 *)
   apply (rule_tac ?instrs1.0 = "[LitPush (Bool True)]" in jump_fwd_progression)
     apply (auto simp: nat_add_distrib)
   apply (rule progression_one_step)
   apply simp

  (* case v1 \<noteq> v2 *)
  apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified])
   apply auto
  apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified])
   apply auto
  apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
    apply (auto simp: nat_add_distrib intro: progression_refl)
  done

(**********************************************************************)

(* to avoid automatic pair splits *)

declare split_paired_All [simp del] split_paired_Ex [simp del]

lemma distinct_method:
  "\ wf_java_prog G; is_class G C; method (G, C) S = Some (D, rT, pns, lvars, blk, res) \ \
  distinct (gjmb_plns (gmb G C S))"
  apply (frule method_wf_mdecl [THEN conjunct2],  assumption, assumption)
  apply (case_tac S)
  apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs)
  apply (simp add: unique_def map_of_in_set)
  apply blast
  done

lemma distinct_method_if_class_sig_defined :
  "\ wf_java_prog G; class_sig_defined G C S \ \ distinct (gjmb_plns (gmb G C S))"
  by (auto intro: distinct_method simp: class_sig_defined_def)

lemma method_yields_wf_java_mdecl: "\ wf_java_prog G; is_class G C;
  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk>  \<Longrightarrow>
  wf_java_mdecl G D (S,rT,(pns,lvars,blk,res))"
  apply (frule method_wf_mdecl)
    apply (auto simp: wf_mdecl_def)
  done

(**********************************************************************)

lemma progression_lvar_init_aux [rule_format (no_asm)]: "
  \<forall> zs prfx lvals lvars0.
  lvars0 =  (zs @ lvars) \<longrightarrow>
  (disjoint_varnames pns lvars0 \<longrightarrow>
  (length lvars = length lvals) \<longrightarrow>
  (Suc(length pns + length zs) = length prfx) \<longrightarrow>
   ({cG, D, S} \<turnstile>
    {h, os, (prfx @ lvals)}
    >- (concat (map (compInit (pns, lvars0, blk, res)) lvars)) \<rightarrow>
    {h, os, (prfx @ (map (\<lambda>p. (default_val (snd p))) lvars))}))"
  apply simp
  apply (induct lvars)
   apply (clarsimp, rule progression_refl)
  apply (intro strip)
  apply (case_tac lvals)
   apply simp
  apply (simp (no_asm_simp) )

  apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ list" in progression_transitive, rule HOL.refl)
   apply (case_tac a)
   apply (simp (no_asm_simp) add: compInit_def)
   apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
    apply (rule progression_one_step)
    apply (simp (no_asm_simp) add: load_default_val_def)

   apply (rule progression_one_step)
   apply (simp (no_asm_simp))
   apply (rule conjI, simp)+
   apply (simp add: index_of_var2)
  apply (drule_tac x="zs @ [a]" in spec) (* instantiate zs *)
  apply (drule mp, simp)
  apply (drule_tac x="(prfx @ [default_val (snd a)])" in spec) (* instantiate prfx *)
  apply auto
  done

lemma progression_lvar_init [rule_format (no_asm)]:
  "\ wf_java_prog G; is_class G C;
  method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow>
  length pns = length pvs \<longrightarrow>
  (\<forall> lvals.
  length lvars = length lvals \<longrightarrow>
   {cG, D, S} \<turnstile>
   {h, os, (a' # pvs @ lvals)}
   >- (compInitLvars (pns, lvars, blk, res) lvars) \<rightarrow>
   {h, os, (locvars_xstate G C S (Norm (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))))})"
  apply (simp only: compInitLvars_def)
  apply (frule method_yields_wf_java_mdecl, assumption, assumption)

  apply (simp only: wf_java_mdecl_def)
  apply (subgoal_tac "(\y\set pns. y \ set (map fst lvars))")
   apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map)
   apply (intro strip)
   apply (simp (no_asm_simp) only: append_Cons [symmetric])
   apply (rule progression_lvar_init_aux)
      apply (auto simp: unique_def map_of_in_set disjoint_varnames_def)
  done

(**********************************************************************)

lemma state_ok_eval:
  "\xs::\E; wf_java_prog (prg E); wtpd_expr E e; (prg E)\xs -e\v -> xs'\ \ xs'::\E"
  apply (simp only: wtpd_expr_def)
  apply (erule exE)
  apply (case_tac xs', case_tac xs)
  apply (auto intro: eval_type_sound [THEN conjunct1])
  done

lemma state_ok_evals:
  "\xs::\E; wf_java_prog (prg E); wtpd_exprs E es; prg E \ xs -es[\]vs-> xs'\ \ xs'::\E"
  apply (simp only: wtpd_exprs_def)
  apply (erule exE)
  apply (case_tac xs)
  apply (case_tac xs')
  apply (auto intro: evals_type_sound [THEN conjunct1])
  done

lemma state_ok_exec:
  "\xs::\E; wf_java_prog (prg E); wtpd_stmt E st; prg E \ xs -st-> xs'\ \ xs'::\E"
  apply (simp only: wtpd_stmt_def)
  apply (case_tac xs', case_tac xs)
  apply (auto dest: exec_type_sound)
  done

lemma state_ok_init:
  "\ wf_java_prog G; (x, h, l)::\(env_of_jmb G C S);
  is_class G dynT;
  method (G, dynT) (mn, pTs) = Some (md, rT, pns, lvars, blk, res);
  list_all2 (conf G h) pvs pTs; G,h \<turnstile> a' ::\<preceq> Class md\<rbrakk>
  \<Longrightarrow>
  (np a' x, h, init_vars lvars(pns[\]pvs)(This\a'))::\(env_of_jmb G md (mn, pTs))"
  apply (frule wf_prog_ws_prog)
  apply (frule method_in_md [THEN conjunct2], assumption+)
  apply (frule method_yields_wf_java_mdecl, assumption, assumption)
  apply (simp add: env_of_jmb_def gs_def conforms_def split_beta)
  apply (simp add: wf_java_mdecl_def)
  apply (rule conjI)
   apply (rule lconf_ext)
    apply (rule lconf_ext_list)
       apply (rule lconf_init_vars)
       apply (auto dest: Ball_set_table)
  apply (simp add: np_def xconf_raise_if)
  done

lemma ty_exprs_list_all2 [rule_format (no_asm)]:
  "(\ Ts. (E \ es [::] Ts) = list_all2 (\e T. E \ e :: T) es Ts)"
  apply (rule list.induct)
   apply simp
   apply (rule allI)
   apply (rule iffI)
    apply (ind_cases "E \ [] [::] Ts" for Ts, assumption)
   apply simp apply (rule WellType.Nil)
  apply (simp add: list_all2_Cons1)
  apply (rule allI)
  apply (rule iffI)
   apply (rename_tac a exs Ts)
   apply (ind_cases "E \ a # exs [::] Ts" for a exs Ts) apply blast
  apply (auto intro: WellType.Cons)
  done

lemma conf_bool: "G,h \ v::\PrimT Boolean \ \ b. v = Bool b"
  apply (simp add: conf_def)
  apply (erule exE)
  apply (case_tac v)
      apply (auto elim: widen.cases)
  done

lemma max_spec_widen: "max_spec G C (mn, pTs) = {((md,rT),pTs')} \
  list_all2 (\<lambda> T T'. G \<turnstile> T \<preceq> T') pTs pTs'"
  by (blast dest: singleton_in_set max_spec2appl_meths appl_methsD)

lemma eval_conf: "\G \ s -e\v-> s'; wf_java_prog G; s::\E;
  E\<turnstile>e::T; gx s' = None; prg E = G \<rbrakk>
  \<Longrightarrow> G,gh s'\<turnstile>v::\<preceq>T"
  apply (simp add: gh_def)
  apply (rule_tac x3="fst s" and s3="snd s"and x'3="fst s'"
               in eval_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]], simplified])
       apply assumption+
      apply (simp (no_asm_use))
     apply (simp only: surjective_pairing [symmetric])
    apply (auto simp add: gs_def gx_def)
  done

lemma evals_preserves_conf:
  "\ G\ s -es[\]vs-> s'; G,gh s \ t ::\ T; E \es[::]Ts;
  wf_java_prog G; s::\<preceq>E;
  prg E = G \<rbrakk> \<Longrightarrow> G,gh s' \<turnstile> t ::\<preceq> T"
  apply (subgoal_tac "gh s\| gh s'")
   apply (frule conf_hext, assumption, assumption)
  apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]])
   apply (subgoal_tac "G \ (gx s, (gh s, gl s)) -es[\]vs-> (gx s', (gh s', gl s'))")
    apply assumption
   apply (simp add: gx_def gh_def gl_def)
  apply (case_tac E)
  apply (simp add: gx_def gs_def gh_def gl_def)
  done

lemma eval_of_class:
  "\ G \ s -e\a'-> s'; E \ e :: Class C; wf_java_prog G; s::\E; gx s'=None; a' \ Null; G=prg E\
  \<Longrightarrow> (\<exists> lc. a' = Addr lc)"
  apply (case_tac s, case_tac s', simp)
  apply (frule eval_type_sound, (simp add: gs_def)+)
  apply (case_tac a')
      apply (auto simp: conf_def)
  done

lemma dynT_subcls:
  "\ a' \ Null; G,h\a'::\ Class C; dynT = fst (the (h (the_Addr a')));
  is_class G dynT; ws_prog G \<rbrakk> \<Longrightarrow> G\<turnstile>dynT \<preceq>C C"
  apply (case_tac "C = Object")
   apply (simp, rule subcls_C_Object, assumption+)
  apply simp
  apply (frule non_np_objD, auto)
  done

lemma method_defined: "\
  m = the (method (G, dynT) (mn, pTs));
  dynT = fst (the (h a)); is_class G dynT; wf_java_prog G;
  a' \ Null; G,h\a'::\ Class C; a = the_Addr a';
  \<exists>pTsa md rT. max_spec G C (mn, pTsa) = {((md, rT), pTs)} \<rbrakk>
\<Longrightarrow> (method (G, dynT) (mn, pTs)) = Some m"
  apply (erule exE)+
  apply (drule singleton_in_set, drule max_spec2appl_meths)
  apply (simp add: appl_methds_def)
  apply (elim exE conjE)
  apply (drule widen_methd)
  apply (auto intro!: dynT_subcls)
  done

(**********************************************************************)

(* 1. any difference between locvars_xstate \<dots> and L ??? *)
(* 2. possibly skip env_of_jmb ??? *)
theorem compiler_correctness:
  "wf_java_prog G \
  (G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow>
  gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
  (\<forall> os CL S.
  (class_sig_defined G CL S) \<longrightarrow>
  (wtpd_expr (env_of_jmb G CL S) ex) \<longrightarrow>
  (xs ::\<preceq> (env_of_jmb G CL S)) \<longrightarrow>
  ( {TranslComp.comp G, CL, S} \<turnstile>
    {gh xs, os, (locvars_xstate G CL S xs)}
    >- (compExpr (gmb G CL S) ex) \<rightarrow>
    {gh xs', val#os, locvars_xstate G CL S xs'}))) \<and>

(G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow>
  gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
  (\<forall> os CL S.
  (class_sig_defined G CL S) \<longrightarrow>
  (wtpd_exprs (env_of_jmb G CL S) exs) \<longrightarrow>
  (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
  ( {TranslComp.comp G, CL, S} \<turnstile>
    {gh xs, os, (locvars_xstate G CL S xs)}
    >- (compExprs (gmb G CL S) exs) \<rightarrow>
    {gh xs', (rev vals)@os, (locvars_xstate G CL S xs')}))) \<and>

  (G \<turnstile> xs -st-> xs' \<longrightarrow>
   gx xs = None \<longrightarrow> gx xs' = None \<longrightarrow>
  (\<forall> os CL S.
  (class_sig_defined G CL S) \<longrightarrow>
  (wtpd_stmt (env_of_jmb G CL S) st) \<longrightarrow>
  (xs::\<preceq>(env_of_jmb G CL S)) \<longrightarrow>
  ( {TranslComp.comp G, CL, S} \<turnstile>
    {gh xs, os, (locvars_xstate G CL S xs)}
    >- (compStmt (gmb G CL S) st) \<rightarrow>
    {gh xs', os, (locvars_xstate G CL S xs')})))"
  apply (rule Eval.eval_evals_exec.induct)

                     (* case XcptE *)
                     apply simp

                    (* case NewC *)
                    apply clarify
                    apply (frule wf_prog_ws_prog [THEN wf_subcls1]) (* establish  wf ((subcls1 G)\<inverse>) *)
                    apply (simp add: c_hupd_hp_invariant)
                    apply (rule progression_one_step)
                    apply (rotate_tac 1, drule sym) (* reverse equation (a, None) = new_Addr (fst s) *)
                    apply (simp add: locvars_xstate_def locvars_locals_def comp_fields)

                   (* case Cast *)
                   apply (intro allI impI)
                   apply simp
                   apply (frule raise_if_NoneD)
                   apply (frule wtpd_expr_cast)
                   apply simp
                   apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, simp)
                    apply blast
                   apply (rule progression_one_step)
                   apply (simp add: raise_system_xcpt_def  gh_def comp_cast_ok)

                  (* case Lit *)
                  apply simp
                  apply (intro strip)
                  apply (rule progression_one_step)
                  apply simp

                 (* case BinOp *)
                 apply (intro allI impI)
                 apply (frule_tac xs=s1 in eval_xcpt, assumption) (* establish (gx s1 = None) *)
                 apply (frule wtpd_expr_binop)
                 (* establish (s1::\<preceq> \<dots>) *)
                 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)

                 apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
                 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e1" in progression_transitive, simp) apply blast
                 apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e2" in progression_transitive, simp) apply blast
                 apply (case_tac bop)
                  (*subcase bop = Eq *)
                  apply simp
                  apply (rule progression_Eq)
                 (*subcase bop = Add *)
                 apply simp
                 apply (rule progression_one_step)
                 apply simp

                (* case LAcc *)
                apply simp
                apply (intro strip)
                apply (rule progression_one_step)
                apply (simp add: locvars_xstate_def locvars_locals_def)
                apply (frule wtpd_expr_lacc)
                 apply assumption
                apply (simp add: gl_def)
                apply (erule select_at_index)

               (* case LAss *)
               apply (intro allI impI)
               apply (frule wtpd_expr_lass, erule conjE, erule conjE)
               apply simp

               apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
                apply blast

               apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
                apply (rule progression_one_step)
                apply (simp add: gh_def)
               apply simp
               apply (rule progression_one_step)
               apply (simp add: gh_def)
               (* the following falls out of the general scheme *)
               apply (frule wtpd_expr_lacc) apply assumption
               apply (rule update_at_index)
                 apply (rule distinct_method_if_class_sig_defined)
                  apply assumption
                 apply assumption
                apply simp
               apply assumption

              (* case FAcc *)
              apply (intro allI impI)
              (* establish x1 = None \<and> a' \<noteq> Null *)
              apply (simp (no_asm_use) only: gx_conv, frule np_NoneD)
              apply (frule wtpd_expr_facc)

              apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
              apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
               apply blast
              apply (rule progression_one_step)
              apply (simp add: gh_def)
              apply (case_tac "(the (fst s1 (the_Addr a')))")
              apply (simp add: raise_system_xcpt_def)

             (* case FAss *)
             apply (intro allI impI)
             apply (frule wtpd_expr_fass) apply (erule conjE) apply (frule wtpd_expr_facc)
             apply (simp only: c_hupd_xcpt_invariant) (* establish x2 = None *)
             (* establish x1 = None  and  a' \<noteq> Null  *)
             apply (frule_tac xs="(np a' x1, s1)" in eval_xcpt)
              apply (simp only: gx_conv, simp only: gx_conv, frule np_NoneD, erule conjE)

             (* establish ((Norm s1)::\<preceq> \<dots>) *)
             apply (frule_tac e=e1 in state_ok_eval)
                apply (simp (no_asm_simp) only: env_of_jmb_fst)
               apply assumption
              apply (simp (no_asm_use) only: env_of_jmb_fst)

             apply (simp only: compExpr.simps compExprs.simps)

             apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e1)" in progression_transitive, rule HOL.refl)
              apply fast (* blast does not seem to work - why? *)
             apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e2)" in progression_transitive, rule HOL.refl)
              apply fast
             apply (rule_tac ?instrs0.0 = "[Dup_x1]" and ?instrs1.0 = "[Putfield fn T]" in progression_transitive, simp)

              (* Dup_x1 *)
              apply (rule progression_one_step)
              apply (simp add: gh_def)

             (* Putfield \<longrightarrow> still looks nasty*)
             apply (rule progression_one_step)
             apply simp
             apply (case_tac "(the (fst s2 (the_Addr a')))")
             apply (simp add: c_hupd_hp_invariant)
             apply (case_tac s2)
             apply (simp add: c_hupd_conv raise_system_xcpt_def)
             apply (rule locvars_xstate_par_dep, rule HOL.refl)

            defer (* method call *)

            (* case XcptEs *)
            apply simp

           (* case Nil *)
           apply simp
           apply (intro strip)
           apply (rule progression_refl)

          (* case Cons *)
          apply (intro allI impI)
          apply (frule_tac xs=s1 in evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)
          apply (frule wtpd_exprs_cons)
          (* establish ((Norm s0)::\<preceq> \<dots>) *)
          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)

          apply simp
          apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
           apply fast
          apply fast

         (* case Statement: exception *)
         apply simp

        (* case Skip *)
        apply (intro allI impI)
        apply simp
        apply (rule progression_refl)

       (* case Expr *)
       apply (intro allI impI)
       apply (frule wtpd_stmt_expr)
       apply simp
       apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
        apply fast
       apply (rule progression_one_step)
       apply simp

      (* case Comp *)
      apply (intro allI impI)
      apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
      apply (frule wtpd_stmt_comp)

      (* establish (s1::\<preceq> \<dots>) *)
      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)

      apply simp
      apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, rule HOL.refl)
       apply fast
      apply fast

     (* case Cond *)
     apply (intro allI impI)
     apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
     apply (frule wtpd_stmt_cond, (erule conjE)+)
     (* establish (s1::\<preceq> \<dots>) *)
     apply (frule_tac e=e in state_ok_eval)
        apply (simp (no_asm_simp) only: env_of_jmb_fst)
       apply assumption
      apply (simp (no_asm_use) only: env_of_jmb_fst)
     (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
     apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
     apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
     apply (erule exE)

     apply simp
     apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
      apply (rule progression_one_step,  simp)

     apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
      apply fast

     apply (case_tac b)
      (* case b= True *)
      apply simp
      apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
       apply (rule progression_one_step)
       apply simp
      apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
       apply fast
      apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
        apply (simp)
       apply simp
       apply (rule conjI, simp)
       apply (simp add: nat_add_distrib)
      apply (rule progression_refl)

     (* case b= False *)
     apply simp
     apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
       apply (simp)
      apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
     apply fast

    (* case exit Loop *)
    apply (intro allI impI)
    apply (frule wtpd_stmt_loop, (erule conjE)+)

    (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
    apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
    apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
    apply (erule exE)
    apply (case_tac b)

     (* case b= True \<longrightarrow> contradiction *)
     apply simp

    (* case b= False *)
    apply simp

    apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
     apply (rule progression_one_step)
     apply simp

    apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
     apply fast
    apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
      apply (simp)
     apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
    apply (rule progression_refl)

   (* case continue Loop *)
   apply (intro allI impI)
   apply (frule_tac xs=s2 in exec_xcpt, assumption) (* establish (gx s2 = None) *)
   apply (frule_tac xs=s1 in exec_xcpt, assumption) (* establish (gx s1 = None) *)
   apply (frule wtpd_stmt_loop, (erule conjE)+)

   (* establish (s1::\<preceq> \<dots>) *)
   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)
   (* establish (s2::\<preceq> \<dots>) *)
   apply (frule_tac xs=s1 and st=c in state_ok_exec)
      apply (simp (no_asm_simp) only: env_of_jmb_fst)
     apply assumption
    apply (simp (no_asm_use) only: env_of_jmb_fst)

   (* establish G,gh s1\<turnstile>v::\<preceq>PrimT Boolean *)
   apply (frule eval_conf, assumption+, rule env_of_jmb_fst)
   apply (frule conf_bool) (* establish \<exists>b. v = Bool b *)
   apply (erule exE)

   apply simp
   apply (rule jump_bwd_progression)
      apply simp

     apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
      apply (rule progression_one_step)
      apply simp

     apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
      apply fast

     apply (case_tac b)
      (* case b= True *)
      apply simp

      apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
       apply (rule progression_one_step)
       apply simp
      apply fast

     (* case b= False \<longrightarrow> contradiction*)
     apply simp

    apply (rule jump_bwd_one_step)
    apply simp
   apply blast

  (*****)
  (* case method call *)

  apply (intro allI impI)

  apply (frule_tac xs=s3 in eval_xcpt, simp only: gx_conv) (* establish gx s3 = None *)
  apply (frule exec_xcpt, assumption, simp (no_asm_use) only: gx_conv, frule np_NoneD) (* establish x = None \<and> a' \<noteq> Null *)
  apply (frule evals_xcpt, simp only: gx_conv) (* establish gx s1 = None *)

  apply (frule wtpd_expr_call, (erule conjE)+)

  (* assumptions about state_ok and is_class *)

  (* establish s1::\<preceq> (env_of_jmb G CL S) *)
  apply (frule_tac xs="Norm s0" and e=e in state_ok_eval)
     apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp (no_asm_use) only: env_of_jmb_fst)

  (* establish (x, h, l)::\<preceq>(env_of_jmb G CL S) *)
  apply (frule_tac xs=s1 and xs'="(x, h, l)" in state_ok_evals)
     apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)

  (* establish \<exists> lc. a' = Addr lc *)
  apply (frule (5) eval_of_class, rule env_of_jmb_fst [symmetric])
  apply (subgoal_tac "G,h \ a' ::\ Class C")
   apply (subgoal_tac "is_class G dynT")

    (* establish method (G, dynT) (mn, pTs) = Some(md, rT, pns, lvars, blk, res) *)
    apply (drule method_defined, assumption+)
     apply (simp only: env_of_jmb_fst)
     apply ((erule exE)+, erule conjE, (rule exI)+, assumption)

    apply (subgoal_tac "is_class G md")
     apply (subgoal_tac "G\Class dynT \ Class md")
      apply (subgoal_tac " method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res)")
       apply (subgoal_tac "list_all2 (conf G h) pvs pTs")

        (* establish (np a' x, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(env_of_jmb G md (mn, pTs)) *)
        apply (subgoal_tac "G,h \ a' ::\ Class dynT")
         apply (frule (2) conf_widen)
         apply (frule state_ok_init, assumption+)

         apply (subgoal_tac "class_sig_defined G md (mn, pTs)")
          apply (frule wtpd_blk, assumption, assumption)
          apply (frule wtpd_res, assumption, assumption)
          apply (subgoal_tac "s3::\(env_of_jmb G md (mn, pTs))")

           apply (subgoal_tac "method (TranslComp.comp G, md) (mn, pTs) =
                               Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
            prefer 2
            apply (simp add: wf_prog_ws_prog [THEN comp_method])
           apply (subgoal_tac "method (TranslComp.comp G, dynT) (mn, pTs) =
                               Some (md, rT, snd (snd (compMethod G md ((mn, pTs), rT, pns, lvars, blk, res))))")
            prefer 2
            apply (simp add: wf_prog_ws_prog [THEN comp_method])
           apply (simp only: fst_conv snd_conv)

           (* establish length pns = length pTs *)
           apply (frule method_preserves_length, assumption, assumption)
           (* establish length pvs = length ps *)
           apply (frule evals_preserves_length [symmetric])

           (** start evaluating subexpressions **)
           apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)

           (* evaluate e *)
           apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
            apply fast

           (* evaluate parameters *)
           apply (rule_tac ?instrs0.0 = "compExprs (gmb G CL S) ps" in progression_transitive, rule HOL.refl)
            apply fast

           (* invokation *)
           apply (rule progression_call)
           apply (intro allI impI conjI)
              (* execute Invoke statement *)
              apply (simp (no_asm_use) only: exec_instr.simps)
              apply (erule thin_rl, erule thin_rl, erule thin_rl)
              apply (simp add: compMethod_def raise_system_xcpt_def)

             (* get instructions of invoked method *)
             apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)

            (* var. initialization *)
            apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
             apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
              apply (simp (no_asm_simp)) (* length pns = length pvs *)
             apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) undefined) *)

            (* body statement *)
            apply (rule_tac ?instrs0.0 = "compStmt (pns, lvars, blk, res) blk" in progression_transitive, rule HOL.refl)
             apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
              apply (simp (no_asm_simp))
              apply (simp only: gh_conv)
              apply (drule mp [OF _ TrueI])+
              apply (erule allE, erule allE, erule allE, erule impE, assumption)+
              apply ((erule impE, assumption)+, assumption)

             apply (simp (no_asm_use))
             apply (simp (no_asm_simp) add: gmb_def)

            (* return expression *)
            apply (subgoal_tac "(pns, lvars, blk, res) = gmb G md (mn, pTs)")
             apply (simp (no_asm_simp))
             apply (simp only: gh_conv)
             apply ((drule mp, rule TrueI)+, (drule spec)+, (drule mp, assumption)+, assumption)
            apply (simp (no_asm_use))
            apply (simp (no_asm_simp) add: gmb_def)

           (* execute return statement *)
           apply (simp (no_asm_use) add: gh_def locvars_xstate_def gl_def del: drop_append)
           apply (subgoal_tac "rev pvs @ a' # os = (rev (a' # pvs)) @ os")
            apply (simp only: drop_append)
            apply (simp (no_asm_simp))
           apply (simp (no_asm_simp))

          (* show s3::\<preceq>\<dots> *)
          apply (rule_tac xs = "(np a' x, h, init_vars lvars(pns[\]pvs)(This\a'))" and st=blk in state_ok_exec)
             apply assumption
            apply (simp (no_asm_simp) only: env_of_jmb_fst)
           apply assumption
          apply (simp (no_asm_use) only: env_of_jmb_fst)

         (* show class_sig_defined G md (mn, pTs) *)
         apply (simp (no_asm_simp) add: class_sig_defined_def)

        (* show G,h \<turnstile> a' ::\<preceq> Class dynT *)
        apply (frule non_npD)
         apply assumption
        apply (erule exE)+
        apply simp
        apply (rule conf_obj_AddrI)
        apply simp
        apply (rule widen_Class_Class [THEN iffD1], rule widen.refl)

       (* show list_all2 (conf G h) pvs pTs *)
       apply (erule exE)+ apply (erule conjE)+
       apply (rule_tac Ts="pTsa" in conf_list_gext_widen)
         apply assumption
        apply (subgoal_tac "G \ (gx s1, gs s1) -ps[\]pvs-> (x, h, l)")
         apply (frule_tac E="env_of_jmb G CL S" in evals_type_sound)
             apply assumption+
            apply (simp only: env_of_jmb_fst)
            apply (simp add: conforms_def xconf_def gs_def)
           apply simp
          apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [symmetric])
          apply (simp (no_asm_use) only: ty_exprs_list_all2)
          apply simp
         apply simp
        apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [symmetric])
       (* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *)
       apply (rule max_spec_widen, simp only: env_of_jmb_fst)

      (* show method (G, md) (mn, pTs) = Some (md, rT, pns, lvars, blk, res) *)
      apply (frule wf_prog_ws_prog [THEN method_in_md [THEN conjunct2]], assumption+)

     (* show G\<turnstile>Class dynT \<preceq> Class md *)
     apply (simp (no_asm_use) only: widen_Class_Class)
     apply (rule method_wf_mdecl [THEN conjunct1], assumption+)

    (* is_class G md *)
    apply (rule wf_prog_ws_prog [THEN method_in_md [THEN conjunct1]], assumption+)

   (* show is_class G dynT *)
   apply (frule non_npD)
    apply assumption
   apply (erule exE)+
   apply (erule conjE)+
   apply simp
   apply (rule subcls_is_class2)
    apply assumption
   apply (frule expr_class_is_class [rotated])
    apply (simp only: env_of_jmb_fst)
    apply (rule wf_prog_ws_prog, assumption)
   apply (simp only: env_of_jmb_fst)

  (* show G,h \<turnstile> a' ::\<preceq> Class C *)
  apply (simp only: wtpd_exprs_def, erule exE)
  apply (frule evals_preserves_conf)
       apply (rule eval_conf, assumption+)
       apply (rule env_of_jmb_fst, assumption+)
   apply (rule env_of_jmb_fst)
  apply (simp only: gh_conv)
  done

theorem compiler_correctness_eval: "
  \<lbrakk> G \<turnstile> (None,hp,loc) -ex \<succ> val-> (None,hp',loc');
  wf_java_prog G;
  class_sig_defined G C S;
  wtpd_expr (env_of_jmb G C S) ex;
  (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
  {(TranslComp.comp G), C, S} \<turnstile>
    {hp, os, (locvars_locals G C S loc)}
      >- (compExpr (gmb G C S) ex) \<rightarrow>
    {hp', val#os, (locvars_locals G C S loc')}"
  apply (frule compiler_correctness [THEN conjunct1])
  apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
  done

theorem compiler_correctness_exec: "
  \<lbrakk> G \<turnstile> Norm (hp, loc) -st-> Norm (hp', loc');
  wf_java_prog G;
  class_sig_defined G C S;
  wtpd_stmt (env_of_jmb G C S) st;
  (None,hp,loc) ::\<preceq> (env_of_jmb G C S) \<rbrakk> \<Longrightarrow>
  {(TranslComp.comp G), C, S} \<turnstile>
    {hp, os, (locvars_locals G C S loc)}
      >- (compStmt (gmb G C S) st) \<rightarrow>
    {hp', os, (locvars_locals G C S loc')}"
  apply (frule compiler_correctness [THEN conjunct2 [THEN conjunct2]])
  apply (auto simp: gh_def gx_def gs_def gl_def locvars_xstate_def)
  done

(**********************************************************************)

(* reinstall pair splits *)
declare split_paired_All [simp] split_paired_Ex [simp]

declare wf_prog_ws_prog [simp del]

end

¤ Dauer der Verarbeitung: 0.33 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.