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)
     apply (simp add: start_sttp_resp_def)


    (* Comp *)
    apply (intro allI impI)
    apply (drule Comp_invers)
    apply clarify
    apply (simp (no_asm_use))
    apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)
       apply (simp (no_asm_simp)) apply blast
     apply (simp only: compTpStmt_LT_ST)
    apply (simp (no_asm_simp))

   (* Cond *)
   apply (intro allI impI)
   apply (simp (no_asm_simp) only:)
   apply (drule Cond_invers, (erule conjE)+)
   apply (simp (no_asm_simp))

   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 (no_asm_simp) add: length_compTpStmt length_compTpExpr)
    apply (simp (no_asm_simp))

   apply (rename_tac expr stmt1 stmt2 ST LT bc' f')
   apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]"
                and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
                            compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
                            compStmt jmb stmt2"
                and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]"
                and ?f3.0="compTpExpr jmb G expr □ popST 2 □ compTpStmt jmb G stmt1 □
                           nochangeST □ compTpStmt jmb G stmt2"
                 in bc_mt_corresp_comb_inside)
           apply (simp (no_asm_simp))+
       apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
       apply (simp (no_asm_simp) add: start_sttp_resp_def)+

   apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
                and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt1))) #
                            compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
                            compStmt jmb stmt2"
                and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
                and ?f3.0="popST 2 □ compTpStmt jmb G stmt1 □ nochangeST □ compTpStmt jmb G stmt2"
                 in bc_mt_corresp_comb_inside)
           apply (simp (no_asm_simp))+
       apply (simp (no_asm_simp)  add: pushST_def)
       apply (rule  wt_method_compTpExpr_corresp, assumption+)
        apply (simp (no_asm_simp))+


   apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr"
                and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt1)))"
                and ?bc3.0 = "compStmt jmb stmt1 @ Goto (1 + int (length (compStmt jmb stmt2))) #
                              compStmt jmb stmt2"
                and ?f1.0="pushST [PrimT Boolean] □ compTpExpr jmb G expr" and ?f2.0 = "popST 2"
                and ?f3.0="compTpStmt jmb G stmt1 □ nochangeST □ compTpStmt jmb G stmt2"
                 in bc_mt_corresp_comb_wt_instr)
             apply (simp (no_asm_simp) add: length_compTpExpr)+
      apply (simp (no_asm_simp) add: start_sttp_resp_comb)

     (* wt_instr *)
     apply (intro strip)
     apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean" and ST=ST and LT=LT
                  in wt_instr_Ifcmpeq)
           apply (simp (no_asm_simp))
          apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
        apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
        (* current pc *)
        apply (simp add: length_compTpExpr pushST_def)
       apply (simp only: compTpExpr_LT_ST)
       (* Suc pc *)
       apply (simp add: length_compTpExpr pushST_def)
       apply (simp add: popST_def start_sttp_resp_comb)
      (* jump goal *)
      apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
      apply (simp add: length_compTpExpr pushST_def)
      apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt)
      apply (simp only: compTpStmt_LT_ST)
      apply (simp add: nochangeST_def)
     (* check_type *)
     apply (subgoal_tac "
      (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) =
      (Some (PrimT Boolean # PrimT Boolean # ST, LT))")
      apply (simp only:)
     apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length)
       apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr)
     apply (simp (no_asm_simp) add: length_compTpExpr pushST_def)
     apply (simp only: compTpExpr_LT_ST_rewr)
    (* contracting… *)
    apply (rule contracting_popST)

   apply (drule_tac ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @
                            [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] "
                and ?bc2.0 = "compStmt jmb stmt1"
                and ?bc3.0="Goto (1 + int (length (compStmt jmb stmt2))) # compStmt jmb stmt2"
                and ?f1.0="pushST [PrimT Boolean] □ compTpExpr jmb G expr □ popST 2"
                and ?f2.0 = "compTpStmt jmb G stmt1"
                and ?f3.0="nochangeST □ compTpStmt jmb G stmt2"
                 in bc_mt_corresp_comb_inside)
           apply (simp (no_asm_simp))+
       apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
       apply (simp only: compTpExpr_LT_ST)
       apply (simp (no_asm_simp))
      apply (simp (no_asm_simp) add: length_compTpExpr)+


   apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @ compStmt jmb stmt1"
                and inst = "Goto (1 + int (length (compStmt jmb stmt2)))"
                and ?bc3.0 = "compStmt jmb stmt2"
                and ?f1.0="pushST [PrimT Boolean] □ compTpExpr jmb G expr □ popST 2 □ compTpStmt jmb G stmt1"
                and ?f2.0 = "nochangeST"
                and ?f3.0="compTpStmt jmb G stmt2"
                 in bc_mt_corresp_comb_wt_instr)
             apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
     apply (intro strip)
     apply (rule wt_instr_Goto)
        apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
      apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
      (* … ! nat (int pc + i) = … ! pc *)
      apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
      apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
      apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
      apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
      apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
     apply (simp only:)
     apply (simp add: length_compTpExpr length_compTpStmt)
    apply (rule contracting_nochangeST)


   apply (drule_tac
           ?bc1.0= "[LitPush (Bool False)] @ compExpr jmb expr @
                    [Ifcmpeq (2 + int (length (compStmt jmb stmt1)))] @
                    compStmt jmb stmt1 @ [Goto (1 + int (length (compStmt jmb stmt2)))]"
           and ?bc2.0 = "compStmt jmb stmt2"
           and ?bc3.0="[]"
           and ?f1.0="pushST [PrimT Boolean] □ compTpExpr jmb G expr □ popST 2 □ compTpStmt jmb G stmt1 □ nochangeST"
           and ?f2.0 = "compTpStmt jmb G stmt2"
           and ?f3.0="comb_nil"
           in bc_mt_corresp_comb_inside)
           apply (simp (no_asm_simp))+
       apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def compTpExpr_LT_ST)
       apply (simp only: compTpExpr_LT_ST)
       apply (simp (no_asm_simp))
       apply (simp only: compTpStmt_LT_ST)
      apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+

   apply simp


  (* Loop *)
  apply (intro allI impI)
  apply (simp (no_asm_simp) only:)
  apply (drule Loop_invers, (erule conjE)+)
  apply (simp (no_asm_simp))

  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 (no_asm_simp) add: length_compTpStmt length_compTpExpr)
   apply (simp (no_asm_simp))

  apply (rename_tac expr stmt ST LT bc' f')
  apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "[LitPush (Bool False)]"
               and ?bc3.0="compExpr jmb expr @ Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
                           compStmt jmb stmt @
                           [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
               and ?f1.0=comb_nil and ?f2.0 = "pushST [PrimT Boolean]"
               and ?f3.0="compTpExpr jmb G expr □ popST 2 □ compTpStmt jmb G stmt □ nochangeST"
                in bc_mt_corresp_comb_inside)
          apply (simp (no_asm_simp))+
      apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush)
      apply (simp (no_asm_simp) add: start_sttp_resp_def)+

  apply (drule_tac ?bc1.0="[LitPush (Bool False)]" and ?bc2.0 = "compExpr jmb expr"
               and ?bc3.0="Ifcmpeq (2 + int (length (compStmt jmb stmt))) #
                           compStmt jmb stmt @
                           [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
               and ?f1.0="pushST [PrimT Boolean]" and ?f2.0 = "compTpExpr jmb G expr"
               and ?f3.0="popST 2 □ compTpStmt jmb G stmt □ nochangeST"
                in bc_mt_corresp_comb_inside)
          apply (simp (no_asm_simp))+
      apply (simp (no_asm_simp)  add: pushST_def)
      apply (rule  wt_method_compTpExpr_corresp, assumption+)
       apply (simp (no_asm_simp))+


  apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr"
               and inst = "Ifcmpeq (2 + int (length (compStmt jmb stmt)))"
               and ?bc3.0 = "compStmt jmb stmt @
                             [Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
               and ?f1.0="pushST [PrimT Boolean] □ compTpExpr jmb G expr" and ?f2.0 = "popST 2"
               and ?f3.0="compTpStmt jmb G stmt □ nochangeST"
                in bc_mt_corresp_comb_wt_instr)
            apply (simp (no_asm_simp) add: length_compTpExpr)+
     apply (simp (no_asm_simp) add: start_sttp_resp_comb)

    (* wt_instr *)
    apply (intro strip)
    apply (rule_tac ts="PrimT Boolean" and ts'="PrimT Boolean"
          and ST=ST and LT=LT
          in wt_instr_Ifcmpeq)
          apply (simp (no_asm_simp))
         apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
       apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
       (* current pc *)
       apply (simp add: length_compTpExpr pushST_def)
      apply (simp only: compTpExpr_LT_ST)
      (* Suc pc *)
      apply (simp add: length_compTpExpr pushST_def)
      apply (simp add: popST_def start_sttp_resp_comb)
     (* jump goal *)
     apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
     apply (simp add: length_compTpExpr pushST_def)
     apply (simp add: popST_def start_sttp_resp_comb length_compTpStmt)
     apply (simp only: compTpStmt_LT_ST)
     apply (simp add: nochangeST_def)
    (* check_type *)
    apply (subgoal_tac "
     (mt_sttp_flatten (f' (ST, LT)) ! length ([LitPush (Bool False)] @ compExpr jmb expr)) =
     (Some (PrimT Boolean # PrimT Boolean # ST, LT))")
     apply (simp only:)
    apply (simp (no_asm_simp)) apply (rule trans, rule mt_sttp_flatten_comb_length)
      apply (rule HOL.refl) apply (simp (no_asm_simp) add: length_compTpExpr)
    apply (simp (no_asm_simp) add: length_compTpExpr pushST_def)
    apply (simp only: compTpExpr_LT_ST_rewr)
   (* contracting… *)
   apply (rule contracting_popST)

  apply (drule_tac
          ?bc1.0="[LitPush (Bool False)] @ compExpr jmb expr @
                  [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] "
          and ?bc2.0 = "compStmt jmb stmt"
          and ?bc3.0="[Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))]"
          and ?f1.0="pushST [PrimT Boolean] □ compTpExpr jmb G expr □ popST 2"
          and ?f2.0 = "compTpStmt jmb G stmt"
          and ?f3.0="nochangeST"
          in bc_mt_corresp_comb_inside)
          apply (simp (no_asm_simp))+
      apply (simp (no_asm_simp) add: pushST_def popST_def compTpExpr_LT_ST)
      apply (simp only: compTpExpr_LT_ST)
      apply (simp (no_asm_simp))
     apply (simp (no_asm_simp) add: length_compTpExpr)+


  apply (drule_tac ?bc1.0 = "[LitPush (Bool False)] @ compExpr jmb expr @ [Ifcmpeq (2 + int (length (compStmt jmb stmt)))] @ compStmt jmb stmt"
            and inst = "Goto (-2 + (- int (length (compStmt jmb stmt)) - int (length (compExpr jmb expr))))"
            and ?bc3.0 = "[]"
            and ?f1.0="pushST [PrimT Boolean] □ compTpExpr jmb G expr □ popST 2 □ compTpStmt jmb G stmt"
            and ?f2.0 = "nochangeST"
            and ?f3.0="comb_nil"
            in bc_mt_corresp_comb_wt_instr)
            apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)+
    apply (intro strip)
    apply (rule wt_instr_Goto)
       apply arith
      apply arith
     (* … ! nat (int pc + i) = … ! pc *)
     apply (simp (no_asm_simp))
     apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
     apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
     apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
     apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
     apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
    apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
    apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
    apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)

    apply (simp add: length_compTpExpr length_compTpStmt) (* check_type *)
    apply (simp add: pushST_def popST_def compTpExpr_LT_ST compTpStmt_LT_ST)
   apply (rule contracting_nochangeST)
  apply simp

  done


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



lemma wt_method_compTpInit_corresp: "⟦ jmb = (pns,lvars,blk,res); 
  wf_java_mdecl G C ((mn, pTs), rT, jmb); mxr = length LT;
  length LT = (length pns) + (length lvars) + 1;  vn ∈ set (map fst lvars);
  bc = (compInit jmb (vn,ty)); f = (compTpInit jmb (vn,ty));
  is_type G ty ⟧
  ⟹ bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
  apply (simp add: compInit_def compTpInit_def split_beta)
  apply (rule_tac ?bc1.0="[load_default_val ty]" and ?bc2.0="[Store (index jmb vn)]"
      in bc_mt_corresp_comb)
      apply simp+
    apply (simp add: load_default_val_def)
    apply (rule typeof_default_val [THEN exE])

    apply (rule bc_mt_corresp_LitPush_CT, assumption)
    apply (simp add: comp_is_type)
   apply (simp add: pushST_def)
   apply (rule bc_mt_corresp_Store_init)
   apply simp
   apply (rule index_length_lvars [THEN conjunct2])
     apply auto
  done


lemma wt_method_compTpInitLvars_corresp_aux [rule_format (no_asm)]: "
  ∀ lvars_pre lvars0 ST LT.
  jmb = (pns,lvars0,blk,res) ∧
  lvars0 = (lvars_pre @ lvars) ∧
  length LT = (length pns) + (length lvars0) + 1 ∧
  wf_java_mdecl G C ((mn, pTs), rT, jmb)
 ⟶ bc_mt_corresp (compInitLvars jmb lvars) (compTpInitLvars jmb lvars) (ST, LT) (comp G) rT 
       (length LT) (length (compInitLvars jmb lvars))"
  apply (induct lvars)
   apply (simp add: compInitLvars_def)

  apply (intro strip, (erule conjE)+)
  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="lvars_pre @ [a]" in spec)
  apply (drule_tac x="lvars0" in spec)
  apply (simp (no_asm_simp) add: compInitLvars_def)
  apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb lvars"
      in bc_mt_corresp_comb)
      apply (simp (no_asm_simp) add: compInitLvars_def)+

    apply (rule_tac vn=vn and ty=ty in wt_method_compTpInit_corresp)
           apply assumption+
         apply (simp (no_asm_simp))+
    apply (simp add: wf_java_mdecl_def)     (* is_type G ty *)
   apply (simp add: compTpInit_def storeST_def pushST_def)
  apply simp
  done


lemma wt_method_compTpInitLvars_corresp: "⟦ jmb = (pns,lvars,blk,res); 
  wf_java_mdecl G C ((mn, pTs), rT, jmb);
  length LT = (length pns) + (length lvars) + 1; mxr = (length LT);
  bc = (compInitLvars jmb lvars); f= (compTpInitLvars jmb lvars) ⟧
  ⟹ bc_mt_corresp bc f (ST, LT) (comp G) rT mxr (length bc)"
  apply (simp only:)
  apply (subgoal_tac "bc_mt_corresp (compInitLvars (pns, lvars, blk, res) lvars)
            (compTpInitLvars (pns, lvars, blk, res) lvars) (ST, LT) (TranslComp.comp G) rT
            (length LT) (length (compInitLvars (pns, lvars, blk, res) lvars))")
   apply simp
  apply (rule_tac lvars_pre="[]" in wt_method_compTpInitLvars_corresp_aux)
  apply auto
  done


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



lemma wt_method_comp_wo_return: "⟦ wf_prog wf_java_mdecl G;
  wf_java_mdecl G C ((mn, pTs), rT, jmb); 
  bc = compInitLvars jmb lvars @ compStmt jmb blk @ compExpr jmb res;
  jmb = (pns,lvars,blk,res); 
  f = (compTpInitLvars jmb lvars □ compTpStmt jmb G blk □ compTpExpr jmb G res);
  sttp = (start_ST, start_LT C pTs (length lvars));
  li = (length (inited_LT C pTs lvars))
  ⟧
⟹ bc_mt_corresp bc f sttp (comp G) rT  li (length bc)"
  apply (subgoal_tac "∃E. (E = (local_env G C (mn, pTs) pns lvars) ∧ E ⊢ blk √ ∧
                          (∃T. E⊢res::T ∧ G⊢T≼rT))")
   apply (erule exE, (erule conjE)+)+
   apply (simp only:)
   apply (rule bc_mt_corresp_comb, (rule HOL.refl)+)

     (* InitLvars *)
     apply (rule wt_method_compTpInitLvars_corresp)
          apply assumption+
         apply (simp only:)
        apply (simp (no_asm_simp) add: start_LT_def)
        apply (rule wf_java_mdecl_length_pTs_pns, assumption)
       apply (simp (no_asm_simp) only: start_LT_def)
       apply (simp (no_asm_simp) add: inited_LT_def)+

    apply (rule bc_mt_corresp_comb, (rule HOL.refl)+)
       apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST)

      (* stmt *)
      apply (simp only: compTpInitLvars_LT_ST)
      apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))")
       prefer 2 apply (simp (no_asm_simp) add: inited_LT_def)
      apply (simp only:)
      apply (rule_tac s=blk in wt_method_compTpStmt_corresp)
             apply assumption+
           apply (simp only:)+
        apply (simp (no_asm_simp) add: is_inited_LT_def)
       apply (simp only:)+

     (* expr *)
     apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST is_inited_LT_def)
     apply (subgoal_tac "(Suc (length pTs + length lvars)) = (length (inited_LT C pTs lvars))")
      prefer 2 apply (simp (no_asm_simp) add: inited_LT_def)
     apply (simp only:)
     apply (rule_tac ex=res in wt_method_compTpExpr_corresp)
            apply assumption+
          apply (simp only:)+
       apply (simp (no_asm_simp) add: is_inited_LT_def)
      apply (simp only:)+

    (* start_sttp_resp *)
    apply (simp add: start_sttp_resp_comb)+

  (* subgoal *)
  apply (simp add: wf_java_mdecl_def local_env_def)
  done


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



