Correct.ML
Back to theory Correct
goal thy
"!!dummy. \
\[|correct_heap CFS hp; hp a = Some (Obj cn od) |] ==> is_class CFS cn";
by (fast_tac (claset() addss (simpset() addsimps [correct_heap_def,correct_obj_def])) 1);
qed "correct_heap_imp_is_class";
(** sup_heap **)
goal thy
"hp x = None --> sup_heap hp (hp((newref hp) |-> obj))";
by (asm_full_simp_tac (simpset() addsplits [obj.split] addsimps [sup_heap_def]) 1);
by (Clarify_tac 1);
bd newref_None 1;
back();
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "sup_heap_newref";
goal thy
"hp a = Some (Obj cn od') --> sup_heap hp (hp(a |-> Obj cn od))";
by (asm_full_simp_tac (simpset() setloop (split_tac [split_if,obj.split])addsimps [sup_heap_def]) 1);
qed_spec_mp "sup_heap_update_value";
goal thy
"hp a = Some (Arr fd ad') --> sup_heap hp (hp(a |-> Arr fd ad))";
by (asm_full_simp_tac (simpset() setloop (split_tac [split_if,obj.split]) addsimps [sup_heap_def]) 1);
qed_spec_mp "sup_heap_update_array";
(** approx_val **)
goal thy
"!!dummy. \
\[| wf_classfiles CFS |] \
\==> approx_val CFS hp v (Refs rs) --> wideRefsConvertible CFS rs rs' \
\ --> approx_val CFS hp v (Refs rs')";
by (asm_full_simp_tac (simpset() setloop (split_tac [val_.split]) addsimps [approx_val_def,wRC]) 1);
by (fast_tac (claset() addDs [wideRefConvertible_trans]) 1);
qed_spec_mp "approx_val_imp_approx_val_wideRefConvertible";
goal thy
"!!dummy. \
\[| wf_classfiles CFS |] \
\==> approx_val CFS hp v (US ts) --> invoConvertible CFS ts ts' --> approx_val CFS hp v (US ts')";
by (exhaust_tac "ts" 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addIs [approx_val_imp_approx_val_wideRefConvertible] addss (simpset())) 1);
qed_spec_mp "approx_val_imp_approx_val_invoConvertible";
goal thy
"!!dummy. \
\[| wf_classfiles CFS |] \
\==> assConvertible CFS tys at --> approx_val CFS hp s (US tys) --> approx_val CFS hp s (US at)";
by (fast_tac (claset() addIs [approx_val_imp_approx_val_invoConvertible]
addss (simpset() addsimps [assConvertible_def])) 1);
qed_spec_mp "approx_val_imp_approx_val_assConvertible";
goal thy
"approx_val CFS hp val at --> sup_heap hp hp' --> approx_val CFS hp' val at";
by (asm_full_simp_tac (simpset() setloop (split_tac [any.split,val_.split,obj.split])
addsimps [approx_val_def,sup_heap_def]) 1);
by (Clarify_tac 1);
by (exhaust_tac "obj" 1);
by (fast_tac (claset() addss (simpset() delsplits [split_if])) 1);
by (eres_inst_tac [("x","loc")] allE 1);
by (eres_inst_tac [("x","Arr field_desc list")] allE 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","field_desc")] allE 1);
by (eres_inst_tac [("x","list")] allE 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
by (res_inst_tac [("x","Arr field_desc ad'")] exI 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (res_inst_tac [("x","r'")] bexI 1);
by (Fast_tac 2);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "approx_val_imp_approx_val_sup_heap";
goal thy
"hp a = Some obj' & approx_val CFS hp val at & get_obj_type obj = get_obj_type obj' \
\ --> approx_val CFS (hp(a|->obj)) val at";
by (asm_full_simp_tac (simpset() setloop (split_tac [any.split,val_.split])
addsimps [approx_val_def]) 1);
by (fast_tac (claset() addss (simpset())) 1);
qed_spec_mp "approx_val_imp_approx_val_heap_update";
goal thy
"approx_val CFS hp val us --> us' >= us --> approx_val CFS hp val us'";
by (simp_tac (simpset() addsplits [any.split,val_.split,tys.split]
addsimps [approx_val_def,sup_any_def]) 1);
by (fast_tac (claset() addss (simpset() addsplits [any.split,val_.split,tys.split]
addsimps [approx_val_def,sup_any_def])) 1);
qed_spec_mp "approx_val_imp_approx_val_sup";
goal thy
"(approx_val CFS hp val (Refs rs)) = \
\ ((? a obj rt. val = Addr a & \
\ hp a = Some obj & \
\ fd2tys CFS (get_obj_type obj) = RTS [rt] & \
\ wideRefsConvertible CFS [rt] rs) | \
\ (val=Null))";
by (asm_full_simp_tac (simpset() setloop (split_tac [val_.split]) addsimps [approx_val_def]) 1);
qed_spec_mp "approx_val_RTS";
goal thy
"(approx_val CFS hp val (Refs (map AT ts))) = \
\ ((? a fd ad. val = Addr a & \
\ hp a = Some (Arr fd ad) & \
\ (? t:set ts. invoConvertible CFS (fd2tys CFS fd) t)) | \
\ (val=Null))";
by (fast_tac (claset() addDs [fd2ty_RT_AT] addss (simpset() addsimps [approx_val_RTS])) 1);
qed_spec_mp "approx_val_RTS_AT";
goal thy
"!! dummy. \
\[| approx_loc CFS hp loc LT; idx < length LT ; val = loc ! idx ; at >= LT ! idx |] \
\==> approx_val CFS hp val at";
by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps
[split_def,approx_loc_def,set_list_all_nth_conv,nth_in_set_list,nth_zip RS sym,length_zip])) 1);
qed "approx_loc_imp_approx_val_sup";
(** approx_loc **)
goal thy
"approx_loc CFS hp (s#xs) (l#ls) = \
\ ((length xs = length ls) & (approx_val CFS hp s l) & (approx_loc CFS hp xs ls))";
by (fast_tac (claset() addss (simpset() addsimps [approx_loc_def])) 1);
qed "approx_loc_Cons";
goalw thy [approx_stk_def,approx_loc_def]
"!!dummy. \
\[| wf_classfiles CFS |] \
\==> (!(t,t'):set (zip tys_n ts). invoConvertible CFS t t') --> \
\ length tys_n = length ts --> approx_stk CFS hp s tys_n --> approx_loc CFS hp s (map US ts)";
by (force_tac (claset() addIs [approx_val_imp_approx_val_invoConvertible], simpset()
addsplits [tys.split,tys.split_asm]
addsimps [set_list_all_nth_conv,length_zip,split_def,nth_zip RS sym]) 1);
qed_spec_mp "invoConv_approx_stk_imp_approx_loc";
goalw thy [approx_loc_def]
"! lvars. approx_loc CFS hp lvars lt --> sup_heap hp hp' --> approx_loc CFS hp' lvars lt";
by (exhaust_tac "lt" 1);
by (Asm_simp_tac 1);
by (deepen_tac (claset() addDs [Suc_imp_0_less] addIs [approx_val_imp_approx_val_sup_heap]
addss (simpset () addsimps [neq_Nil_conv])) 0 1);
qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
goalw thy [sup_loc_def,approx_loc_def]
"approx_loc CFS hp lvars lt --> lt' >>= lt --> approx_loc CFS hp lvars lt'";
by (asm_full_simp_tac (simpset() addsimps [set_list_all_nth_conv,length_zip,split_def,nth_zip RS sym]) 1);
by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset())) 1);
qed_spec_mp "approx_loc_imp_approx_loc_sup";
goalw thy [approx_loc_def]
"!loc idx x X. (approx_loc CFS hp loc LT) --> (approx_val CFS hp x X) \
\ --> (approx_loc CFS hp (loc[idx:=x]) (LT[idx:=X]))";
by (fast_tac (claset() addDs [in_set_list_update_disj] addss (simpset() addsimps [length_lupdate,zip_list_update])) 1);
qed_spec_mp "approx_loc_imp_approx_loc_subst";
(** approx_stk **)
goalw thy [approx_stk_def,approx_loc_def]
"approx_stk CFS hp (rev s) (rev t) = approx_stk CFS hp s t";
by (fast_tac (claset() addss (simpset() addsimps [length_zip,zip_rev,rev_map RS sym])) 1);
qed_spec_mp "approx_stk_rev_lem";
goal thy
"approx_stk CFS hp (rev s) t = approx_stk CFS hp s (rev t)";
by (fast_tac (claset() addIs [approx_stk_rev_lem RS subst] addss (simpset())) 1);
qed_spec_mp "approx_stk_rev";
goalw thy [approx_stk_def]
"! lvars. approx_stk CFS hp lvars lt --> sup_heap hp hp' --> approx_stk CFS hp' lvars lt";
by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup_heap]) 1);
qed_spec_mp "approx_stk_imp_approx_stk_sup_heap";
goalw thy [approx_stk_def]
"! lvars st. approx_stk CFS hp lvars st --> (map US st') >>= (map US st) --> approx_stk CFS hp lvars st'";
by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
qed_spec_mp "approx_stk_imp_approx_stk_sup";
goalw thy [approx_stk_def,approx_loc_def]
"approx_stk CFS hp [] []";
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "approx_stk_Nil";
goalw thy [approx_stk_def,approx_loc_def]
"approx_stk CFS hp (x # stk) (S#ST) = (approx_stk CFS hp stk ST & approx_val CFS hp x (US S))";
by (fast_tac (claset() addss (simpset())) 1);
qed "approx_stk_Cons";
goal thy
"!!dummy. \
\[| approx_stk CFS hp stk (S#ST') |] \
\ ==> ? s stk'. stk = s#stk' & approx_stk CFS hp stk' ST' & approx_val CFS hp s (US S)";
by (exhaust_tac "stk" 1);
by (fast_tac (claset() addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
by (fast_tac (claset() addss (simpset() addsimps [approx_stk_Cons])) 1);
qed "approx_stk_Cons_lemma";
goal thy
"!ST' stk. approx_stk CFS hp stk (S@ST') \
\ --> (? s stk'. stk = s@stk' & length s = length S & length stk' = length ST' & \
\ approx_stk CFS hp s S & approx_stk CFS hp stk' ST')";
by (induct_tac "S" 1);
by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
bd approx_stk_Cons_lemma 1;
by (Clarify_tac 1);
by (eres_inst_tac [("x","ST'")] allE 1);
by (eres_inst_tac [("x","stk'")] allE 1);
by (Clarify_tac 1);
by (res_inst_tac [("x","s#sa")] exI 1);
by (res_inst_tac [("x","stk'a")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
qed_spec_mp "approx_stk_append_lemma";
goalw thy [push_rd_def,pop_rd_def]
"approx_stk CFS hp stk ST' --> (map US ST) >>= map US (push_rd CFS rd ST') \
\ --> approx_stk CFS hp stk (pop_rd CFS rd ST)";
by (asm_full_simp_tac (simpset() addsplits [return_desc.split] addsimps [sup_loc_Cons,map_eq_Cons]) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup]
addss (simpset() addsplits [return_desc.split] addsimps [sup_loc_Cons,map_eq_Cons])) 1);
qed_spec_mp "approx_stk_imp_approx_stk_pop_sup_push";
(** correct_obj **)
goalw thy [correct_obj_def]
"!!dummy. \
\[| is_class CFS cn |] ==> correct_obj CFS hp (Obj cn (init_obj CFS cn))";
by (asm_full_simp_tac (simpset() addsimps [approx_val_def,init_obj_def,Let_def,map_compose_def]) 1);
by (Clarify_tac 1);
by (exhaust_tac "fd" 1);
by (ALLGOALS Asm_simp_tac);
qed "correct_init_obj";
goalw thy [correct_obj_def]
"correct_obj CFS hp (Arr fd (init_arr (default_val fd) n))";
by (asm_full_simp_tac (simpset()
setloop (split_tac [option.split,tys.split,val_.split])
addsimps [approx_val_def,init_obj_def,init_arr_def]) 1);
by (Clarify_tac 1);
bd in_set_replicate 1;
by (fast_tac (claset() addDs [default_val_Intg,default_val_Addr,default_val_Null] addss (simpset())) 1);
qed "correct_init_arr";
goal thy
"(get_all_fields (CFS,cn)) fl = Some fd --> approx_val CFS hp val (fd2any CFS fd) \
\ --> correct_obj CFS hp (Obj cn od) \
\ --> correct_obj CFS hp (Obj cn (od(fl|->val)))";
by (asm_full_simp_tac (simpset() setloop (split_tac [split_if,tys.split])
addsimps [correct_obj_def]) 1);
qed_spec_mp "correct_obj_imp_correct_obj_field_update";
goalw thy [correct_obj_def]
"i < length ad --> approx_val CFS hp val (fd2any CFS fd) --> correct_obj CFS hp (Arr fd ad) \
\ --> correct_obj CFS hp (Arr fd (ad[i:=val]))";
by (fast_tac (claset() addDs [in_set_list_update_disj] addss (simpset())) 1);
qed_spec_mp "correct_obj_imp_correct_obj_array_update";
goal thy
"hp x = None --> correct_obj CFS hp obj --> correct_obj CFS hp obj' \
\ --> correct_obj CFS (hp(newref hp|->obj')) obj";
by (asm_full_simp_tac (simpset() setloop (split_tac [obj.split])
addsimps [correct_obj_def]) 1);
by (blast_tac (claset() addIs [approx_val_imp_approx_val_sup_heap,sup_heap_newref] addss (simpset())) 1);
qed_spec_mp "correct_obj_imp_correct_obj_heap_newref";
goal thy
"hp a = Some obj' --> get_obj_type obj' = get_obj_type obj'' --> correct_obj CFS hp obj \
\ --> correct_obj CFS (hp(a|->obj'')) obj";
by (asm_full_simp_tac (simpset() setloop (split_tac [obj.split]) addsimps [correct_obj_def]) 1);
by (fast_tac (claset() addIs [approx_val_imp_approx_val_heap_update] addss (simpset())) 1);
qed_spec_mp "correct_obj_imp_correct_obj_heap_update";
(** correct_heap **)
goal thy
"hp x = None --> correct_heap CFS hp --> correct_obj CFS hp obj\
\ --> correct_heap CFS (hp(newref hp |-> obj))";
by (asm_full_simp_tac (simpset() addsplits [obj.split] addsimps [correct_heap_def]) 1);
by (fast_tac (claset() addIs [correct_obj_imp_correct_obj_heap_newref]
addss (simpset() addsimps [])) 1);
qed_spec_mp "correct_heap_imp_correct_heap_newref";
goal thy
"(get_all_fields (CFS,cn)) fl = Some fd & hp a = Some (Obj cn od) & \
\ approx_val CFS hp val (fd2any CFS fd) & correct_heap CFS hp \
\ --> correct_heap CFS (hp(a |-> (Obj cn (od(fl|->val)))))";
by (asm_full_simp_tac (simpset() setloop (split_tac [split_if,obj.split])
addsimps [correct_heap_def]) 1);
by (strip_tac 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","aa")] allE 1);
by (fast_tac (claset() addIs
[correct_obj_imp_correct_obj_heap_update,
correct_obj_imp_correct_obj_field_update,
approx_val_imp_approx_val_sup_heap]
addss (simpset() addsimps [sup_heap_update_value])) 1);
qed_spec_mp "correct_heap_imp_correct_heap_field_update";
goal thy
"i<length ad & hp a = Some (Arr fd ad) & \
\ approx_val CFS hp val (fd2any CFS fd) & correct_heap CFS hp \
\ --> correct_heap CFS (hp(a |-> (Arr fd (ad[i:=val]))))";
by (asm_full_simp_tac (simpset() setloop (split_tac [split_if,obj.split])
addsimps [correct_heap_def]) 1);
by (strip_tac 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","aa")] allE 1);
by (fast_tac (claset() addIs
[correct_obj_imp_correct_obj_heap_update,
correct_obj_imp_correct_obj_array_update,
approx_val_imp_approx_val_sup_heap]
addss (simpset() addsimps [sup_heap_update_array])) 1);
qed_spec_mp "correct_heap_imp_correct_heap_array_update";
(** correct_frames **)
Delsimps [fun_upd_apply];
goal thy
"!cl ml. correct_frames CFS hp phi cl ml frs & \
\ hp a = Some (Obj cn od) & (get_all_fields (CFS,cn)) fl = Some fd & \
\ approx_val CFS hp val (fd2any CFS fd) \
\ --> correct_frames CFS (hp(a |-> (Obj cn (od(fl|->val))))) phi cl ml frs";
by (induct_tac "frs" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() setloop (split_tac [return_desc.split])
addsimps [Let_def,split_def,correct_frame_def]) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
approx_loc_imp_approx_loc_sup_heap,
correct_heap_imp_correct_heap_field_update,
sup_heap_update_value] addss (simpset())) 1);
qed_spec_mp "correct_frames_imp_correct_frames_field_update";
goal thy
"!cl ml. correct_frames CFS hp phi cl ml frs & \
\ hp a = Some (Arr fd ad) & i<length ad & \
\ approx_val CFS hp val (fd2any CFS fd) \
\ --> correct_frames CFS (hp(a |-> (Arr fd (ad[i:=val])))) phi cl ml frs";
by (induct_tac "frs" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() setloop (split_tac [return_desc.split])
addsimps [Let_def,split_def,correct_frame_def]) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
approx_loc_imp_approx_loc_sup_heap,
correct_heap_imp_correct_heap_array_update,
sup_heap_update_array] addss (simpset())) 1);
qed_spec_mp "correct_frames_imp_correct_frames_array_update";
goal thy
"!cl ml. hp x = None --> correct_frames CFS hp phi cl ml frs & \
\ correct_obj CFS hp obj \
\ --> correct_frames CFS (hp(newref hp |-> obj)) phi cl ml frs";
by (induct_tac "frs" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() setloop (split_tac [return_desc.split])
addsimps [Let_def,split_def,correct_frame_def]) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
approx_loc_imp_approx_loc_sup_heap,
correct_heap_imp_correct_heap_newref,
sup_heap_newref] addss (simpset())) 1);
qed_spec_mp "correct_frames_imp_correct_frames_newref";
goal thy
"!! dummy. \
\[| correct_heap CFS hp; hp a = Some obj; \
\ fd2tys CFS (get_obj_type obj) = RTS [rt] |] \
\==> wideRefConvertible CFS rt (CT cn) \
\ --> ((? od cn'. obj = Obj cn' od & is_class CFS cn' & wideRefConvertible CFS (CT cn') (CT cn)) | \
\ (? ad fd. obj = Arr fd ad & cn=Object))";
by (exhaust_tac "obj" 1);
by (fast_tac (claset() addss (simpset() addsimps [correct_heap_def,correct_obj_def,is_class_def])) 1);
by (fast_tac (claset() addss (simpset() addsimps [correct_obj_def])) 1);
qed_spec_mp "wRC_lemma0";
goal thy
"!! dummy. \
\[| wf_classfiles CFS; correct_heap CFS hp; hp a = Some obj; \
\ fd2tys CFS (get_obj_type obj) = RTS [rt]; get_fields (CFS !! cn) (cn,fn) = Some fd; \
\ wideRefConvertible CFS rt (CT cn) |] \
\==> ? od cn'. obj = Obj cn' od & is_class CFS cn' & wideRefConvertible CFS (CT cn') (CT cn)";
by (fast_tac (claset() addDs [wRC_lemma0,wf_cs6] addss (simpset())) 1);
qed_spec_mp "wRC_lemma1";
goal thy
"!! dummy. \
\[| wf_classfiles CFS; hp a = Some obj; correct_heap CFS hp |] \
\==> is_class CFS (get_obj_class obj)";
by (exhaust_tac "obj" 1);
by (fast_tac (claset() addss (simpset() addsimps [correct_heap_def,correct_obj_def])) 1);
by (fast_tac (claset() addDs [wf_cs6] addss (simpset() addsimps [correct_heap_def])) 1);
qed "is_class_get_obj_class";
goal thy
"wf_classfiles CFS --> t : set ts --> \
\ invoConvertible CFS (fd2tys CFS fd) t --> \
\ ins_type_tysl_ok X ts --> \
\ ins_type_tys_ok X ts' --> \
\ approx_val CFS hp s (US ts') --> \
\ fd_compatible CFS hp X s fd --> \
\approx_val CFS hp s (fd2any CFS fd)";
by (exhaust_tac "X" 1);
by (asm_full_simp_tac (simpset() setloop (split_tac [ins_type.split,val_.split])
addsimps [fd_compatible_def,ins_type_tys_ok_def,ins_type_tysl_ok_def,approx_val_def,
prim_eq_Integer]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (exhaust_tac "fd" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps [fd_compatible_def,ins_type_tys_ok_def,ins_type_tysl_ok_def]) 1);
by (Clarify_tac 1);
br conjI 1;
by (asm_full_simp_tac (simpset() setloop (split_tac [val_.split])
addsimps [fd_compatible_def,ins_type_tys_ok_def,ins_type_tysl_ok_def,Let_def,
approx_val_def]) 1);
by (Clarify_tac 1);
by (exhaust_tac "fd" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [approx_val_RTS,Let_def]) 1);
by (Clarify_tac 1);
bd compatible_imp_invoConvertible 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps [approx_val_def,get_Addr_Addr]) 1);
by (Fast_tac 1);
qed_spec_mp "fd_compatible_imp_approx_val";
goal thy
"wf_classfiles CFS --> hp a = Some (Obj cn od) --> \
\ correct_heap CFS hp --> \
\ wideRefConvertible CFS (CT cn) (CT fc) --> \
\ get_fields (CFS !! fc) (fc,fn) = Some fd --> \
\approx_val CFS hp (od!!(fc,fn)) (fd2any CFS fd)";
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [correct_heap_def]) 1);
by (eres_inst_tac [("x","a")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [correct_obj_def]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","fc")] allE 1);
by (eres_inst_tac [("x","fn")] allE 1);
by (eres_inst_tac [("x","fd")] allE 1);
bd get_fields_impl_get_all_fields3 1;
by (asm_full_simp_tac (simpset() addsimps []) 2);
ba 2;
by (fast_tac (claset() addDs [in_d_superclass_rel_is_class2]) 1);
by (fast_tac (claset() addss (simpset())) 1);
qed_spec_mp "get_fields_imp_approx_val";
goal thy
"!!dummy ml. \
\[| wf_classfiles CFS; correct_obj CFS hp obj; \
\ r:set rs; oc=get_obj_class obj; fd2tys CFS (get_obj_type obj) = RTS [rt]; \
\ wideRefConvertible CFS rt r; inv_methref_ok CFS mci rs inv_com; is_class CFS oc |] \
\ ==> get_methods (CFS !! mci) ml = Some (rd,ins) \
\ --> dc=dyn_class (CFS, ml, oc) \
\ --> is_class CFS dc & wideRefConvertible CFS rt (CT dc) & \
\ (? ins'. get_methods (CFS !! dc) ml = Some (rd,ins'))";
by (exhaust_tac "obj" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [correct_obj_def,is_class_def]) 1);
(* ???? *)
by (Clarify_tac 1);
bd inv_methref_ok_impl_get_methods_CT 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
ba 1;
by (asm_full_simp_tac (simpset() addsimps [is_class_def]) 1);
ba 1;
br refl 1;
by (fast_tac (claset() addDs [inv_methref_ok_impl_get_methods_CT] addss (simpset() addsimps [is_class_def])) 1);
by (Clarify_tac 1);
bd inv_methref_ok_impl_get_methods_AT 1;
ba 1;
by (fast_tac (claset() addDs [inv_methref_ok_impl_get_methods_AT] addss (simpset() addsimps [correct_obj_def])) 1);
ba 1;
ba 1;
br refl 1;
by (fast_tac (claset() addDs [inv_methref_ok_impl_get_methods_AT] addss (simpset() addsimps [correct_obj_def])) 1);
(*
by (force_tac (claset() addDs [inv_methref_ok_impl_get_methods_CT], simpset() addsimps [is_class_def]) 1);
by (force_tac (claset() addDs [inv_methref_ok_impl_get_methods_AT], simpset() addsimps [correct_obj_def]) 1);
by (fast_tac (claset() addDs [inv_methref_ok_impl_get_methods_CT] addss (simpset() addsimps [is_class_def])) 1);
by (fast_tac (claset() addDs [inv_methref_ok_impl_get_methods_AT] addss (simpset() addsimps [correct_obj_def])) 1);
*)
qed_spec_mp "inv_methref_ok_impl_get_methods";