Theory CorrCompTp

theory CorrCompTp
imports LemmasComp TypeInf JVM Altern
(*  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[\<mapsto>]pTs)(This\<mapsto>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 \<turnstile> expr :: Class cname;
E = local_env G C (mn, pTs) pns lvars|]
==> is_class G cname "

apply (subgoal_tac "((fst E), (snd E)) \<turnstile> expr :: Class cname")
apply (frule ty_expr_is_type) apply simp
apply simp apply (simp (no_asm_use))
done



(********************************************************************************)
section "index"

lemma local_env_snd: "
snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>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 [rule_format (no_asm)]:
"∀ x1s m. (length k1s = length x1s
--> m(k1s[\<mapsto>]x1s)(k2s[\<mapsto>]x2s) = m ((k1s@k2s)[\<mapsto>](x1s@x2s)))"

apply (induct k1s)
apply simp
apply (intro strip)
apply (subgoal_tac "∃ x xr. x1s = x # xr")
apply clarify
apply simp
(* subgoal *)
apply (case_tac x1s)
apply auto
done


lemma map_of_append [rule_format]:
"∀ ys. (map_of ((rev xs) @ ys) = (map_of ys) ((map fst xs) [\<mapsto>] (map snd xs)))"
apply (induct xs)
apply simp
apply (rule allI)
apply (drule_tac x="a # ys" in spec)
apply (simp only: rev.simps append_assoc append_Cons append_Nil
map.simps map_of.simps map_upds_Cons hd.simps tl.simps)
done

lemma map_of_as_map_upds: "map_of (rev xs) = empty ((map fst xs) [\<mapsto>] (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 [THEN sym]
Map.map_of_append[symmetric] del:Map.map_of_append)
done

lemma map_upds_rev [rule_format]: "∀ xs. (distinct ks --> length ks = length xs
--> m (rev ks [\<mapsto>] rev xs) = m (ks [\<mapsto>] xs))"

apply (induct ks)
apply simp
apply (intro strip)
apply (subgoal_tac "∃ x xr. xs = x # xr")
apply clarify
apply (drule_tac x=xr in spec)
apply (simp add: map_upds_append [THEN sym])
(* subgoal *)
apply (case_tac xs)
apply auto
done

lemma map_upds_takeWhile [rule_format]:
"∀ ks. (empty(rev ks[\<mapsto>]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 "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
apply (simp split:split_if_asm)
apply (simp add: map_upds_append [THEN sym])
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] map.simps [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 [THEN sym])
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] map.simps [symmetric] length_map)
apply (simp only: nth_map)
apply simp
done


lemma sup_loc_update_index: "
[| G \<turnstile> T \<preceq> 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 \<turnstile>
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


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

section "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 \<box> 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 \<box> 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 \<box> 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 \<turnstile> ex :: T -->
is_inited_LT C pTs lvars LT -->
sttp_of (compTpExpr jmb G ex (ST, LT)) = (T # ST, LT))

(∀ ST LT Ts.
E \<turnstile> exs [::] Ts -->
is_inited_LT C pTs lvars LT -->
sttp_of (compTpExprs jmb G exs (ST, LT)) = ((rev Ts) @ ST, LT))"


apply (rule expr.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 (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 (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 (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 \<turnstile> s\<surd> -->
(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)"

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 [THEN sym])
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: le_maxI1 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
using [[linarith_split_limit = 0]]
apply simp
apply arith
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)
apply (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)
apply 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)
apply 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)) =
(Option.map (λ 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)
apply (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))"

apply (simp only:)
apply (induct i)
apply auto
done


(* 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 only: fst_conv image_compose [THEN sym] Fun.comp_def)
apply simp
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) apply 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 Option.map_def 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 \<box> 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 \<box> f')"

apply (simp add: start_sttp_resp_def)
apply (erule disjE)
apply simp+
done

lemma start_sttp_resp_cons_comb [simp]: "start_sttp_resp_cons f
==> start_sttp_resp (f \<box> 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 \<box> f')"

apply (simp add: start_sttp_resp_def)
apply (erule disjE)
apply simp
apply (erule disjE)
apply simp+
done

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+)




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