lemma check_type_start:
  "⟦ wf_mhead cG (mn, pTs) rT; is_class cG C⟧
  ⟹ check_type cG (length start_ST) (Suc (length pTs + mxl))
              (OK (Some (start_ST, start_LT C pTs mxl)))"
  apply (simp add: check_type_def wf_mhead_def start_ST_def start_LT_def)
  apply (simp add: check_type_simps)
  apply (simp only: list_def)
  apply (auto simp: err_def)
  done


lemma wt_method_comp_aux:
  "⟦ bc' = bc @ [Return]; f' = (f □ nochangeST);
  bc_mt_corresp bc f sttp0 cG rT (1+length pTs+mxl) (length bc);
  start_sttp_resp_cons f';
  sttp0 = (start_ST, start_LT C pTs mxl);
  mxs = max_ssize (mt_of (f' sttp0));
  wf_mhead cG (mn, pTs) rT; is_class cG C;
  sttp_of (f sttp0) = (T # ST, LT);

  check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT))) ⟶
  wt_instr_altern Return cG rT (mt_of (f' sttp0)) mxs (1+length pTs+mxl) 
         (Suc (length bc)) empty_et (length bc)
⟧
⟹ wt_method_altern cG C pTs rT mxs mxl bc' empty_et (mt_of (f' sttp0))"
  apply (subgoal_tac "check_type cG (length start_ST) (Suc (length pTs + mxl))
                                    (OK (Some (start_ST, start_LT C pTs mxl)))")
   apply (subgoal_tac "check_type cG mxs (1+length pTs+mxl) (OK (Some (T # ST, LT)))")

    apply (simp add: wt_method_altern_def)

    (* length (.. f ..) = length bc *)
    apply (rule conjI)
     apply (simp add: bc_mt_corresp_def split_beta)

    (* check_bounded *)
    apply (rule conjI)
     apply (simp add: bc_mt_corresp_def split_beta check_bounded_def)
     apply (erule conjE)+
     apply (intro strip)
     apply (subgoal_tac "pc < (length bc) ∨ pc = length bc")
      apply (erule disjE)
       (* case  pc < length bc *)
       apply (subgoal_tac "(bc' ! pc) = (bc ! pc)")
        apply (simp add: wt_instr_altern_def eff_def)
       (* subgoal *)
       apply (simp add: nth_append)
      (* case  pc = length bc *)
      apply (subgoal_tac "(bc' ! pc) = Return")
       apply (simp add: wt_instr_altern_def)
      (* subgoal *)
      apply (simp add: nth_append)

     (* subgoal pc < length bc ∨ pc = length bc *)
     apply arith

    (* wt_start *)
    apply (rule conjI)
     apply (simp add: wt_start_def start_sttp_resp_cons_def split_beta)
     apply (drule_tac x=sttp0 in spec) apply (erule exE)
     apply (simp add: mt_sttp_flatten_def start_ST_def start_LT_def)

    (* wt_instr *)
    apply (intro strip)
    apply (subgoal_tac "pc < (length bc) ∨ pc = length bc")
     apply (erule disjE)

      (* pc < (length bc) *)
      apply (simp (no_asm_use) add: bc_mt_corresp_def mt_sttp_flatten_def split_beta)
      apply (erule conjE)+
      apply (drule mp, assumption)+
      apply (erule conjE)+
      apply (drule spec, drule mp, assumption)
      apply (simp add: nth_append)
      apply (simp (no_asm_simp) add: comb_def split_beta nochangeST_def)

     (* pc = length bc *)
     apply (simp add: nth_append)

    (* subgoal pc < (length bc) ∨ pc = length bc *)
    apply arith

   (* subgoals *)
   apply (simp (no_asm_use) add: bc_mt_corresp_def split_beta)
   apply (subgoal_tac "check_type cG (length (fst sttp0)) (Suc (length pTs + mxl))
                                     (OK (Some sttp0))")
    apply ((erule conjE)+, drule mp, assumption)
    apply (simp add: nth_append)
    apply (simp (no_asm_simp) add: comb_def nochangeST_def split_beta)
   apply (simp (no_asm_simp))

  apply (rule check_type_start, assumption+)
  done


lemma wt_instr_Return: "⟦fst f ! pc = Some (T # ST, LT); (G ⊢ T ≼ rT); pc < max_pc;
  check_type (TranslComp.comp G) mxs mxr (OK (Some (T # ST, LT)))
  ⟧
  ⟹ wt_instr_altern Return (comp G) rT  (mt_of f) mxs mxr max_pc empty_et pc"
  apply (case_tac "(mt_of f ! pc)")
   apply (simp  add: wt_instr_altern_def eff_def norm_eff_def app_def)+
  apply (drule sym)
  apply (simp add: comp_widen xcpt_app_def)
  done


theorem wt_method_comp: "
  ⟦ wf_java_prog G; (C, D, fds, mths) ∈ set G; jmdcl ∈ set mths;
  jmdcl = ((mn,pTs), rT, jmb);
  mt = (compTpMethod G C jmdcl);
  (mxs, mxl, bc, et) = mtd_mb (compMethod G C jmdcl) ⟧
  ⟹ wt_method (comp G) C pTs rT mxs mxl bc et mt"

  (* show statement for wt_method_altern *)
  apply (rule wt_method_altern_wt_method)

  apply (subgoal_tac "wf_java_mdecl G C jmdcl")
   apply (subgoal_tac "wf_mhead G (mn, pTs) rT")
    apply (subgoal_tac "is_class G C")
     apply (subgoal_tac "∀jmb. ∃ pns lvars blk res. jmb = (pns, lvars, blk, res)")
      apply (drule_tac x=jmb in spec, (erule exE)+)
      apply (subgoal_tac "∃E. (E = (local_env G C (mn, pTs) pns lvars) ∧ E ⊢ blk √ ∧
                              (∃T. E⊢res::T ∧ G⊢T≼rT))")
       apply (erule exE, (erule conjE)+)+
       apply (simp add: compMethod_def compTpMethod_def split_beta)
       apply (rule_tac T=T and LT="inited_LT C pTs lvars" and ST=start_ST in wt_method_comp_aux)

                (* bc *)
                apply (simp only: append_assoc [symmetric])

               (* comb *)
               apply (simp only: comb_assoc [symmetric])

              (* bc_corresp *)
              apply (rule wt_method_comp_wo_return)
                    apply assumption+
                  apply (simp (no_asm_use) only: append_assoc)
                 apply (rule HOL.refl)
                apply (simp (no_asm_simp))+
              apply (simp (no_asm_simp) add: inited_LT_def)

             (* start_sttp_resp *)
             apply (simp add: start_sttp_resp_cons_comb_cons_r)+

          (* wf_mhead / is_class *)
          apply (simp add: wf_mhead_def comp_is_type)
         apply (simp add: comp_is_class)

        (* sttp_of .. = (T # ST, LT) *)
        apply (simp (no_asm_simp) add: compTpInitLvars_LT_ST compTpExpr_LT_ST compTpStmt_LT_ST is_inited_LT_def)
       apply (subgoal_tac "(snd (compTpInitLvars (pns, lvars, blk, res) lvars
                            (start_ST, start_LT C pTs (length lvars))))
                           = (start_ST, inited_LT C pTs lvars)")
        prefer 2
        apply (rule compTpInitLvars_LT_ST)
         apply (rule HOL.refl)
        apply assumption
       apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
                            (start_ST, inited_LT C pTs lvars)))
                            = (start_ST, inited_LT C pTs lvars)")
        prefer 2 apply (erule conjE)+
        apply (rule compTpStmt_LT_ST)
             apply (rule HOL.refl)
            apply assumption+
         apply (simp only:)+
        apply (simp (no_asm_simp) add: is_inited_LT_def)
       apply (simp (no_asm_simp) add: is_inited_LT_def)


       (* Return *)
       apply (intro strip)
       apply (rule_tac T=T and ST=start_ST and LT="inited_LT C pTs lvars" in wt_instr_Return)
          apply (simp (no_asm_simp) add: nth_append length_compTpInitLvars length_compTpStmt length_compTpExpr)
          apply (simp only: compTpInitLvars_LT_ST compTpStmt_LT_ST compTpExpr_LT_ST nochangeST_def)
          apply (simp only: is_inited_LT_def compTpStmt_LT_ST compTpExpr_LT_ST)
          apply (simp (no_asm_simp))+
      apply simp

      (* subgoal ∃ E. … *)
      apply (simp add: wf_java_mdecl_def local_env_def)

     (* subgoal jmb = (…) *)
     apply (simp only: split_paired_All, simp)

    (* subgoal is_class / wf_mhead / wf_java_mdecl *)
    apply (blast intro: methd [THEN conjunct2])
   apply (frule wf_prog_wf_mdecl, assumption+)
    apply (simp only:)
   apply (simp add: wf_mdecl_def)
  apply (rule wf_java_prog_wf_java_mdecl, assumption+)
  done


lemma comp_set_ms: "(C, D, fs, cms)∈set (comp G) 
  ⟹ ∃ ms. (C, D, fs, ms) ∈set G   ∧ cms = map (compMethod G C) ms"
  by (auto simp: comp_def compClass_def)


  (* ---------------------------------------------------------------------- *)

subsection "Main Theorem"
  (* MAIN THEOREM: 
  Methodtype computed by comp is correct for bytecode generated by compTp *)
theorem wt_prog_comp: "wf_java_prog G  ⟹ wt_jvm_prog (comp G) (compTp G)"
  apply (simp add: wf_prog_def)

  apply (subgoal_tac "wf_java_prog G")
   prefer 2
   apply (simp add: wf_prog_def)
  apply (simp (no_asm_simp) add: wf_prog_def wt_jvm_prog_def)
  apply (simp add: comp_ws_prog)

  apply (intro strip)
  apply (subgoal_tac "∃C D fs cms. c = (C, D, fs, cms)")
   apply clarify
   apply (frule comp_set_ms)
   apply clarify
   apply (drule bspec, assumption)
   apply (rule conjI)

    (* wf_mrT *)
    apply (case_tac "C = Object")
     apply (simp add: wf_mrT_def)
    apply (subgoal_tac "is_class G D")
     apply (simp add: comp_wf_mrT)
    apply (simp add: wf_prog_def ws_prog_def ws_cdecl_def)
    apply blast

   (* wf_cdecl_mdecl *)
   apply (simp add: wf_cdecl_mdecl_def)
   apply (simp add: split_beta)
   apply (intro strip)

   (* show wt_method … *)
   apply (subgoal_tac "∃sig rT mb. x = (sig, rT, mb)")
    apply (erule exE)+
    apply (simp (no_asm_simp) add: compMethod_def split_beta)
    apply (erule conjE)+
    apply (drule_tac x="(sig, rT, mb)" in bspec)
     apply simp
    apply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp)
         apply assumption+
      apply simp
     apply (simp (no_asm_simp) add: compTp_def)
     apply (simp (no_asm_simp) add: compMethod_def split_beta)
     apply (frule WellForm.methd) apply assumption+
      apply simp
     apply simp
    apply (simp add: compMethod_def split_beta)
   apply auto
  done



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

declare split_paired_All [simp add]
declare split_paired_Ex [simp add]


end