Proof.ML
Back to theory Proof
val defs1 = [Let_def,split_def,hd (tl exec.rules),sup_state_def,get_code_def,correct_state_def,
correct_frame_def,wt_instr_def];
goal thy
"correct_state CFS phi (None, hp, (stk, loc, cn, ml, pc) # fs) --> wt_classfiles CFS phi \
\ --> wt_class CFS cn (phi cn)";
by (fast_tac (claset() addss (simpset() addsimps [wt_method_def,wt_class_def,wt_classfiles_def]@defs1)) 1);
qed_spec_mp "correct_state_imp_wt_class";
goal thy
"wt_classfiles CFS phi --> pc < length ins --> is_class CFS cn --> get_methods (CFS !! cn) ml = Some (rd, ins) \
\ --> wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc";
by (fast_tac (claset() addss (simpset() delsimps [split_paired_All]
addsimps [wt_method_def,wt_class_def,wt_classfiles_def]@defs1)) 1);
qed_spec_mp "get_methods_imp_wt_instr";
goal thy
"wt_classfiles CFS phi --> is_class CFS cn --> get_methods (CFS !! cn) ml = Some (rd, ins) \
\ --> 0 < (length ins) & wt_start CFS cn (snd ml) (phi cn ml)";
by (fast_tac (claset() addss (simpset() delsimps [split_paired_All]
addsimps [wt_method_def,wt_class_def,wt_classfiles_def]@defs1)) 1);
qed_spec_mp "get_methods_imp_wt_start";
Delsimps [split_paired_All];
(******* LAS *******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = LAS (X load idx); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "IAload_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = LAS (X store idx); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RS approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "IAstore_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = LAS (Bipush i); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
qed "Bipush_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = LAS Aconst_null; \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_def,sup_RTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
qed "Aconst_null_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = LAS las_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "las_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [IAload_correct,IAstore_correct,Bipush_correct,Aconst_null_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def]))));
qed "LAS_correct";
(******* MA *******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = MA (X aload); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup,
approx_val_imp_approx_val_invoConvertible RS approx_val_imp_approx_val_sup,ins_type_tylist_ok_lemma]
addss (simpset() addsimps [approx_stk_Cons,approx_val_RTS_AT,get_Addr_Addr,get_Arr_Arr,get_Nat_def,
correct_heap_def,correct_obj_def,nth_in_set_list,le_def,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "IAaload_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = MA (X astore); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [sup_heap_update_array,approx_stk_imp_approx_stk_sup_heap RS approx_stk_imp_approx_stk_sup,
approx_loc_imp_approx_loc_sup_heap RS approx_loc_imp_approx_loc_sup,fd_compatible_imp_approx_val,
correct_heap_imp_correct_heap_array_update,correct_frames_imp_correct_frames_array_update]
addss (simpset() addsimps [approx_stk_Cons,approx_val_RTS_AT,get_Addr_Addr,get_Arr_Arr,get_Nat_def,le_def,
sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "IAastore_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = MA ma_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "ma_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [IAaload_correct,IAastore_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def]))));
qed "MA_correct";
(**** CH ****)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = CH (Checkcast idx); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [compatible_imp_invoConvertible,approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,sup_RTS_eq,approx_stk_Cons,
approx_val_RTS,get_Addr_Addr]@defs1)) 1);
qed "Checkcast_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = CH ch_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "ch_com" 1);
by (fast_tac (claset() addIs [Checkcast_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def])) 1);
qed "CH_correct";
(******* MO *******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = MO (Getfield idx); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
by (Clarify_tac 1);
bd approx_stk_Cons_lemma 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [approx_val_RTS]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [get_Addr_Addr]) 1);
by (forward_tac [wRC_lemma1] 1);
ba 1;
ba 1;
ba 1;
ba 1;
by (fast_tac (claset() addEs [wideRefConvertible_trans RS mp RS mp] addss (simpset() addsimps [wRC])) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,
get_fields_imp_approx_val RS approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,approx_val_RTS,get_Obj_Obj,get_Addr_Addr,
sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "Getfield_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = MO (Putfield idx); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
by (Clarify_tac 1);
bd approx_stk_Cons_lemma 1;
by (Clarify_tac 1);
bd approx_stk_Cons_lemma 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [approx_val_RTS]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [get_Addr_Addr]) 1);
by (forward_tac [wRC_lemma1] 1);
ba 1;
ba 1;
ba 1;
ba 1;
by (fast_tac (claset() addEs [wideRefConvertible_trans RS mp RS mp] addss (simpset() addsimps [wRC])) 1);
by (Clarify_tac 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap RS approx_stk_imp_approx_stk_sup,
approx_loc_imp_approx_loc_sup_heap RS approx_loc_imp_approx_loc_sup,
sup_heap_update_value,correct_heap_imp_correct_heap_field_update,correct_frames_imp_correct_frames_field_update,
approx_val_imp_approx_val_assConvertible,get_fields_impl_get_all_fields3]
addss (simpset() addsimps [get_Obj_Obj])) 1);
qed "Putfield_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = MO mo_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "mo_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def]))));
qed "MO_correct";
(****** CO ******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = CO (New cl_idx); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addIs [sup_heap_newref,
approx_stk_imp_approx_stk_sup_heap RS approx_stk_imp_approx_stk_sup,Convertible_refl,
approx_loc_imp_approx_loc_sup_heap RS approx_loc_imp_approx_loc_sup,
correct_heap_imp_correct_heap_newref,correct_frames_imp_correct_frames_newref,correct_init_obj]
addss (simpset() addsimps [sup_RTS_eq,approx_stk_Cons,approx_val_def,
fun_upd_apply,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "New_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = CO (IAnewarray atd); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addSIs [disjI2] (*** ??? ***)
addIs [Convertible_refl RS conjunct2 RS conjunct1,sup_heap_newref,
approx_stk_imp_approx_stk_sup_heap RS approx_stk_imp_approx_stk_sup,
approx_loc_imp_approx_loc_sup_heap RS approx_loc_imp_approx_loc_sup,
correct_heap_imp_correct_heap_newref,correct_frames_imp_correct_frames_newref]
addss (simpset() addsimps [approx_stk_Cons,sup_RTS_eq,
approx_val_def,fun_upd_apply,correct_init_arr,sup_loc_Cons,
map_eq_Cons]@defs1)) 1);
qed "IAnewarray_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = CO co_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "co_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [New_correct,IAnewarray_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def]))));
qed "CO_correct";
(****** MI ******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ wt_classfiles CFS phi; \
\ (get_code CFS cn ml) ! pc = MI inv_com; \
\ Some (xp',hp,frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp,frs')";
by (asm_full_simp_tac (simpset() addsimps ([exec_mi_def,wt_MI_def]@defs1)) 1);
by (Clarify_tac 1);
by (forward_tac [get_methods_imp_wt_instr] 1);
ba 1;
ba 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps [wt_MI_def]@defs1) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
bd approx_stk_append_lemma 1;
by (Clarify_tac 1);
bd approx_stk_Cons_lemma 1;
by (asm_full_simp_tac (simpset() addsimps [take_all,drop_all]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [approx_val_RTS]) 1);
by (Clarify_tac 1);
by (forward_tac [inv_methref_ok_impl_get_methods] 1);
by (asm_full_simp_tac (simpset() addsimps[correct_heap_def]) 1);
by (eres_inst_tac [("x","a")] allE 1);
by (eres_inst_tac [("x","obj")] allE 1);
by (asm_full_simp_tac (simpset() addsimps[]) 1);
ba 1;
br refl 1;
ba 1;
ba 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps[is_class_get_obj_class]) 1);
ba 1;
br refl 1;
by (asm_full_simp_tac (simpset() addsimps [get_Addr_Addr]) 1);
by (Clarify_tac 1);
by (forward_tac [get_methods_imp_wt_start] 1);
ba 1;
back();
ba 1;
by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def,surjective_pairing RS sym]) 1);
by (Clarify_tac 1);
(** approx_stk **)
br conjI 1;
by (asm_full_simp_tac (simpset() addsimps [sup_loc_Nil,approx_stk_Nil]) 1);
(** approx_loc **)
br conjI 1;
br approx_loc_imp_approx_loc_sup 1;
by (Fast_tac 2);
by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,invoConv_approx_stk_imp_approx_loc)]
addss (simpset() addsimps [split_def,approx_loc_Cons,approx_val_def])) 1);
(* correct_frames *)
br conjI 1;
by (res_inst_tac [("x","fst (extract_inv_methref (get_cpool (CFS !! cn)) inv_com)")] exI 1);
by (res_inst_tac [("x","snd (snd (snd (extract_inv_methref (get_cpool (CFS !! cn)) inv_com)))")] exI 1);
by (dres_inst_tac [("s","snd (snd (snd (extract_inv_methref (get_cpool (CFS !! cn)) inv_com)))")] sym 1);
by (asm_full_simp_tac (simpset() addsimps [surjective_pairing RS sym]) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_pop_sup_push,approx_loc_imp_approx_loc_sup]
addss (simpset())) 1);
qed "MI_correct";
(****** MR ******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ wt_classfiles CFS phi; \
\ (get_code CFS cn ml) ! pc = MR (X return); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
by (Clarify_tac 1);
by (forward_tac [get_methods_imp_wt_instr] 1);
by (REPEAT (atac 1));
by (asm_full_simp_tac (simpset() addsimps [rd2tyOrVoid_TY]@defs1) 1);
by (Clarify_tac 1);
by (exhaust_tac "frs" 1);
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1) 1);
by (Clarify_tac 1);
by (forward_tac [get_methods_imp_wt_instr] 1);
by (EVERY [etac Suc_lessD 1,atac 1,atac 1]);
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_val_imp_approx_val_invoConvertible RS approx_val_imp_approx_val_sup]
addss (simpset() addsimps [push_rd_def,pop_rd_def,wt_MI_def,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
qed "IAreturn_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ wt_classfiles CFS phi; \
\ (get_code CFS cn ml) ! pc = MR Return; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (asm_full_simp_tac (simpset() addsplits [list.split] addsimps defs1) 1);
by (Clarify_tac 1);
by (forward_tac [get_methods_imp_wt_instr] 1);
by (REPEAT (atac 1));
by (asm_full_simp_tac (simpset() addsimps [pop_rd_def,rd2tyOrVoid_Void]@defs1) 1);
qed "Return_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = MR mr_com; \
\ wt_classfiles CFS phi; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (exhaust_tac "mr_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [IAreturn_correct,Return_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def]))));
qed "MR_correct";
(****** UB ******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = UB (Goto branch); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
addss (simpset() addsimps defs1)) 1);
qed "Goto_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = UB ub_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "ub_com" 1);
by (fast_tac (claset() addIs [Goto_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def])) 1);
qed "UB_correct";
(****** CB ******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = CB (If_ bop branch); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
qed "If_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = CB (Ifnull branch); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
qed "Ifnull_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = CB (X Ifiacmpeq branch); \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
qed "Ifiacmpeq_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = CB cb_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "cb_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [If_correct,Ifnull_correct,Ifiacmpeq_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def]))));
qed "CB_correct";
(****** OS ******)
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = OS Pop; \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
qed "Pop_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = OS Dup; \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "Dup_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ get_methods (CFS !! cn) ml = Some (rd, ins); \
\ ins ! pc = OS Swap; \
\ wt_instr (ins ! pc) CFS rd (get_cpool (CFS !! cn)) (phi cn ml) (length ins) pc; \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
qed "Swap_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS ; \
\ (get_code CFS cn ml) ! pc = OS os_com; \
\ wt_class CFS cn (phi cn); \
\ Some (xp',hp',frs') = exec (CFS, None, hp, (stk,loc,cn,ml,pc)#frs) ; \
\ correct_state CFS phi (None, hp, (stk,loc,cn,ml,pc)#frs) |] \
\==> correct_state CFS phi (xp',hp',frs')";
by (subgoal_tac "? rd ins. get_methods (CFS !! cn) ml = Some (rd, ins) & pc < length ins" 1);
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,Let_def,correct_frame_def,split_def]) 2);
by (exhaust_tac "os_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Swap_correct]
addss (simpset() addsimps [get_code_def,Let_def,wt_class_def,wt_method_def]))));
qed "OS_correct";
goal thy
"!!dummy. \
\[| wf_classfiles CFS; wt_classfiles CFS phi; correct_state CFS phi (xp,hp,frs)|] \
\ ==> exec (CFS,xp,hp,frs) = Some (xp',hp',frs') --> correct_state CFS phi (xp',hp',frs')";
by (exhaust_tac "xp" 1);
by (fast_tac (claset() addss (simpset() addsimps exec.rules)) 2);
by (exhaust_tac "frs" 1);
by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
by (force_tac (claset() addIs [LAS_correct,CO_correct,MO_correct,MA_correct,CH_correct,MI_correct,MR_correct,OS_correct,
CB_correct,UB_correct,correct_state_imp_wt_class],
simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[Let_def,split_def]) 1);
qed_spec_mp "BV_correct_1";
(*******)
goal thy
"xp=None --> frs~=[] --> (? xp' hp' frs'. exec (CFS,xp,hp,frs) = Some (xp',hp',frs'))";
by (fast_tac (claset() addIs [BV_correct_1]
addss (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)) 1);
qed_spec_mp "exec_lemma";
goal thy
"!!dummy. \
\[| wf_classfiles CFS; wt_classfiles CFS phi; \
\ correct_state CFS phi (xp,hp,frs); xp=None; frs~=[] |] \
\ ==> ? xp' hp' frs'. exec (CFS,xp,hp,frs) = Some (xp',hp',frs') & correct_state CFS phi (xp',hp',frs')";
by (dres_inst_tac [("CFS","CFS"),("hp","hp")] exec_lemma 1);
ba 1;
by (fast_tac (claset() addIs [BV_correct_1]) 1);
qed "L1";
(*******)
goalw thy [exec_all_def]
"!!dummy. \
\[| wf_classfiles CFS; CFS |- s -jvm-> t |] \
\ ==> wt_classfiles CFS phi --> correct_state CFS phi s --> correct_state CFS phi t";
be rtrancl_induct 1;
by (Simp_tac 1);
by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
qed_spec_mp "BV_correct";
Goal
"[| wf_classfiles CFS; wt_classfiles CFS phi; CFS |- s0 -jvm-> (None,hp,(stk,loc,cn,ml,pc)#frs); correct_state CFS phi s0 |] \
\ ==> approx_stk CFS hp stk (fst (((phi cn) ml) ! pc)) & approx_loc CFS hp loc (snd (((phi cn) ml) ! pc)) ";
bd BV_correct 1;
ba 1;
ba 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps [correct_state_def,correct_frame_def,Let_def,split_def]) 1);
qed_spec_mp "BV_correct_initial";