Theory CorrCompTp

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

theory CorrCompTp
imports LemmasComp TypeInf "../BV/JVM" "../BV/Altern"
begin

declare split_paired_All [simp del]
declare split_paired_Ex [simp del]


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

definition inited_LT :: "[cname, ty list, (vname × ty) list] ⇒ locvars_type" where
  "inited_LT C pTs lvars == (OK (Class C))#((map OK pTs))@(map (Fun.comp OK snd) lvars)"

definition is_inited_LT :: "[cname, ty list, (vname × ty) list, locvars_type] ⇒ bool" where
  "is_inited_LT C pTs lvars LT == (LT = (inited_LT C pTs lvars))"

definition local_env :: "[java_mb prog, cname, sig, vname list,(vname × ty) list] ⇒ java_mb env" where
  "local_env G C S pns lvars == 
     let (mn, pTs) = S in (G,(map_of lvars)(pns[↦]pTs, This↦Class C))"

lemma local_env_fst [simp]: "fst (local_env G C S pns lvars) = G"
  by (simp add: local_env_def split_beta)


lemma wt_class_expr_is_class:
  "⟦ ws_prog G; E ⊢ expr :: Class cname; E = local_env G C (mn, pTs) pns lvars⟧
  ⟹ is_class G cname "
  apply (subgoal_tac "((fst E), (snd E)) ⊢ expr :: Class cname")
   apply (frule ty_expr_is_type)
    apply simp
   apply simp
  apply (simp (no_asm_use))
  done



(********************************************************************************)
subsection "index"

lemma local_env_snd:
  "snd (local_env G C (mn, pTs) pns lvars) = (map_of lvars)(pns[↦]pTs, This↦Class C)"
  by (simp add: local_env_def)



lemma index_in_bounds:
  "length pns = length pTs ⟹
  snd (local_env G C (mn, pTs) pns lvars) vname = Some T
       ⟹ index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)"
  apply (simp add: local_env_snd index_def split_beta)
  apply (case_tac "vname = This")
   apply (simp add: inited_LT_def)
  apply simp
  apply (drule map_of_upds_SomeD)
  apply (drule length_takeWhile)
  apply (simp add: inited_LT_def)
  done


lemma map_upds_append: 
  "length k1s = length x1s ⟹ m(k1s[↦]x1s, k2s[↦]x2s) = m ((k1s@k2s)[↦](x1s@x2s))"
  apply (induct k1s arbitrary: x1s m)
   apply simp
  apply (subgoal_tac "∃x xr. x1s = x # xr")
   apply clarsimp
  (* subgoal *)
  apply (case_tac x1s)
   apply auto
  done


lemma map_of_append: 
  "map_of ((rev xs) @ ys) = (map_of ys) ((map fst xs) [↦] (map snd xs))"
  apply (induct xs arbitrary: ys)
   apply simp
  apply (rename_tac a xs ys)
  apply (drule_tac x="a # ys" in meta_spec)
  apply (simp only: rev.simps append_assoc append_Cons append_Nil
                    list.map map_of.simps map_upds_Cons list.sel)
  done

lemma map_of_as_map_upds: "map_of (rev xs) = Map.empty ((map fst xs) [↦] (map snd xs))"
  by (rule map_of_append [of _ "[]", simplified])

lemma map_of_rev: "unique xs ⟹ map_of (rev xs) = map_of xs"
  apply (induct xs)
   apply simp
  apply (simp add: unique_def map_of_append map_of_as_map_upds [symmetric]
                   Map.map_of_append[symmetric] del:Map.map_of_append)
  done

lemma map_upds_rev:
  "⟦ distinct ks; length ks = length xs ⟧ ⟹ m (rev ks [↦] rev xs) = m (ks [↦] xs)"
  apply (induct ks arbitrary: xs)
   apply simp
  apply (subgoal_tac "∃x xr. xs = x # xr")
   apply clarify
   apply (drule_tac x=xr in meta_spec)
   apply (simp add: map_upds_append [symmetric])
  apply (case_tac xs, auto)
  done

lemma map_upds_takeWhile [rule_format]:
  "∀ks. (Map.empty(rev ks[↦]rev xs)) k = Some x ⟶ length ks = length xs ⟶
    xs ! length (takeWhile (λz. z ≠ k) ks) = x"
  apply (induct xs)
   apply simp
  apply (intro strip)
  apply (subgoal_tac "∃k' kr. ks = k' # kr")
   apply (clarify)
   apply (drule_tac x=kr in spec)
   apply (simp only: rev.simps)
   apply (subgoal_tac "(Map.empty(rev kr @ [k'][↦]rev xs @ [a])) = Map.empty (rev kr[↦]rev xs, [k'][↦][a])")
    apply (simp split:if_split_asm)
   apply (simp add: map_upds_append [symmetric])
  apply (case_tac ks)
   apply auto
  done


