Quelle CorrCompTp.thy
Sprache: Isabelle
(* Title: HOL/MicroJava/Comp/CorrCompTp.thy Author: Martin Strecker *) theory CorrCompTpimports 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] ==> 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] ==> ool" 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] ==> 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 simpapply simpapply (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 simpapply (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 simpapply (subgoal_tac "∃ x xr. x1s = x # xr" )apply clarsimp(* subgoal *) apply (case_tac x1s)apply autodone lemma map_of_append: "map_of ((rev xs) @ ys) = (map_of ys) ((map fst xs) [↦ ] (map snd xs))" apply (induct xs arbitrary: ys)apply simpapply (rename_tac a xs ys)apply (drule_tac x="a # ys" in meta_spec)apply (simp only: rev.simps append_assoc append_Cons append_Nildone 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 simpapply (simp add: unique_def map_of_append map_of_as_map_upds [symmetric]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 simpapply (subgoal_tac "∃ x xr. xs = x # xr" )apply clarifyapply (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 simpapply (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[↦ ↦ ][a])" )apply (simp split:if_split_asm)apply (simp add: map_upds_append [symmetric])apply (case_tac ks)apply autodone 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 (\<lambda>p. (fst p, snd p)) lvars) *) apply simp(* show length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars) *) apply (drule map_of_upds_SomeD)apply (drule length_takeWhile)apply simpdone 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 simpdone 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 assumptionapply (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 \<and> 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 simpdone lemmas compTpExpr_LT_ST [rule_format (no_asm)] = THEN conjunct1]lemmas compTpExprs_LT_ST [rule_format (no_asm)] = 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)" apply (induct lvars)apply simpapply (intro strip)apply (subgoal_tac "∃ vn ty. a = (vn, ty)" )prefer 2apply (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_alldone 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_defapply (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 autodone 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 autodone (* 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 arithdone 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 arithdone (**********************************************************************) definition offset_xcentry :: "[nat, 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] ==> 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)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 2apply (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 clarifyapply (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') \<in> set (eff \<dots>) *) apply (simp add: eff_def)(* norm_eff *) apply (clarsimp simp: nth_append pc_succs_shift)(* show P x of bspec *) apply simpapply (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 \<exists> 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 ==> × state_type] ==> ool" 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 ==> × state_type] ==> 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 autodone 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)"state_type ==> where "ST_of == fst" abbreviation (input)"state_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_defapply (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 clarifyapply autodone 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 ==> × state_type, state_type, jvm_prog, ty, nat, p_count] ==> 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 \<dots> *) 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 simpapply (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 arithapply (simp (no_asm_simp))+(* case pc \<ge> length mt1 *) apply (rule_tac bc=bc2 and mt=mt2 and bc_post="[]" and mt_post="[Some sttp2]" and mxr=mxrin wt_instr_offset)apply simpapply (simp (no_asm_simp))+apply simpapply (simp add: max_ssize_def) apply (simp (no_asm_simp))(* show check_type \<dots> *) apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2" )apply (simp only:)apply (rule check_type_mono) apply assumptionapply (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 simpapply (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 ==> 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 simpdone (* move into prelude -- compare with nat_int_length *) lemma int_outside_right: "0 ≤ (m::int) ==> m + (int n) = int ((nat m) + n)" by simplemma 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 arithlemmas check_type_simps = check_type_def states_def JVMType.sl_defup_deflemma 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 clarifyapply (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_defapply (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 clarifyapply (rule_tac x="(length ST)" in exI)apply simpdone 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 clarifyapply (rule_tac x="Suc (length STo)" in exI)apply simpdone 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_defapply (intro strip)apply (rule conjI)apply (rule check_type_mono, assumption, simp)apply (simp add: check_type_simps)apply clarifyapply (rule_tac x="Suc (length ST)" in exI)apply simpapply (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_defapply (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 clarifyapply (rule_tac x="Suc (length ST)" in exI)apply simpapply simpdone 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_defapply (intro strip)apply (rule conjI)apply (rule check_type_mono, assumption, simp)apply (simp add: check_type_simps)apply clarifyapply (rule_tac x="Suc (length ST)" in exI)apply (simp (no_asm_simp))apply (simp only: err_def)apply (frule listE_nth_in)apply assumptionapply (subgoal_tac "LT ! i ∈ {x. ∃ y∈ types cG. x = OK y}" )apply (drule CollectD)apply (erule bexE)apply (simp (no_asm_simp))apply blastapply blastdone 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 clarifyapply (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 clarifyapply (rule_tac x="(length ST)" in exI)apply simpdone 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_defapply (intro strip)apply (rule conjI)apply (rule check_type_mono, assumption, simp)apply (simp add: check_type_simps)apply clarifyapply (rule_tac x="Suc (Suc (length ST))" in exI)apply simpdone 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_defapply (intro strip)apply (rule conjI)apply (rule check_type_mono, assumption, simp)apply (simp add: check_type_simps)apply clarifyapply (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 clarifyapply (rule_tac x="Suc (length ST)" in exI)apply simpdone 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 clarifyapply (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 assumptiondone 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 clarifyapply (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 assumptionapply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)🍋 ‹ ‹ 🚫 › \
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 simpapply (simp add: check_type_simps)apply clarifyapply (rule_tac x="Suc (length ST)" in exI)apply simp+apply (simp only: comp_is_type)apply (frule method_wf_mdecl) apply assumption apply assumptionapply (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 simpapply (intro strip, (erule conjE)+)apply (case_tac "pc < length mt1" )(* case pc < length mt1 *) apply (drule spec, drule mp, assumption)apply assumption(* case pc \<ge> 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=bc3and 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 simpapply (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 blastapply (simp (no_asm_simp))apply simp (* subgoal bc3 = [] *) apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> 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=bc3and 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 simpapply (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 blastapply (simp (no_asm_simp))apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *) (* subgoals check_type*) (* \<dots> ! length mt2 *) apply simpapply (erule_tac P="f3 = comb_nil" in disjE)(* -- case f3 = comb_nil *) apply (subgoal_tac "mt3 = [] ∧ sttp2 = sttp3" ) apply (erule conjE)+apply simpapply (rule check_type_mono, assumption)apply (simp only: max_ssize_def)apply (rule max_of_list_sublist)apply (simp (no_asm_simp))apply blastapply simp (* subgoal bc3 = [] *) apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> 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 blastapply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *) (* subgoal check_type \<dots> Some sttp2 *) apply (simp add: nth_append)(* subgoal check_type \<dots> 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 \<exists> ... *) apply (rule surj_pair)+done (* ******************** *) definition contracting :: "(state_type ==> × state_type) ==> 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 simpapply (intro strip)apply (rule list.induct)apply simpapply simpapply blastapply (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 simpapply (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 autodone 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 clarifyapply (drule_tac x=ST in spec, drule_tac x=LT in spec)apply (case_tac "(sttp_of (f (ST, LT)))" )apply simpapply (erule conjE)+apply (drule listE_set)+apply (rule conjI)apply (rule_tac x="length a" in exI)apply simpapply (rule listI)apply simpapply blastapply (rule listI)apply simpapply blastapply autodone (* ******************** *) 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_defapply (intro strip, (erule conjE)+)apply (drule mp, assumption)+apply (erule conjE)+apply (drule mp, assumption)apply (rule conjI)(* wt_instr \<dots> *) apply (intro strip)apply (case_tac "pc < length mt1" )(* case pc < length mt1 *) apply (drule spec, drule mp, assumption)apply assumption(* case pc \<ge> length mt1 *) apply (subgoal_tac "pc = length mt1" ) prefer 2 apply arithapply (simp only:)apply (simp add: nth_append mt_sttp_flatten_def)(* check_type \<dots> *) 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 = [] \<and> sttp2 = sttp3 *) apply (simp add: nth_append comb_nil_def) (* subgoal \<dots> ! 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) autolemma 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 clarifyapply (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 blastapply (simp add: start_sttp_resp_def)(* Lit *) apply (intro allI impI)apply (simp only:)apply (drule Lit_invers)apply simpapply (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 2apply (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 blastapply (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 simpapply (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 simpapply (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 simpapply (rule bc_mt_corresp_comb)apply (rule HOL.refl)apply simpapply blastapply (rule bc_mt_corresp_comb, rule HOL.refl)apply (simp only: compTpExpr_LT_ST)apply (simp only: compTpExpr_LT_ST)apply blastapply (simp only: compTpExpr_LT_ST)apply simpapply (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 clarifyapply (simp add: is_inited_LT_def)apply (rule bc_mt_corresp_Load)apply (rule index_in_bounds)apply simpapply assumptionapply (rule inited_LT_at_index_no_err)apply (rule index_in_bounds)apply simpapply assumptionapply (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 clarifyapply (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 simpapply assumptionapply (rule sup_loc_update_index, assumption+)apply simpapply 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 clarifyapply (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 clarifyapply (simp (no_asm_use))apply (rule bc_mt_corresp_comb)apply (rule HOL.refl)apply simpapply blastapply (simp only: compTpExpr_LT_ST)apply (rule bc_mt_corresp_comb, (rule HOL.refl)+)apply blastapply (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 clarifyapply (simp (no_asm_use))apply (rule bc_mt_corresp_comb)apply (rule HOL.refl)apply simpapply blastapply (simp only: compTpExpr_LT_ST)apply (rule bc_mt_corresp_comb, (rule HOL.refl)+)apply blastapply (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 clarifyapply (simp (no_asm_use))apply (rule bc_mt_corresp_comb)apply (rule HOL.refl)apply simpapply blastapply (simp only: compTpExpr_LT_ST)apply blastapply simpdone lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = 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 clarifyapply (simp (no_asm_use))apply (rule bc_mt_corresp_comb) apply (rule HOL.refl)apply (simp (no_asm_simp)) apply blastapply (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 2apply (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=LTin 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\<dots> *) 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))(* \<dots> ! nat (int pc + i) = \<dots> ! 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"[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 2apply (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=LTin 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\<dots> *) apply (rule contracting_popST)apply (drule_tac"[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 arithapply arith(* \<dots> ! nat (int pc + i) = \<dots> ! 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 simpdone (**********************************************************************************) 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 simpapply (rule index_length_lvars [THEN conjunct2])apply autodone 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 2apply (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 simpdone 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 simpapply (rule_tac lvars_pre="[]" in wt_method_compTpInitLvars_corresp_aux)apply autodone (**********************************************************************************) 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 \<or> 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) \<or> 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 2apply (rule compTpInitLvars_LT_ST)apply (rule HOL.refl)apply assumptionapply (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 \<exists> E. \<dots> *) apply (simp add: wf_java_mdecl_def local_env_def)(* subgoal jmb = (\<dots>) *) 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 2apply (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 clarifyapply (frule comp_set_ms)apply clarifyapply (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 \<dots> *) 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 simpapply (rule_tac mn="fst sig" and pTs="snd sig" in wt_method_comp)apply assumption+apply simpapply (simp (no_asm_simp) add: compTp_def)apply (simp (no_asm_simp) add: compMethod_def split_beta)apply (frule WellForm.methd) apply assumption+apply simpapply simpapply (simp add: compMethod_def split_beta)apply autodone (**********************************************************************************) declare split_paired_All [simp add]declare split_paired_Ex [simp add]end
Messung V0.5 in Prozent C=93 H=100 G=96
¤ Dauer der Verarbeitung: 0.63 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