lemma length_comb [simp]: "length (mt_of ((f1 \<box> 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 expr.induct)
apply simp+
apply (case_tac binop)
apply simp+
apply (simp add: pushST_def split_beta)
apply simp+
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)))"

apply (rule stmt.induct)
apply (simp add: length_compTpExpr)+
done


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)+)


(* ********************************************************************** *)
section "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 \<box> 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 max_ac)
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 max_ac)
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 \<box> 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 \<box> 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 min_max.sup_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 min_max.sup_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 min_max.sup_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 \<turnstile> T \<preceq> 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 min_max.sup_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 min_max.sup_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 min_max.sup_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 \<turnstile> 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 min_max.sup_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 min_max.sup_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 min_max.sup_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 min_max.sup_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 \<turnstile> T \<preceq> 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 min_max.sup_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_def)
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (rule exI)+
apply (simp add: wf_prog_ws_prog [THEN comp_method])
apply auto
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)

-- {* @{text "<=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 [THEN sym])

-- "@{text 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 \<box> f2 \<box> 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 set.simps map.simps) 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 set.simps map.simps) 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) apply 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

lemma set_drop [simp] : "set (drop m xs) ⊆ set xs"
apply (rule_tac B="set (drop 0 xs)" in subset_trans)
apply (rule set_drop_le)
apply simp+
done



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 \<box> f2 \<box> 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 \<turnstile> ex :: T;
is_inited_LT C pTs lvars LT|]
==> sttp_of (compTpExpr (pns, lvars, blk, res) G ex (ST, LT)) = (T # ST, LT)"

apply (rule compTpExpr_LT_ST)
apply auto
done




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 \<turnstile> 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 \<turnstile> 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 expr.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 (no_asm_use)) *)
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 (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 \<box> compTpExpr jmb G expr2"
and ?f2.0="popST 2" and ?f3.0="pushST [PrimT Boolean] \<box> popST 1 \<box> 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 \<box> compTpExpr jmb G expr2 \<box> popST 2"
and ?f2.0 = "pushST [PrimT Boolean]"
and ?f3.0 = "popST (Suc 0) \<box> 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 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box> 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 \<box> compTpExpr jmb G expr2 \<box> popST 2 \<box>
pushST [PrimT Boolean] \<box> 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 (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 (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) apply 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 \<turnstile> s\<surd> -->
(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 (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 \<box> popST 2 \<box> compTpStmt jmb G stmt1 \<box>
nochangeST \<box> 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 \<box> compTpStmt jmb G stmt1 \<box>
nochangeST \<box> 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) apply 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] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
and ?f3.0="compTpStmt jmb G stmt1 \<box> nochangeST \<box> 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] \<box> compTpExpr jmb G expr \<box> popST 2"
and ?f2.0 = "compTpStmt jmb G stmt1"
and ?f3.0="nochangeST \<box> 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] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
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] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
compTpStmt jmb G stmt1 \<box> 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 (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 \<box> popST 2 \<box> compTpStmt jmb G stmt \<box> 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 \<box> compTpStmt jmb G stmt \<box> 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) apply 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] \<box> compTpExpr jmb G expr" and ?f2.0 = "popST 2"
and ?f3.0="compTpStmt jmb G stmt \<box> 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] \<box> compTpExpr jmb G expr \<box> 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] \<box> compTpExpr jmb G expr \<box> popST 2 \<box>
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) apply 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 \<box> compTpStmt jmb G blk \<box> 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 \<turnstile> blk \<surd> ∧
(∃T. E\<turnstile>res::T ∧ G\<turnstile>T\<preceq>rT))"
)
apply (erule exE, (erule conjE)+)+
apply (simp only:)
apply (rule bc_mt_corresp_comb) apply (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) apply (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 \<box> 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 \<turnstile> T \<preceq> 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 \<turnstile> blk \<surd> ∧
(∃T. E\<turnstile>res::T ∧ G\<turnstile>T\<preceq>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 [THEN sym])

(* comb *)
apply (simp only: comb_assoc [THEN sym])

(* 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 (simp only:)
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 only:)
apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
apply (simp only:)+ 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)


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

section "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