lemma local_env_inited_LT:
  "⟦ snd (local_env G C (mn, pTs) pns lvars) vname = Some T;
  length pns = length pTs; distinct pns; unique lvars ⟧
  ⟹ (inited_LT C pTs lvars ! index (pns, lvars, blk, res) vname) = OK T"
  apply (simp add: local_env_snd index_def)
  apply (case_tac "vname = This")
   apply (simp add: inited_LT_def)
  apply (simp add: inited_LT_def)
  apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] list.map [symmetric])
  apply (subgoal_tac "length (takeWhile (λz. z ≠ vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
   apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
   apply (subgoal_tac "map_of lvars = map_of (map (λ p. (fst p, snd p)) lvars)")
    apply (simp only:)
    apply (subgoal_tac "distinct (map fst lvars)")
     apply (frule_tac g=snd in AuxLemmas.map_of_map_as_map_upd)
     apply (simp only:)
     apply (simp add: map_upds_append)
     apply (frule map_upds_SomeD)
     apply (rule map_upds_takeWhile)
      apply (simp (no_asm_simp))
      apply (simp add: map_upds_append [symmetric])
      apply (simp add: map_upds_rev)

     (* show length (pns @ map fst lvars) = length (pTs @ map snd lvars) *)
     apply simp

    (* show distinct (map fst lvars) *)
    apply (simp only: unique_def Fun.comp_def)

   (* show map_of lvars = map_of (map (λp. (fst p, snd p)) lvars) *)
   apply simp

  (* show length (takeWhile (λz. z ≠ vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars) *)
  apply (drule map_of_upds_SomeD)
  apply (drule length_takeWhile)
  apply simp
  done


lemma inited_LT_at_index_no_err:
  "i < length (inited_LT C pTs lvars) ⟹ inited_LT C pTs lvars ! i ≠ Err"
  apply (simp only: inited_LT_def)
  apply (simp only: map_map [symmetric] map_append [symmetric] list.map [symmetric] length_map)
  apply (simp only: nth_map)
  apply simp
  done


lemma sup_loc_update_index: "
  ⟦ G ⊢ T ≼ T'; is_type G T'; length pns = length pTs; distinct pns; unique lvars;
  snd (local_env G C (mn, pTs) pns lvars) vname = Some T' ⟧
  ⟹ 
  comp G ⊢ (inited_LT C pTs lvars) [index (pns, lvars, blk, res) vname := OK T] <=l 
           inited_LT C pTs lvars"
  apply (subgoal_tac " index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)")
   apply (frule_tac blk=blk and res=res in local_env_inited_LT, assumption+)
   apply (rule sup_loc_trans)
    apply (rule_tac b="OK T'" in sup_loc_update)
      apply (simp add: comp_widen)
     apply assumption
    apply (rule sup_loc_refl)
   apply (simp add: list_update_same_conv [THEN iffD2])
  (* subgoal *)
  apply (rule index_in_bounds)
   apply simp+
  done


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

subsection "Preservation of ST and LT by compTpExpr / compTpStmt"

lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp"
  by (simp add: comb_nil_def)

lemma mt_of_comb_nil [simp]: "mt_of (comb_nil sttp) = []"
  by (simp add: comb_nil_def)


lemma sttp_of_comb [simp]: "sttp_of ((f1 □ f2) sttp) = sttp_of (f2 (sttp_of (f1 sttp)))"
  apply (case_tac "f1 sttp")
  apply (case_tac "(f2 (sttp_of (f1 sttp)))")
  apply (simp add: comb_def)
  done

lemma mt_of_comb: "(mt_of ((f1 □ f2) sttp)) = 
  (mt_of (f1 sttp)) @ (mt_of (f2 (sttp_of (f1 sttp))))"
  by (simp add: comb_def split_beta)


lemma mt_of_comb_length [simp]: "⟦ n1 = length (mt_of (f1 sttp)); n1 ≤ n ⟧
  ⟹ (mt_of ((f1 □ f2) sttp) ! n) = (mt_of (f2 (sttp_of (f1 sttp))) ! (n - n1))"
  by (simp add: comb_def nth_append split_beta)


lemma compTpExpr_Exprs_LT_ST: "
  ⟦jmb = (pns, lvars, blk, res);
  wf_prog wf_java_mdecl G;
  wf_java_mdecl G C ((mn, pTs), rT, jmb);
  E = local_env G C (mn, pTs) pns lvars ⟧
  ⟹
  (∀ ST LT T.
  E ⊢ ex :: T ⟶
  is_inited_LT C pTs lvars LT ⟶
  sttp_of (compTpExpr jmb G ex (ST, LT)) = (T # ST, LT))
  ∧
  (∀ ST LT Ts.
  E ⊢ exs [::] Ts ⟶
  is_inited_LT C pTs lvars LT ⟶
  sttp_of (compTpExprs jmb G exs (ST, LT)) = ((rev Ts) @ ST, LT))"

  apply (rule compat_expr_expr_list.induct)

            (* expresssions *)

            (* NewC *)
            apply (intro strip)
            apply (drule NewC_invers)
            apply (simp add: pushST_def)

           (* Cast *)
           apply (intro strip)
           apply (drule Cast_invers, clarify)
           apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
           apply (simp add: replST_def split_beta)

          (* Lit *)
          apply (intro strip)
          apply (drule Lit_invers)
          apply (simp add: pushST_def)

         (* BinOp *)
         apply (intro strip)
         apply (drule BinOp_invers, clarify)
         apply (drule_tac x=ST in spec)
         apply (drule_tac x="Ta # ST" in spec)
         apply ((drule spec)+, (drule mp, assumption)+)
         apply (rename_tac binop x2 x3 ST LT T Ta, case_tac binop)
          apply (simp (no_asm_simp))
          apply (simp (no_asm_simp) add: popST_def pushST_def)
         apply (simp)
         apply (simp (no_asm_simp) add: replST_def)


        (* LAcc *)
        apply (intro strip)
        apply (drule LAcc_invers)
        apply (simp add: pushST_def is_inited_LT_def)
        apply (simp add: wf_prog_def)
        apply (frule wf_java_mdecl_disjoint_varnames)
        apply (simp add: disjoint_varnames_def)
        apply (frule wf_java_mdecl_length_pTs_pns)
        apply (erule conjE)+
        apply (simp (no_asm_simp) add: local_env_inited_LT)

       (* LAss *)
       apply (intro strip)
       apply (drule LAss_invers, clarify)
       apply (drule LAcc_invers)
       apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
       apply (simp add: popST_def dupST_def)

      (* FAcc *)
      apply (intro strip)
      apply (drule FAcc_invers, clarify)
      apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
      apply (simp add: replST_def)

      (* show   snd (the (field (G, cname) vname)) = T *)
      apply (subgoal_tac "is_class G Ca")
       apply (rename_tac cname x2 vname ST LT T Ca, subgoal_tac "is_class G cname ∧ field (G, cname) vname = Some (cname, T)")
        apply simp

       (* show is_class G cname ∧ field (G, cname) vname = Some (cname, T) *)
       apply (rule field_in_fd) apply assumption+
      (* show is_class G Ca *)
      apply (fast intro: wt_class_expr_is_class)

     (* FAss *)
     apply (intro strip)
     apply (drule FAss_invers, clarify)
     apply (drule FAcc_invers, clarify)
     apply (drule_tac x=ST in spec)
     apply (drule_tac x="Class Ca # ST" in spec)
     apply ((drule spec)+, (drule mp, assumption)+)
     apply (simp add: popST_def dup_x1ST_def)


    (* Call *)
    apply (intro strip)
    apply (drule Call_invers, clarify)
    apply (drule_tac x=ST in spec)
    apply (rename_tac cname x2 x3 x4 x5 ST LT T pTsa md, drule_tac x="Class cname # ST" in spec)
    apply ((drule spec)+, (drule mp, assumption)+)
    apply (simp add: replST_def)


   (* expression lists *)
   (* nil *)

   apply (intro strip)
   apply (drule Nil_invers)
   apply (simp add: comb_nil_def)

  (* cons *)

  apply (intro strip)
  apply (drule Cons_invers, clarify)
  apply (drule_tac x=ST in spec)
  apply (drule_tac x="T # ST" in spec)
  apply ((drule spec)+, (drule mp, assumption)+)
  apply simp

  done



lemmas compTpExpr_LT_ST [rule_format (no_asm)] = 
  compTpExpr_Exprs_LT_ST [THEN conjunct1]

lemmas compTpExprs_LT_ST [rule_format (no_asm)] = 
  compTpExpr_Exprs_LT_ST [THEN conjunct2]

lemma compTpStmt_LT_ST [rule_format (no_asm)]: "
  ⟦ jmb = (pns,lvars,blk,res); 
  wf_prog wf_java_mdecl G;
  wf_java_mdecl G C ((mn, pTs), rT, jmb);
  E = (local_env G C (mn, pTs) pns lvars)⟧ 
⟹ (∀ ST LT.
  E ⊢ s√ ⟶
  (is_inited_LT C pTs lvars LT)
⟶ sttp_of (compTpStmt jmb G s (ST, LT)) = (ST, LT))"

  apply (rule stmt.induct)

      (* Skip *)
      apply (intro strip)
      apply simp

     (* Expr *)
     apply (intro strip)
     apply (drule Expr_invers, erule exE)
     apply (simp (no_asm_simp) add: compTpExpr_LT_ST)
     apply (frule_tac ST=ST in compTpExpr_LT_ST, assumption+)
     apply (simp add: popST_def)

    (* Comp *)
    apply (intro strip)
    apply (drule Comp_invers, clarify)
    apply (simp (no_asm_use))
    apply simp

   (* Cond *)
   apply (intro strip)
   apply (drule Cond_invers)
   apply (erule conjE)+
   apply (drule_tac x=ST in spec)
   apply (drule_tac x=ST in spec)
   apply (drule spec)+ apply (drule mp, assumption)+
   apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
   apply (simp add: popST_def pushST_def nochangeST_def)

  (* Loop *)
  apply (intro strip)
  apply (drule Loop_invers)
  apply (erule conjE)+
  apply (drule_tac x=ST in spec)
  apply (drule spec)+ apply (drule mp, assumption)+
  apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
  apply (simp add: popST_def pushST_def nochangeST_def)
  done



lemma compTpInit_LT_ST: "
  sttp_of (compTpInit jmb (vn,ty) (ST, LT)) = (ST, LT[(index jmb vn):= OK ty])"
  by (simp add: compTpInit_def storeST_def pushST_def)


lemma compTpInitLvars_LT_ST_aux [rule_format (no_asm)]:
  "∀ pre lvars_pre lvars0.
  jmb = (pns,lvars0,blk,res) ∧
  lvars0 = (lvars_pre @ lvars) ∧
  (length pns) + (length lvars_pre) + 1 = length pre ∧
  disjoint_varnames pns (lvars_pre @ lvars)
  ⟶
sttp_of (compTpInitLvars jmb lvars (ST, pre @ replicate (length lvars) Err))
    = (ST, pre @ map (Fun.comp OK snd) lvars)"
  supply [[simproc del: defined_all]]
  apply (induct lvars)
   apply simp

  apply (intro strip)
  apply (subgoal_tac "∃vn ty. a = (vn, ty)")
   prefer 2
   apply (simp (no_asm_simp))
  apply ((erule exE)+, simp (no_asm_simp))

  apply (drule_tac x="pre @ [OK ty]" in spec)
  apply (drule_tac x="lvars_pre @ [a]" in spec)
  apply (drule_tac x="lvars0" in spec)
  apply (simp add: compTpInit_LT_ST index_of_var2)
  done

lemma compTpInitLvars_LT_ST: 
  "⟦ jmb = (pns, lvars, blk, res); wf_java_mdecl G C ((mn, pTs), rT, jmb) ⟧
  ⟹ sttp_of (compTpInitLvars jmb lvars (ST, start_LT C pTs (length lvars)))
      = (ST, inited_LT C pTs lvars)"
  apply (simp add: start_LT_def inited_LT_def)
  apply (simp only: append_Cons [symmetric])
  apply (rule compTpInitLvars_LT_ST_aux)
  apply (auto dest: wf_java_mdecl_length_pTs_pns wf_java_mdecl_disjoint_varnames)
  done



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

lemma max_of_list_elem: "x ∈ set xs ⟹ x ≤ (max_of_list xs)"
  by (induct xs, auto intro: max.cobounded1 simp: le_max_iff_disj max_of_list_def)

lemma max_of_list_sublist: "set xs ⊆ set ys 
  ⟹ (max_of_list xs) ≤ (max_of_list ys)"
  by (induct xs, auto dest: max_of_list_elem simp: max_of_list_def)

lemma max_of_list_append [simp]:
  "max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)" 
  apply (simp add: max_of_list_def)
  apply (induct xs)
   apply simp_all
  done


lemma app_mono_mxs: "⟦ app i G mxs rT pc et s; mxs ≤ mxs' ⟧ 
  ⟹ app i G mxs' rT pc et s"
  apply (case_tac s)
   apply (simp add: app_def)
  apply (case_tac i, auto intro: less_trans)
  done



lemma err_mono [simp]: "A ⊆ B ⟹ err A ⊆ err B"
  by (auto simp: err_def)

lemma opt_mono [simp]: "A ⊆ B ⟹ opt A ⊆ opt B"
  by (auto simp: opt_def)


lemma states_mono: "⟦ mxs ≤ mxs' ⟧
  ⟹ states G mxs mxr ⊆ states G mxs' mxr"
  apply (simp add: states_def JVMType.sl_def)
  apply (simp add: Product.esl_def stk_esl_def reg_sl_def
                   upto_esl_def Listn.sl_def Err.sl_def  JType.esl_def)
  apply (simp add: Err.esl_def Err.le_def Listn.le_def)
  apply (simp add: Product.le_def Product.sup_def Err.sup_def)
  apply (simp add: Opt.esl_def Listn.sup_def)
  apply (rule err_mono)
  apply (rule opt_mono)
  apply (rule Sigma_mono)
   apply (rule Union_mono)
   apply auto
  done


lemma check_type_mono:
  "⟦ check_type G mxs mxr s; mxs ≤ mxs' ⟧ ⟹ check_type G mxs' mxr s"
  apply (simp add: check_type_def)
  apply (frule_tac G=G and mxr=mxr in states_mono)
  apply auto
  done


(* wt is preserved when adding instructions/state-types at the end *)
lemma wt_instr_prefix: "
  ⟦ wt_instr_altern (bc ! pc) cG rT mt mxs mxr max_pc et pc; 
    bc' = bc @ bc_post; mt' = mt @ mt_post; 
    mxs ≤ mxs'; max_pc ≤ max_pc'; 
    pc < length bc; pc < length mt; 
    max_pc = (length mt)⟧
  ⟹ wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' et pc"
  apply (simp add: wt_instr_altern_def nth_append)
  apply (auto intro: app_mono_mxs check_type_mono)
  done


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



lemma pc_succs_shift:
  "pc'∈set (succs i (pc'' + n)) ⟹ ((pc' - n) ∈set (succs i pc''))"
  apply (induct i, simp_all)
  apply arith
  done


lemma pc_succs_le:
  "⟦ pc' ∈ set (succs i (pc'' + n));   
     ∀b. ((i = (Goto b) ∨ i=(Ifcmpeq b)) ⟶ 0 ≤ (int pc'' + b)) ⟧
  ⟹ n ≤ pc'"
  apply (induct i, simp_all)
  apply arith
  done


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

definition offset_xcentry :: "[nat, exception_entry] ⇒ exception_entry" where
  "offset_xcentry == 
      λ n (start_pc, end_pc, handler_pc, catch_type).
          (start_pc + n, end_pc + n, handler_pc + n, catch_type)"

definition offset_xctable :: "[nat, exception_table] ⇒ exception_table" where
  "offset_xctable n == (map (offset_xcentry n))"

lemma match_xcentry_offset [simp]: "
  match_exception_entry G cn (pc + n) (offset_xcentry n ee) = 
  match_exception_entry G cn pc ee"
  by (simp add: match_exception_entry_def offset_xcentry_def split_beta)

lemma match_xctable_offset: "
  (match_exception_table G cn (pc + n) (offset_xctable n et)) =
  (map_option (λ pc'. pc' + n) (match_exception_table G cn pc et))"
  apply (induct et)
   apply (simp add: offset_xctable_def)+
  apply (case_tac "match_exception_entry G cn pc a")
   apply (simp add: offset_xcentry_def split_beta)+
  done


lemma match_offset [simp]: "
  match G cn (pc + n) (offset_xctable n et) = match G cn pc et"
  apply (induct et)
   apply (simp add: offset_xctable_def)+
  done

lemma match_any_offset [simp]: "
  match_any G (pc + n) (offset_xctable n et) = match_any G pc et"
  apply (induct et)
   apply (simp add: offset_xctable_def offset_xcentry_def split_beta)+
  done

lemma app_mono_pc: "⟦ app i G mxs rT pc et s; pc'= pc + n ⟧ 
  ⟹ app i G mxs rT pc' (offset_xctable n et) s"
  apply (case_tac s)
   apply (simp add: app_def)
  apply (case_tac i, auto)
  done

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

  (* Currently: empty exception_table *)

abbreviation (input)
  empty_et :: exception_table
  where "empty_et == []"



  (* move into Effect.thy *)
lemma xcpt_names_Nil [simp]: "(xcpt_names (i, G, pc, [])) = []"
  by (induct i, simp_all)

lemma xcpt_eff_Nil [simp]: "(xcpt_eff i G pc s []) = []"
  by (simp add: xcpt_eff_def)


lemma app_jumps_lem: "⟦ app i cG mxs rT pc empty_et s; s=(Some st) ⟧
  ⟹  ∀ b. ((i = (Goto b) ∨ i=(Ifcmpeq b)) ⟶ 0 ≤ (int pc + b))"
  by (induct i) auto


(* wt is preserved when adding instructions/state-types to the front *)
lemma wt_instr_offset: "
 ⟦ ∀ pc'' < length mt. 
    wt_instr_altern ((bc@bc_post) ! pc'') cG rT (mt@mt_post) mxs mxr max_pc empty_et pc''; 
  bc' = bc_pre @ bc @ bc_post; mt' = mt_pre @ mt @ mt_post; 
  length bc_pre = length mt_pre; length bc = length mt;
  length mt_pre ≤ pc; pc < length (mt_pre @ mt); 
  mxs ≤ mxs'; max_pc + length mt_pre ≤ max_pc' ⟧
⟹ wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' empty_et pc"
  apply (simp add: wt_instr_altern_def)
  apply (subgoal_tac "∃ pc''. pc = pc'' + length mt_pre", erule exE)
   prefer 2
   apply (rule_tac x="pc - length mt_pre" in exI, arith)

  apply (drule_tac x=pc'' in spec)
  apply (drule mp) 
   apply arith    (* show pc'' < length mt *)
  apply clarify

  apply (rule conjI)
   (* app *)
   apply (simp add: nth_append)
   apply (rule app_mono_mxs)
    apply (frule app_mono_pc)
     apply (rule HOL.refl)
    apply (simp add: offset_xctable_def)
   apply assumption+

  (* check_type *)
  apply (rule conjI)
   apply (simp add: nth_append)
   apply (rule  check_type_mono)
    apply assumption+

  (* ..eff.. *)
  apply (intro ballI)
  apply (subgoal_tac "∃ pc' s'. x = (pc', s')", (erule exE)+, simp)

   apply (case_tac s')
    (* s' = None *)
    apply (simp add: eff_def nth_append norm_eff_def)
    apply (frule_tac x="(pc', None)" and  f=fst and b=pc' in rev_image_eqI)
     apply (simp (no_asm_simp))
    apply (simp add: image_comp Fun.comp_def)
    apply (frule pc_succs_shift)
    apply (drule bspec, assumption)
    apply arith

   (* s' = Some a *)
   apply (drule_tac x="(pc' - length mt_pre, s')" in bspec)

    (* show  (pc' - length mt_pre, s') ∈ set (eff …) *)
    apply (simp add: eff_def)
    (* norm_eff *)
    apply (clarsimp simp: nth_append pc_succs_shift)

   (* show P x of bspec *)
   apply simp
   apply (subgoal_tac "length mt_pre ≤ pc'")
    apply (simp add: nth_append)
    apply arith

   (* subgoals *)
   apply (simp add: eff_def xcpt_eff_def)
   apply (clarsimp)
   apply (rule pc_succs_le,  assumption+)
   apply (subgoal_tac "∃ st. mt ! pc'' = Some st", erule exE)
    apply (rule_tac s="Some st" and st=st and cG=cG and mxs=mxs and rT=rT in app_jumps_lem)
     apply (simp add: nth_append)+
   (* subgoal ∃ st. mt ! pc'' = Some st *)
   apply (simp add: norm_eff_def map_option_case nth_append)
   apply (case_tac "mt ! pc''")
    apply simp+
  done


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


definition start_sttp_resp_cons :: "[state_type ⇒ method_type × state_type] ⇒ bool" where
  "start_sttp_resp_cons f == 
     (∀ sttp. let (mt', sttp') = (f sttp) in (∃mt'_rest. mt' = Some sttp # mt'_rest))"

definition start_sttp_resp :: "[state_type ⇒ method_type × state_type] ⇒ bool" where
  "start_sttp_resp f == (f = comb_nil) ∨ (start_sttp_resp_cons f)"

lemma start_sttp_resp_comb_nil [simp]: "start_sttp_resp comb_nil"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_cons_comb_cons [simp]: "start_sttp_resp_cons f 
  ⟹ start_sttp_resp_cons (f □ f')"
  apply (simp add: start_sttp_resp_cons_def comb_def split_beta)
  apply (rule allI)
  apply (drule_tac x=sttp in spec)
  apply auto
  done

lemma start_sttp_resp_cons_comb_cons_r: "⟦ start_sttp_resp f; start_sttp_resp_cons f'⟧
  ⟹ start_sttp_resp_cons (f □ f')"
  by (auto simp: start_sttp_resp_def)

lemma start_sttp_resp_cons_comb [simp]: "start_sttp_resp_cons f 
  ⟹ start_sttp_resp (f □ f')"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_comb: "⟦ start_sttp_resp f; start_sttp_resp f' ⟧
  ⟹ start_sttp_resp (f □ f')"
  by (auto simp: start_sttp_resp_def)

lemma start_sttp_resp_cons_nochangeST [simp]: "start_sttp_resp_cons nochangeST"
  by (simp add: start_sttp_resp_cons_def nochangeST_def)

lemma start_sttp_resp_cons_pushST [simp]: "start_sttp_resp_cons (pushST Ts)"
  by (simp add: start_sttp_resp_cons_def pushST_def split_beta)

lemma start_sttp_resp_cons_dupST [simp]: "start_sttp_resp_cons dupST"
  by (simp add: start_sttp_resp_cons_def dupST_def split_beta)

lemma start_sttp_resp_cons_dup_x1ST [simp]: "start_sttp_resp_cons dup_x1ST"
  by (simp add: start_sttp_resp_cons_def dup_x1ST_def split_beta)

lemma start_sttp_resp_cons_popST [simp]: "start_sttp_resp_cons (popST n)"
  by (simp add: start_sttp_resp_cons_def popST_def split_beta)

lemma start_sttp_resp_cons_replST [simp]: "start_sttp_resp_cons (replST n tp)"
  by (simp add: start_sttp_resp_cons_def replST_def split_beta)

lemma start_sttp_resp_cons_storeST [simp]: "start_sttp_resp_cons (storeST i tp)"
  by (simp add: start_sttp_resp_cons_def storeST_def split_beta)

lemma start_sttp_resp_cons_compTpExpr [simp]: "start_sttp_resp_cons (compTpExpr jmb G ex)"
  apply (induct ex)
          apply simp+
      apply (simp add: start_sttp_resp_cons_def comb_def pushST_def split_beta) (* LAcc *)
     apply simp+
  done

lemma start_sttp_resp_cons_compTpInit [simp]: "start_sttp_resp_cons (compTpInit jmb lv)"
  by (simp add: compTpInit_def split_beta)


lemma start_sttp_resp_nochangeST [simp]: "start_sttp_resp nochangeST"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_pushST [simp]: "start_sttp_resp (pushST Ts)"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_dupST [simp]: "start_sttp_resp dupST"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_dup_x1ST [simp]: "start_sttp_resp dup_x1ST"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_popST [simp]: "start_sttp_resp (popST n)"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_replST [simp]: "start_sttp_resp (replST n tp)"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_storeST [simp]: "start_sttp_resp (storeST i tp)"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_compTpExpr [simp]: "start_sttp_resp (compTpExpr jmb G ex)"
  by (simp add: start_sttp_resp_def)

lemma start_sttp_resp_compTpExprs [simp]: "start_sttp_resp (compTpExprs jmb G exs)"
  by (induct exs, (simp add: start_sttp_resp_comb)+)

lemma start_sttp_resp_compTpStmt [simp]: "start_sttp_resp (compTpStmt jmb G s)"
  by (induct s, (simp add: start_sttp_resp_comb)+)

lemma start_sttp_resp_compTpInitLvars [simp]: "start_sttp_resp (compTpInitLvars jmb lvars)"
  by (induct lvars, simp+)




  (* ********************************************************************** *)
subsection "length of compExpr/ compTpExprs"
  (* ********************************************************************** *)

lemma length_comb [simp]:  "length (mt_of ((f1 □ f2) sttp)) = 
  length (mt_of (f1 sttp)) + length (mt_of (f2 (sttp_of (f1 sttp))))"
  by (simp add: comb_def split_beta)


lemma length_comb_nil [simp]: "length (mt_of (comb_nil sttp)) = 0"
  by (simp add: comb_nil_def)

lemma length_nochangeST [simp]: "length (mt_of (nochangeST sttp)) = 1"
  by (simp add: nochangeST_def)

lemma length_pushST [simp]: "length (mt_of (pushST Ts sttp)) = 1"
  by (simp add: pushST_def split_beta)

lemma length_dupST [simp]: "length (mt_of (dupST sttp)) = 1"
  by (simp add: dupST_def split_beta)

lemma length_dup_x1ST [simp]: "length (mt_of (dup_x1ST sttp)) = 1"
  by (simp add: dup_x1ST_def split_beta)

lemma length_popST [simp]: "length (mt_of (popST n sttp)) = 1"
  by (simp add: popST_def split_beta)

lemma length_replST [simp]: "length (mt_of (replST n tp sttp)) = 1"
  by (simp add: replST_def split_beta)

lemma length_storeST [simp]: "length (mt_of (storeST i tp sttp)) = 1"
  by (simp add: storeST_def split_beta)


lemma length_compTpExpr_Exprs [rule_format]: "
  (∀sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)))
  ∧ (∀sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))"
  apply (rule compat_expr_expr_list.induct)
            apply (simp_all)[3]
         apply (rename_tac binop a b, case_tac binop)
          apply (auto simp add: pushST_def split_beta)
  done

lemma length_compTpExpr: "length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)"
  by (rule length_compTpExpr_Exprs [THEN conjunct1 [THEN spec]])

lemma length_compTpExprs: "length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)"
  by (rule length_compTpExpr_Exprs [THEN conjunct2 [THEN spec]])

lemma length_compTpStmt [rule_format]: "
  (∀ sttp. (length (mt_of (compTpStmt jmb G s sttp)) = length (compStmt jmb s)))"
  by (rule stmt.induct) (auto simp: length_compTpExpr)

lemma length_compTpInit: "length (mt_of (compTpInit jmb lv sttp)) = length (compInit jmb lv)"
  by (simp add: compTpInit_def compInit_def split_beta)

lemma length_compTpInitLvars [rule_format]: 
  "∀ sttp. length (mt_of (compTpInitLvars jmb lvars sttp)) = length (compInitLvars jmb lvars)"
  by (induct lvars, (simp add: compInitLvars_def length_compTpInit split_beta)+)


  (* ********************************************************************** *)
subsection "Correspondence bytecode - method types"
  (* ********************************************************************** *)

abbreviation (input)
  ST_of :: "state_type ⇒ opstack_type"
  where "ST_of == fst"

abbreviation (input)
  LT_of :: "state_type ⇒ locvars_type"
  where "LT_of == snd"

lemma states_lower:
  "⟦ OK (Some (ST, LT)) ∈ states cG mxs mxr; length ST ≤ mxs⟧
  ⟹ OK (Some (ST, LT)) ∈ states cG (length ST) mxr"
  apply (simp add: states_def JVMType.sl_def)
  apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
                   JType.esl_def)
  apply (simp add: Err.esl_def Err.le_def Listn.le_def)
  apply (simp add: Product.le_def Product.sup_def Err.sup_def)
  apply (simp add: Opt.esl_def Listn.sup_def)
  apply clarify
  apply auto
  done

lemma check_type_lower:
  "⟦ check_type cG mxs mxr (OK (Some (ST, LT))); length ST ≤ mxs⟧
  ⟹check_type cG (length ST) mxr (OK (Some (ST, LT)))"
  by (simp add: check_type_def states_lower)

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

definition bc_mt_corresp :: "
  [bytecode, state_type ⇒ method_type × state_type, state_type, jvm_prog, ty, nat, p_count]
  ⇒ bool" where

  "bc_mt_corresp bc f sttp0 cG rT mxr idx ==
  let (mt, sttp) = f sttp0 in
  (length bc = length mt ∧ 
    ((check_type cG (length (ST_of sttp0)) mxr (OK (Some sttp0))) ⟶
    (∀  mxs. 
     mxs = max_ssize (mt@[Some sttp]) ⟶
     (∀ pc. pc < idx ⟶ 
      wt_instr_altern (bc ! pc) cG rT (mt@[Some sttp]) mxs mxr (length mt + 1) empty_et pc)
     ∧ 
     check_type cG mxs mxr (OK ((mt@[Some sttp]) ! idx)))))"


lemma bc_mt_corresp_comb: "
  ⟦ bc' = (bc1@bc2); l' = (length bc');
  bc_mt_corresp bc1 f1 sttp0 cG rT mxr (length bc1);
  bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
  start_sttp_resp f2⟧
⟹ bc_mt_corresp bc' (f1 □ f2) sttp0 cG rT mxr l'"
  apply (subgoal_tac "∃mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
   apply (subgoal_tac "∃mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)

    (* unfold start_sttp_resp and make case distinction *)
    apply (simp only: start_sttp_resp_def)
    apply (erule disjE)
     (* case f2 = comb_nil *)
     apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)
     apply (erule conjE)+
     apply (intro strip)
     apply simp

    (* case start_sttp_resp_cons f2 *)
    apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def del: all_simps)
    apply (intro strip)
    apply (erule conjE)+
    apply (drule mp, assumption)
    apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
     apply (erule conjE)+
     apply (drule mp, assumption)
     apply (erule conjE)+

     apply (rule conjI)
      (* show wt_instr  … *)

      apply (drule_tac x=sttp1 in spec, simp)
      apply (erule exE)
      apply (intro strip)
      apply (case_tac "pc < length mt1")

       (* case pc < length mt1 *)
       apply (drule spec, drule mp, simp)
       apply simp
       apply (rule_tac mt="mt1 @ [Some sttp1]" in wt_instr_prefix)
              apply assumption+ apply (rule HOL.refl)
            apply (simp (no_asm_simp))
           apply (simp (no_asm_simp) add: max_ssize_def)
           apply (simp add: max_of_list_def ac_simps)
          apply arith
         apply (simp (no_asm_simp))+

      (* case pc ≥ length mt1 *)
      apply (rule_tac bc=bc2 and mt=mt2 and bc_post="[]" and mt_post="[Some sttp2]"
              and mxr=mxr
              in wt_instr_offset)
              apply simp
             apply (simp (no_asm_simp))+
        apply simp
       apply (simp add: max_ssize_def) apply (simp (no_asm_simp))

     (* show check_type … *)
     apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
      apply (simp only:)
      apply (rule check_type_mono) apply assumption
      apply (simp (no_asm_simp) add: max_ssize_def ac_simps)
     apply (simp add: nth_append)

    apply (erule conjE)+
    apply (case_tac sttp1)
    apply (simp add: check_type_def)
    apply (rule states_lower, assumption)
    apply (simp (no_asm_simp) add: max_ssize_def)
    apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
   apply (simp (no_asm_simp))+
  done


lemma bc_mt_corresp_zero [simp]:
  "⟦ length (mt_of (f sttp)) = length bc; start_sttp_resp f⟧
  ⟹ bc_mt_corresp bc f sttp cG rT mxr 0"
  apply (simp add: bc_mt_corresp_def start_sttp_resp_def split_beta)
  apply (erule disjE)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
  apply (intro strip)
  apply (simp add: start_sttp_resp_cons_def split_beta)
  apply (drule_tac x=sttp in spec, erule exE)
  apply simp
  apply (rule check_type_mono, assumption)
  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
  done

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


definition mt_sttp_flatten :: "method_type × state_type ⇒ method_type" where
  "mt_sttp_flatten mt_sttp == (mt_of mt_sttp) @ [Some (sttp_of mt_sttp)]"


lemma mt_sttp_flatten_length [simp]: "n = (length (mt_of (f sttp)))
  ⟹ (mt_sttp_flatten (f sttp)) ! n = Some (sttp_of (f sttp))"
  by (simp add: mt_sttp_flatten_def)

lemma mt_sttp_flatten_comb: "(mt_sttp_flatten ((f1 □ f2) sttp)) = 
  (mt_of (f1 sttp)) @ (mt_sttp_flatten (f2 (sttp_of (f1 sttp))))"
  by (simp add: mt_sttp_flatten_def comb_def split_beta)

lemma mt_sttp_flatten_comb_length [simp]: "⟦ n1 = length (mt_of (f1 sttp)); n1 ≤ n ⟧
  ⟹ (mt_sttp_flatten ((f1 □ f2) sttp) ! n) = (mt_sttp_flatten (f2 (sttp_of (f1 sttp))) ! (n - n1))"
  by (simp add: mt_sttp_flatten_comb nth_append)

lemma mt_sttp_flatten_comb_zero [simp]:
  "start_sttp_resp f ⟹ (mt_sttp_flatten (f sttp)) ! 0 = Some sttp"
  apply (simp only: start_sttp_resp_def)
  apply (erule disjE)
   apply (simp add: comb_nil_def mt_sttp_flatten_def)
  apply (simp add: start_sttp_resp_cons_def mt_sttp_flatten_def split_beta)
  apply (drule_tac x=sttp in spec)
  apply (erule exE)
  apply simp
  done


(* move into prelude -- compare with nat_int_length *)
lemma int_outside_right: "0 ≤ (m::int) ⟹ m + (int n) = int ((nat m) + n)"
  by simp

lemma int_outside_left: "0 ≤ (m::int) ⟹ (int n) + m = int (n + (nat m))"
  by simp




  (* ********************************************************************** *)
  (* bc_mt_corresp for individual instructions                              *)
  (* ---------------------------------------------------------------------- *)

lemma less_Suc [simp] : "n ≤ k ⟹ (k < Suc n) = (k = n)"
  by arith

lemmas check_type_simps = check_type_def states_def JVMType.sl_def
   Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
  JType.esl_def Err.esl_def Err.le_def Listn.le_def Product.le_def Product.sup_def Err.sup_def
  Opt.esl_def Listn.sup_def


lemma check_type_push: 
  "⟦ is_class cG cname; check_type cG (length ST) mxr (OK (Some (ST, LT))) ⟧
  ⟹ check_type cG (Suc (length ST)) mxr (OK (Some (Class cname # ST, LT)))"
  apply (simp add: check_type_simps)
  apply clarify
  apply (rule_tac x="Suc (length ST)" in exI)
  apply simp+
  done

lemma bc_mt_corresp_New: "⟦is_class cG cname ⟧
  ⟹ bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
                   max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
  apply (intro strip)
  apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
  apply (simp add: check_type_push)
  done

lemma bc_mt_corresp_Pop: "
  bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: max_ssize_def ssize_sto_def max_of_list_def)
  apply (simp add: check_type_simps max.absorb1)
  apply clarify
  apply (rule_tac x="(length ST)" in exI)
  apply simp
  done

lemma bc_mt_corresp_Checkcast: "⟦ is_class cG cname; sttp = (ST, LT); 
  (∃rT STo. ST = RefT rT # STo) ⟧
  ⟹ bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
  apply (erule exE)+
  apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (simp add: check_type_simps)
  apply clarify
  apply (rule_tac x="Suc (length STo)" in exI)
  apply simp
  done


lemma bc_mt_corresp_LitPush: "⟦ typeof (λv. None) val = Some T ⟧
  ⟹ bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
  apply (subgoal_tac "∃ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
                    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
    apply (rule check_type_mono, assumption, simp)
   apply (simp add: check_type_simps)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
   apply simp
   apply (drule sym)
   apply (case_tac val)
       apply simp+
  done


lemma bc_mt_corresp_LitPush_CT:
  "⟦ typeof (λv. None) val = Some T ∧ cG ⊢ T ≼ T'; is_type cG T' ⟧
  ⟹ bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
  apply (subgoal_tac "∃ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def max_ssize_def
                    max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
    apply (rule check_type_mono, assumption, simp)
   apply (simp add: check_type_simps)
   apply (simp add: sup_state_Cons)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
   apply simp
  apply simp
  done

declare not_Err_eq [iff del]

lemma bc_mt_corresp_Load: "⟦ i < length LT; LT ! i ≠ Err; mxr = length LT ⟧
  ⟹ bc_mt_corresp [Load i] 
         (λ(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def max_ssize_def max_of_list_def
                   ssize_sto_def eff_def norm_eff_def max.absorb2)
  apply (intro strip)
  apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
  apply (simp add: check_type_simps)
  apply clarify
  apply (rule_tac x="Suc (length ST)" in exI)
  apply (simp (no_asm_simp))
  apply (simp only: err_def)
  apply (frule listE_nth_in)
   apply assumption
  apply (subgoal_tac "LT ! i ∈ {x. ∃y∈types cG. x = OK y}")
   apply (drule CollectD)
   apply (erule bexE)
   apply (simp (no_asm_simp))
   apply blast
  apply blast
  done


lemma bc_mt_corresp_Store_init:
  "i < length LT ⟹ bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: max_ssize_def  max_of_list_def)
  apply (simp add: ssize_sto_def)
  apply (intro strip)
  apply (simp add: check_type_simps max.absorb1)
  apply clarify
  apply (rule conjI)
   apply (rule_tac x="(length ST)" in exI)
   apply simp+
  done


lemma bc_mt_corresp_Store:
  "⟦ i < length LT; cG  ⊢  LT[i := OK T] <=l LT ⟧
  ⟹ bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: sup_state_conv)
  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (intro strip)
  apply (simp add: check_type_simps max.absorb1)
  apply clarify
  apply (rule_tac x="(length ST)" in exI)
  apply simp
  done


lemma bc_mt_corresp_Dup: "
  bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
                   max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
  apply (intro strip)
  apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
  apply (simp add: check_type_simps)
  apply clarify
  apply (rule_tac x="Suc (Suc (length ST))" in exI)
  apply simp
  done

lemma bc_mt_corresp_Dup_x1: "
  bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
  apply (intro strip)
  apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
  apply (simp add: check_type_simps)
  apply clarify
  apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
  apply simp+
  done



lemma bc_mt_corresp_IAdd: "
  bc_mt_corresp [IAdd] (replST 2 (PrimT Integer)) 
         (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (simp add: check_type_simps max.absorb1)
  apply clarify
  apply (rule_tac x="Suc (length ST)" in exI)
  apply simp
  done

lemma bc_mt_corresp_Getfield: "⟦ wf_prog wf_mb G; 
  field (G, C) vname = Some (cname, T);  is_class G C ⟧
  ⟹ bc_mt_corresp [Getfield vname cname] 
        (replST (Suc 0) (snd (the (field (G, cname) vname))))
        (Class C # ST, LT) (comp G) rT mxr (Suc 0)"
  apply (frule wf_prog_ws_prog [THEN wf_subcls1])
  apply (frule field_in_fd, assumption+)
  apply (frule widen_field, assumption+)
  apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (intro strip)
  apply (simp add: check_type_simps)
  apply clarify
  apply (rule_tac x="Suc (length ST)" in exI)
  apply simp+
  apply (simp only: comp_is_type)
  apply (rule_tac C=cname in fields_is_type)
    apply (simp add: TypeRel.field_def)
    apply (drule JBasis.table_of_remap_SomeD)+
    apply assumption+
   apply (erule wf_prog_ws_prog)
  apply assumption
  done

lemma bc_mt_corresp_Putfield: "⟦ wf_prog wf_mb G; 
  field (G, C) vname = Some (cname, Ta); G ⊢ T ≼ Ta; is_class G C ⟧
  ⟹ bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT)
           (comp G) rT mxr (Suc 0)"
  apply (frule wf_prog_ws_prog [THEN wf_subcls1])
  apply (frule field_in_fd, assumption+)
  apply (frule widen_field, assumption+)
  apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)

  apply (intro strip)
  apply (simp add: check_type_simps max.absorb1)
  apply clarify
  apply (rule_tac x="Suc (length ST)" in exI)
  apply simp+
  done



lemma Call_app:
  "⟦ wf_prog wf_mb G; is_class G cname;
     STs = rev pTsa @ Class cname # ST;
     max_spec G cname (mname, pTsa) = {((md, T), pTs')} ⟧
  ⟹ app (Invoke cname mname pTs') (comp G) (length (T # ST)) rT 0 empty_et (Some (STs, LTs))"
  apply (subgoal_tac "(∃mD' rT' comp_b. 
                        method (comp G, cname) (mname, pTs') = Some (mD', rT', comp_b))")
   apply (simp add: comp_is_class)
   apply (rule_tac x=pTsa in exI)
   apply (rule_tac x="Class cname" in exI)
   apply (simp add: max_spec_preserves_length comp_is_class)
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (simp add: split_paired_all comp_widen list_all2_iff)
  apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  apply (rule exI)+
  apply (simp add: wf_prog_ws_prog [THEN comp_method])
  done


lemma bc_mt_corresp_Invoke:
  "⟦ wf_prog wf_mb G; 
  max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
  is_class G cname ⟧
 ⟹ bc_mt_corresp [Invoke cname mname fpTs] (replST (Suc (length pTsa)) T)
           (rev pTsa @ Class cname # ST, LT) (comp G) rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def wt_instr_altern_def eff_def norm_eff_def)
  apply (simp add: replST_def del: appInvoke)
  apply (intro strip)
  apply (rule conjI)

   ― ‹app›
   apply (rule Call_app [THEN app_mono_mxs])
       apply assumption+
     apply (rule HOL.refl)
    apply assumption
   apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)

  ― ‹‹<=s››
  apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
  apply (simp add: wf_prog_ws_prog [THEN comp_method])
  apply (simp add: max_spec_preserves_length [symmetric])

  ― ‹‹check_type››
  apply (simp add: max_ssize_def ssize_sto_def)
  apply (simp add: max_of_list_def)
  apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
   apply simp
   apply (simp add: check_type_simps)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
   apply simp+
   apply (simp only: comp_is_type)
   apply (frule method_wf_mdecl) apply assumption apply assumption
   apply (simp add: wf_mdecl_def wf_mhead_def)
  apply (simp)
  done


lemma wt_instr_Ifcmpeq: "⟦Suc pc < max_pc; 
  0 ≤ (int pc + i);  nat (int pc + i) < max_pc;
  (mt_sttp_flatten f ! pc = Some (ts#ts'#ST,LT)) ∧ 
  ((∃p. ts = PrimT p ∧ ts' = PrimT p) ∨ (∃r r'. ts = RefT r ∧ ts' = RefT r'));
  mt_sttp_flatten f ! Suc pc = Some (ST,LT);
  mt_sttp_flatten f ! nat (int pc + i) = Some (ST,LT);
  check_type (TranslComp.comp G) mxs mxr (OK (Some (ts # ts' # ST, LT))) ⟧
    ⟹  wt_instr_altern (Ifcmpeq i) (comp G) rT  (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
  by (simp  add: wt_instr_altern_def eff_def norm_eff_def)


lemma wt_instr_Goto: "⟦ 0 ≤ (int pc + i); nat (int pc + i) < max_pc;
  mt_sttp_flatten f ! nat (int pc + i) = (mt_sttp_flatten f ! pc);
  check_type (TranslComp.comp G) mxs mxr (OK (mt_sttp_flatten f ! pc)) ⟧
  ⟹ wt_instr_altern (Goto i) (comp G) rT  (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
  apply (case_tac "(mt_sttp_flatten f ! pc)")
   apply (simp  add: wt_instr_altern_def eff_def norm_eff_def app_def xcpt_app_def)+
  done




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



lemma bc_mt_corresp_comb_inside: "
  ⟦ 
  bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
  bc' = (bc1@bc2@bc3); f'= (f1 □ f2 □ f3); 
  l1 = (length bc1); l12 = (length (bc1@bc2));
  bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
  length bc1 = length (mt_of (f1 sttp0));
  start_sttp_resp f2; start_sttp_resp f3⟧
⟹ bc_mt_corresp bc' f' sttp0 cG rT mxr l12"
  apply (subgoal_tac "∃ mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
   apply (subgoal_tac "∃ mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
    apply (subgoal_tac "∃ mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)

     (* unfold start_sttp_resp and make case distinction *)
     apply (simp only: start_sttp_resp_def)
     apply (erule_tac Q="start_sttp_resp_cons f2" in disjE)
      (* case f2 = comb_nil *)
      apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)

     (* case start_sttp_resp_cons f2 *)
     apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def)
     apply (drule_tac x=sttp1 in spec, simp, erule exE)
     apply (intro strip, (erule conjE)+)


     (* get rid of all check_type info *)
     apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
      apply (subgoal_tac "check_type cG (max_ssize (mt2 @ [Some sttp2])) mxr (OK (Some sttp2))")
       apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr
                                         (OK ((mt2 @ mt3 @ [Some sttp3]) ! length mt2))")
        apply simp



        apply (intro strip, (erule conjE)+)
        apply (case_tac "pc < length mt1")

         (* case pc < length mt1 *)
         apply (drule spec, drule mp, assumption)
         apply assumption

        (* case pc ≥ length mt1 *)
        (* case distinction on start_sttp_resp f3 *)
        apply (erule_tac P="f3 = comb_nil" in disjE)

         (* case f3 = comb_nil *)
         apply (subgoal_tac "mt3 = [] ∧ sttp2 = sttp3")  apply (erule conjE)+
          apply (subgoal_tac "bc3=[]")

           apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
                       and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]"
                       and mxs="(max_ssize (mt2 @ [(Some sttp2)]))"
                       and max_pc="(Suc (length mt2))"
                        in wt_instr_offset)
                   apply simp
                  apply (rule HOL.refl)+
                 apply (simp (no_asm_simp))+

            apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
            apply (rule max_of_list_sublist)
            apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast
           apply (simp (no_asm_simp))
          apply simp                    (* subgoal bc3 = [] *)
         apply (simp add: comb_nil_def) (* subgoal mt3 = [] ∧ sttp2 = sttp3 *)

        (* case start_sttp_resp_cons f3 *)
        apply (subgoal_tac "∃mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
         apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
                     and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]"
                     and mxs="(max_ssize (mt2 @ [Some sttp2]))"
                     and max_pc="(Suc (length mt2))"
                      in wt_instr_offset)
                 apply (intro strip)
                 apply (rule_tac bc=bc2 and mt="(mt2 @ [Some sttp2])"
                             and mxs="(max_ssize (mt2 @ [Some sttp2]))"
                             and max_pc="(Suc (length mt2))"
                              in wt_instr_prefix)

                        (* preconditions of  wt_instr_prefix *)
                        apply simp
                       apply (rule HOL.refl)
                      apply (simp (no_asm_simp))+
                   apply simp+
          (* (some) preconditions of  wt_instr_offset *)
          apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
          apply (rule max_of_list_sublist)
          apply (simp (no_asm_simp) only: set_append list.set list.map)
          apply blast
         apply (simp (no_asm_simp))

        apply (drule_tac x=sttp2 in spec, simp) (* subgoal ∃mt3_rest. … *)

       (* subgoals check_type*)
       (* … ! length mt2 *)
       apply simp

       apply (erule_tac P="f3 = comb_nil" in disjE)

        (* -- case f3 = comb_nil *)
        apply (subgoal_tac "mt3 = [] ∧ sttp2 = sttp3")  apply (erule conjE)+
         apply simp
         apply (rule check_type_mono, assumption)
         apply (simp only: max_ssize_def)
         apply (rule max_of_list_sublist)
         apply (simp (no_asm_simp))
         apply blast
        apply simp                    (* subgoal bc3 = [] *)
        apply (simp add: comb_nil_def) (* subgoal mt3 = [] ∧ sttp2 = sttp3 *)


       (* -- case start_sttp_resp_cons f3 *)
       apply (subgoal_tac "∃mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
        apply (simp (no_asm_simp) add: nth_append)
        apply (erule conjE)+
        apply (rule check_type_mono, assumption)
        apply (simp only: max_ssize_def)
        apply (rule max_of_list_sublist)
        apply (simp (no_asm_simp))
        apply blast
       apply (drule_tac x=sttp2 in spec, simp) (* subgoal ∃mt3_rest. … *)


      (* subgoal check_type … Some sttp2 *)
      apply (simp add: nth_append)

     (* subgoal check_type … Some sttp1 *)
     apply (simp add: nth_append)
     apply (erule conjE)+
     apply (case_tac "sttp1", simp)
     apply (rule check_type_lower, assumption)
     apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
     apply (simp (no_asm_simp) add: max_of_list_def)

    (* subgoals ∃ ... *)
    apply (rule surj_pair)+
  done


  (* ******************** *)
definition contracting :: "(state_type ⇒ method_type × state_type) ⇒ bool" where
  "contracting f == (∀ ST LT. 
                    let (ST', LT') = sttp_of (f (ST, LT)) 
                    in (length ST' ≤ length ST ∧ set ST' ⊆ set ST  ∧
                        length LT' = length LT ∧ set LT' ⊆ set LT))"


  (* ### possibly move into HOL *)
lemma set_drop_Suc [rule_format]: "∀xs. set (drop (Suc n) xs) ⊆ set (drop n xs)"
  apply (induct n)
   apply simp
   apply (intro strip)
   apply (rule list.induct)
    apply simp
   apply simp
   apply blast
  apply (intro strip)
  apply (rule_tac P="λ xs. set (drop (Suc (Suc n)) xs) ⊆ set (drop (Suc n) xs)" in list.induct)
   apply simp+
  done

lemma set_drop_le [rule_format,simp]: "∀n xs. n ≤ m ⟶ set (drop m xs) ⊆ set (drop n xs)"
  apply (induct m)
   apply simp
  apply (intro strip)
  apply (subgoal_tac "n ≤ m ∨ n = Suc m")
   apply (erule disjE)
    apply (frule_tac x=n in spec, drule_tac x=xs in spec, drule mp, assumption)
    apply (rule set_drop_Suc [THEN subset_trans], assumption)
   apply auto
  done

declare set_drop_subset [simp]

lemma contracting_popST [simp]: "contracting (popST n)"
  by (simp add: contracting_def popST_def)

lemma contracting_nochangeST [simp]: "contracting nochangeST"
  by (simp add: contracting_def nochangeST_def)


lemma check_type_contracting: "⟦ check_type cG mxs mxr (OK (Some sttp)); contracting f⟧ 
  ⟹ check_type cG mxs mxr (OK (Some (sttp_of (f sttp))))"
  apply (subgoal_tac "∃ ST LT. sttp = (ST, LT)", (erule exE)+)
   apply (simp add: check_type_simps contracting_def)
   apply clarify
   apply (drule_tac x=ST in spec, drule_tac x=LT in spec)
   apply (case_tac "(sttp_of (f (ST, LT)))")
   apply simp
   apply (erule conjE)+

   apply (drule listE_set)+
   apply (rule conjI)
    apply (rule_tac x="length a" in exI)
    apply simp
    apply (rule listI)
     apply simp
    apply blast
   apply (rule listI)
    apply simp
   apply blast
  apply auto
  done

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


lemma bc_mt_corresp_comb_wt_instr: "
  ⟦ bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
  bc' = (bc1@[inst]@bc3); f'= (f1 □ f2 □ f3); 
  l1 = (length bc1); 
  length bc1 = length (mt_of (f1 sttp0));
  length (mt_of (f2 (sttp_of (f1 sttp0)))) = 1;
  start_sttp_resp_cons f1; start_sttp_resp_cons f2; start_sttp_resp f3;

  check_type cG (max_ssize (mt_sttp_flatten (f' sttp0))) mxr
             (OK ((mt_sttp_flatten (f' sttp0)) ! (length bc1)))
  ⟶
  wt_instr_altern inst cG rT 
      (mt_sttp_flatten (f' sttp0)) 
      (max_ssize (mt_sttp_flatten (f' sttp0)))
      mxr
      (Suc (length bc'))
      empty_et
      (length bc1);
  contracting f2
 ⟧
⟹ bc_mt_corresp bc' f' sttp0 cG rT mxr (length (bc1@[inst]))"
  apply (subgoal_tac "∃ mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
   apply (subgoal_tac "∃ mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
    apply (subgoal_tac "∃ mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)

     apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def
                      mt_sttp_flatten_def)

     apply (intro strip, (erule conjE)+)
     apply (drule mp, assumption)+
     apply (erule conjE)+
     apply (drule mp, assumption)
     apply (rule conjI)

      (* wt_instr … *)
      apply (intro strip)
      apply (case_tac "pc < length mt1")

       (* case pc < length mt1 *)
       apply (drule spec, drule mp, assumption)
       apply assumption

      (* case pc ≥ length mt1 *)
      apply (subgoal_tac "pc = length mt1") prefer 2 apply arith
      apply (simp only:)
      apply (simp add: nth_append mt_sttp_flatten_def)


     (* check_type … *)
     apply (simp add: start_sttp_resp_def)
     apply (drule_tac x="sttp0" in spec, simp, erule exE)
     apply (drule_tac x="sttp1" in spec, simp, erule exE)

     apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr
                                       (OK (Some (sttp_of (f2 sttp1))))")

      apply (simp only:)

      apply (erule disjE)
       (* case f3 = comb_nil *)
       apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! Suc (length mt1)) = (Some (snd (f2 sttp1)))")
        apply (subgoal_tac "mt3 = [] ∧ sttp2 = sttp3")
         apply (erule conjE)+
         apply (simp add: nth_append)
        apply (simp add: comb_nil_def) (* subgoal mt3 = [] ∧ sttp2 = sttp3 *)
       apply (simp add: nth_append comb_nil_def) (* subgoal … ! Suc (length mt1) *)

      (* case start_sttp_resp_cons f3 *)
      apply (simp add: start_sttp_resp_cons_def)
      apply (drule_tac x="sttp2" in spec, simp, erule exE)
      apply (simp  add: nth_append)

     (* subgoal check_type *)
     apply (rule check_type_contracting)
      apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! length mt1) = (Some sttp1)")
       apply (simp add: nth_append)
      apply (simp add: nth_append)

     apply assumption

    (* subgoals *)
    apply (rule surj_pair)+
  done


lemma compTpExpr_LT_ST_rewr [simp]:
  "⟦ wf_java_prog G; wf_java_mdecl G C ((mn, pTs), rT, (pns, lvars, blk, res));
     local_env G C (mn, pTs) pns lvars ⊢ ex :: T;
     is_inited_LT C pTs lvars LT⟧
  ⟹ sttp_of (compTpExpr (pns, lvars, blk, res) G ex (ST, LT)) = (T # ST, LT)"
  by (rule compTpExpr_LT_ST) auto


lemma wt_method_compTpExpr_Exprs_corresp: "
  ⟦ jmb = (pns,lvars,blk,res); 
  wf_prog wf_java_mdecl G;
  wf_java_mdecl G C ((mn, pTs), rT, jmb);
  E = (local_env G C (mn, pTs) pns lvars)⟧ 
⟹ 
 (∀ ST LT T bc' f'.
  E ⊢ ex :: T ⟶  
  (is_inited_LT C pTs lvars LT) ⟶
  bc' = (compExpr jmb ex) ⟶
  f' = (compTpExpr jmb G ex)
  ⟶ bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))
 ∧
 (∀ ST LT Ts.
  E ⊢ exs [::] Ts ⟶
  (is_inited_LT C pTs lvars LT) 
  ⟶ bc_mt_corresp (compExprs jmb exs) (compTpExprs jmb G exs) (ST, LT) (comp G) rT (length LT) (length (compExprs jmb exs)))"
  apply (rule compat_expr_expr_list.induct)

            (* expresssions *)

            (* NewC *)
            apply (intro allI impI)
            apply (simp only:)
            apply (drule NewC_invers)
            apply (simp (no_asm_use))
            apply (rule bc_mt_corresp_New)
            apply (simp add: comp_is_class)

           (* Cast *)
           apply (intro allI impI)
           apply (simp only:)
           apply (drule Cast_invers)
           apply clarify
           apply (simp (no_asm_use))
           apply (rule bc_mt_corresp_comb)
               apply (rule HOL.refl, simp (no_asm_simp), blast)
            apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast)
              apply (simp add: comp_is_class)
             apply (simp only: compTpExpr_LT_ST)
            apply (drule cast_RefT)
            apply blast
           apply (simp add: start_sttp_resp_def)

          (* Lit *)
          apply (intro allI impI)
          apply (simp only:)
          apply (drule Lit_invers)
          apply simp
          apply (rule bc_mt_corresp_LitPush)
          apply assumption


         (* BinOp *)

         apply (intro allI impI)
         apply (simp (no_asm_simp) only:)
         apply (drule BinOp_invers, erule exE, (erule conjE)+)
         apply (rename_tac binop expr1 expr2 ST LT T bc' f' Ta, case_tac binop)
          apply (simp (no_asm_simp))

          (* case Eq *)
          apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
           prefer 2
           apply (rule bc_mt_corresp_zero)
            apply (simp add: length_compTpExpr)
           apply (simp (no_asm_simp))

          apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "compExpr jmb expr1"
                       and ?f1.0=comb_nil and ?f2.0 = "compTpExpr jmb G expr1"
                        in bc_mt_corresp_comb_inside)
                  apply (simp (no_asm_simp))+
              apply blast
             apply (simp (no_asm_simp) add: length_compTpExpr)+

          apply (drule_tac ?bc2.0 = "compExpr jmb expr2" and ?f2.0 = "compTpExpr jmb G expr2"
                        in bc_mt_corresp_comb_inside)
                  apply (simp (no_asm_simp))+
              apply (simp only: compTpExpr_LT_ST)
             apply (simp (no_asm_simp) add: length_compTpExpr)
            apply (simp (no_asm_simp))
           apply (simp (no_asm_simp))

          apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2"
                        and inst = "Ifcmpeq 3" and ?bc3.0 = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
                        and ?f1.0="compTpExpr jmb G expr1 □ compTpExpr jmb G expr2"
                        and ?f2.0="popST 2" and ?f3.0="pushST [PrimT Boolean] □ popST 1 □ pushST [PrimT Boolean]"
                         in bc_mt_corresp_comb_wt_instr)
                    apply (simp (no_asm_simp) add: length_compTpExpr)+

            (* wt_instr *)
            apply (intro strip)
            apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr eff_def)
            apply (simp (no_asm_simp) add: norm_eff_def)
            apply (simp (no_asm_simp) only: int_outside_left nat_int)
            apply (simp (no_asm_simp) add: length_compTpExpr)
            apply (simp only: compTpExpr_LT_ST)+
            apply (simp add: eff_def norm_eff_def popST_def pushST_def mt_sttp_flatten_def)
            apply (case_tac Ta)
             apply (simp (no_asm_simp))
            apply (simp (no_asm_simp))
           apply (rule contracting_popST)                (* contracting (popST 2)  *)

          apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
                       and ?bc2.0 = "[LitPush (Bool False)]"
                       and ?bc3.0 = "[Goto 2, LitPush (Bool True)]"
                       and ?f1.0 = "compTpExpr jmb G expr1 □ compTpExpr jmb G expr2 □ popST 2"
                       and ?f2.0 = "pushST [PrimT Boolean]"
                       and ?f3.0 = "popST (Suc 0) □ pushST [PrimT Boolean]"
                        in bc_mt_corresp_comb_inside)
                  apply (simp (no_asm_simp))+
              apply simp
              apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
             apply (simp (no_asm_simp) add: length_compTpExpr)
            apply (simp (no_asm_simp))
           apply (simp (no_asm_simp) add: start_sttp_resp_def)


          apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]"
                       and inst = "Goto 2" and ?bc3.0 = "[LitPush (Bool True)]"
                       and ?f1.0="compTpExpr jmb G expr1 □ compTpExpr jmb G expr2 □ popST 2 □ pushST [PrimT Boolean]"
                       and ?f2.0="popST 1" and ?f3.0="pushST [PrimT Boolean]"
                        in bc_mt_corresp_comb_wt_instr)
                    apply (simp (no_asm_simp) add: length_compTpExpr)+

            (* wt_instr *)
            apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr)
            apply (simp (no_asm_simp) add: eff_def norm_eff_def)
            apply (simp (no_asm_simp) only: int_outside_right nat_int)
            apply (simp (no_asm_simp) add: length_compTpExpr)
            apply (simp only: compTpExpr_LT_ST)+
            apply (simp add: eff_def norm_eff_def popST_def pushST_def)
           apply (rule contracting_popST)                (* contracting (popST 1) *)

          apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False), Goto 2]"
                       and ?bc2.0 = "[LitPush (Bool True)]"
                       and ?bc3.0 = "[]"
                       and ?f1.0 = "compTpExpr jmb G expr1 □ compTpExpr jmb G expr2 □ popST 2 □
                                    pushST [PrimT Boolean] □ popST (Suc 0)"
                       and ?f2.0 = "pushST [PrimT Boolean]"
                       and ?f3.0 = "comb_nil"
                        in bc_mt_corresp_comb_inside)
                  apply (simp (no_asm_simp))+
              apply simp
              apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
              apply (simp (no_asm_simp))
             apply (simp (no_asm_simp) add: length_compTpExpr)
            apply (simp (no_asm_simp) add: start_sttp_resp_def)
           apply (simp (no_asm_simp))

          apply simp

         (* case Add *)
         apply simp
         apply (rule bc_mt_corresp_comb)
             apply (rule HOL.refl)
            apply simp
           apply blast
          apply (rule bc_mt_corresp_comb, rule HOL.refl)
             apply (simp only: compTpExpr_LT_ST)
            apply (simp only: compTpExpr_LT_ST)
            apply blast

           apply (simp only: compTpExpr_LT_ST)
           apply simp
           apply (rule bc_mt_corresp_IAdd)
          apply (simp (no_asm_simp) add: start_sttp_resp_def)
         apply (simp (no_asm_simp) add: start_sttp_resp_def)


        (* LAcc *)
        apply (intro allI impI)
        apply (simp only:)
        apply (drule LAcc_invers)
        apply (frule wf_java_mdecl_length_pTs_pns)
        apply clarify
        apply (simp add: is_inited_LT_def)
        apply (rule bc_mt_corresp_Load)
          apply (rule index_in_bounds)
           apply simp
          apply assumption
         apply (rule inited_LT_at_index_no_err)
         apply (rule index_in_bounds)
          apply simp
         apply assumption
        apply (rule HOL.refl)


       (* LAss *)
       apply (intro allI impI)
       apply (simp only:)
       apply (drule LAss_invers, erule exE, (erule conjE)+)
       apply (drule LAcc_invers)
       apply (frule wf_java_mdecl_disjoint_varnames, simp add: disjoint_varnames_def)
       apply (frule wf_java_mdecl_length_pTs_pns)
       apply clarify
       apply (simp (no_asm_use))
       apply (rule bc_mt_corresp_comb)
           apply (rule HOL.refl, simp (no_asm_simp), blast)
        apply (rename_tac vname x2 ST LT T Ta)
        apply (rule_tac ?bc1.0="[Dup]" and ?bc2.0="[Store (index (pns, lvars, blk, res) vname)]"
                    and ?f1.0="dupST" and ?f2.0="popST (Suc 0)"
                     in bc_mt_corresp_comb)
            apply (simp (no_asm_simp))+
          apply (rule bc_mt_corresp_Dup)
         apply (simp only: compTpExpr_LT_ST)
         apply (simp add: dupST_def is_inited_LT_def)
         apply (rule bc_mt_corresp_Store)
          apply (rule index_in_bounds)
           apply simp
          apply assumption
         apply (rule sup_loc_update_index, assumption+)
            apply simp
           apply assumption+
        apply (simp add: start_sttp_resp_def)
       apply (simp add: start_sttp_resp_def)

      (* FAcc *)
      apply (intro allI impI)
      apply (simp only:)
      apply (drule FAcc_invers)
      apply clarify
      apply (simp (no_asm_use))
      apply (rule bc_mt_corresp_comb)
          apply (rule HOL.refl, simp (no_asm_simp), blast)
       apply (simp (no_asm_simp))
       apply (rule bc_mt_corresp_Getfield)
         apply assumption+
       apply (fast intro: wt_class_expr_is_class)
      apply (simp (no_asm_simp) add: start_sttp_resp_def)


     (* FAss *)
     apply (intro allI impI)
     apply (simp only:)
     apply (drule FAss_invers, erule exE, (erule conjE)+)
     apply (drule FAcc_invers)
     apply clarify
     apply (simp (no_asm_use))
     apply (rule bc_mt_corresp_comb)
         apply (rule HOL.refl)
        apply simp
       apply blast
      apply (simp only: compTpExpr_LT_ST)
      apply (rule bc_mt_corresp_comb, (rule HOL.refl)+)
        apply blast
       apply (simp only: compTpExpr_LT_ST)
       apply (rename_tac cname x2 vname x4 ST LT T Ta Ca)
       apply (rule_tac ?bc1.0="[Dup_x1]" and ?bc2.0="[Putfield vname cname]" in bc_mt_corresp_comb)
           apply (simp (no_asm_simp))+
         apply (rule bc_mt_corresp_Dup_x1)
        apply (simp (no_asm_simp) add: dup_x1ST_def)
        apply (rule bc_mt_corresp_Putfield, assumption+)
        apply (fast intro: wt_class_expr_is_class)
       apply (simp (no_asm_simp) add: start_sttp_resp_def)
      apply (simp (no_asm_simp) add: start_sttp_resp_def)
     apply (simp (no_asm_simp) add: start_sttp_resp_def)

    (* Call *)
    apply (intro allI impI)
    apply (simp only:)
    apply (drule Call_invers)
    apply clarify
    apply (simp (no_asm_use))
    apply (rule bc_mt_corresp_comb)
        apply (rule HOL.refl)
       apply simp
      apply blast
     apply (simp only: compTpExpr_LT_ST)
     apply (rule bc_mt_corresp_comb, (rule HOL.refl)+)
       apply blast
      apply (simp only: compTpExprs_LT_ST)
      apply (simp (no_asm_simp))
      apply (rule bc_mt_corresp_Invoke)
        apply assumption+
      apply (fast intro: wt_class_expr_is_class)
     apply (simp (no_asm_simp) add: start_sttp_resp_def)
    apply (rule start_sttp_resp_comb)
     apply (simp (no_asm_simp))
    apply (simp (no_asm_simp) add: start_sttp_resp_def)


   (* expression lists *)
   (* nil *)

   apply (intro allI impI)
   apply (drule Nil_invers)
   apply simp

  (* cons *)

  apply (intro allI impI)
  apply (drule Cons_invers, (erule exE)+, (erule conjE)+)
  apply clarify
  apply (simp (no_asm_use))
  apply (rule bc_mt_corresp_comb)
      apply (rule HOL.refl)
     apply simp
    apply blast
   apply (simp only: compTpExpr_LT_ST)
   apply blast
  apply simp

done


lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = 
  wt_method_compTpExpr_Exprs_corresp [THEN conjunct1]


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




lemma wt_method_compTpStmt_corresp [rule_format (no_asm)]: "
  ⟦ jmb = (pns,lvars,blk,res); 
  wf_prog wf_java_mdecl G;
  wf_java_mdecl G C ((mn, pTs), rT, jmb);
  E = (local_env G C (mn, pTs) pns lvars)⟧ 
⟹ 
 (∀ ST LT T bc' f'.
  E ⊢ s√ ⟶
  (is_inited_LT C pTs lvars LT) ⟶
  bc' = (compStmt jmb s) ⟶
  f' = (compTpStmt jmb G s)
  ⟶ bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))"

  apply (rule stmt.induct)

      (* Skip *)
      apply (intro allI impI)
      apply simp


     (* Expr *)
     apply (intro allI impI)
     apply (drule Expr_invers, erule exE)
     apply (simp (no_asm_simp))
     apply (rule bc_mt_corresp_comb) apply (rule HOL.refl, simp (no_asm_simp))
       apply (rule wt_method_compTpExpr_corresp) apply assumption+
        apply (simp add: compTpExpr_LT_ST [of _ pns lvars blk res])+
      apply (rule bc_mt_corresp_Pop)