Convert.ML
Back to theory Convert
context WF.thy;
Goal
"!!dummy. wf R ==> wf{((A,x),(B,y)) . A=B & (x,y):R}";
by(simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
by(strip_tac 1);
by(rename_tac "A x" 1);
by (eres_inst_tac [("a","x")] wf_induct 1);
by (Fast_tac 1);
val wf_rel_lemma3 = result();
Goal
"!!dummy. wf R ==> wf{((A,x,m),(B,y,n)) . A=B & (x,y):R & (m,n):R}";
by(simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
br allI 1;
br impI 1;
br allI 1;
br allI 1;
(* do not eliminate the last quantifier! *)
by(rename_tac "P A x" 1);
by (res_inst_tac [("a","x")] wf_induct 1);
ba 1;
by(strip_tac 1);
by(rename_tac "P A xa x m" 1);
by(eres_inst_tac [("a","m")] wf_induct 1);
by (Fast_tac 1);
val wf_rel_lemma4 = result();
context thy;
Goal
"!!dummy. \
\wf_classfiles CFS \
\==> !fd'. compatible CFS fd fd' --> invoConvertible CFS (fd2tys CFS fd) (fd2tys CFS fd')";
by (induct_tac "fd" 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsplits [tys.split,field_desc.split] addsimps [rtrancl_eq_or_trancl]) 1);
by (fast_tac (claset()
addDs [in_superclass_rel_imp_is_class,implements_impl_is_inter]
addss (simpset() addsimps [is_class_def,trancl_into_rtrancl])) 1);
by (asm_full_simp_tac (simpset() addsplits [tys.split,field_desc.split]) 1);
by (fast_tac (claset() addDs [wf_cs6,fd2ty_PT,compatible_I]
addss (simpset() addsimps [prim_eq_Integer RS sym,is_class_def])) 1);
qed_spec_mp "compatible_imp_invoConvertible";
goalw thy [wf_classfiles_def]
"wf_classfiles CFS --> CFS cn ~= None --> get_thisclass (CFS !! cn) = cn";
by (Fast_tac 1);
qed_spec_mp "wf_cs5";
goal thy
"!!dummy. \
\[| wf_classfiles CFS; is_class CFS fc; get_fields (CFS !! fc) (fc', fn) ~= None |] \
\ ==> fc'=fc";
by (fast_tac (claset() addDs [wf_cs5,map_of_SomeD] addss (simpset() addsimps
[get_fields_def,split_def,get_thisclass_def,not_None_eq,is_class_def])) 1);
qed "is_defined_get_fields_lemma";
goal thy
"!!dummy. \
\[| wf_classfiles CFS; is_class CFS fc; fc'~=fc |] \
\ ==> (get_fields (CFS !! fc)) (fc', fn) = None";
be swap 1;
by (fast_tac (claset() addDs [is_defined_get_fields_lemma]) 1);
qed "is_not_defined_get_fields_lemma";
goal thy
"!!dummy. \
\[| wf_classfiles CFS; is_class CFS fc; wideRefConvertible CFS (CT cn) (CT fc) |] \
\ ==> get_fields (CFS !! fc) (fc, fn) = Some fd \
\ --> (get_all_fields (CFS, cn)) (fc,fn) = Some fd";
by (asm_full_simp_tac (simpset()) 1);
by (forward_tac [in_d_superclass_rel_is_class] 1);
ba 1;
be rtrancl_induct 1;
by (asm_full_simp_tac (simpset() addsimps [Let_def,get_all_fields_rec,override_def]) 1);
by (case_tac "fc = z" 1);
by (fast_tac (claset() addss (simpset() addsimps [Let_def,get_all_fields_rec,override_def])) 1);
by (asm_full_simp_tac (simpset() setloop (split_tac [option.split])
addsimps [Let_def,get_all_fields_rec,override_def,d_superclass_rel_def]) 1);
by (dres_inst_tac [("fn","fn")] is_not_defined_get_fields_lemma 1);
ba 2;
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "get_fields_impl_get_all_fields3";
goal thy
"wideRefConvertible CFS r r & invoConvertible CFS t t & (!rs'. set rs <= set rs' --> wideRefsConvertible CFS rs rs')";
by (res_inst_tac [("Rt","r"),("tys","t"),("list","rs")] Rt_tys.induct 1);
auto();
qed "Convertible_refl";
goal thy
"wideRefConvertible CFS (AT ts) r --> (r=CT Object) | (? ts'. r=AT ts' & invoConvertible CFS ts ts')";
by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if,Rt.split])
addsimps [rtrancl_eq_or_trancl]) 1);
qed_spec_mp "wideRefConvertible_AT";
(**
goal thy
"invoConvertible CFS ts ts' --> (? pt. ts=PTS pt & ts'=ts) \
\ | (? rs rs'. ts=RTS rs & ts'=RTS rs' & (!r:set rs. ? r':set rs'. wideRefConvertible CFS r r'))";
**)
goal thy
"invoConvertible CFS ts ts' --> (? pt. ts=PTS pt & ts'=ts) \
\ | (? rs rs'. ts=RTS rs & ts'=RTS rs' & wideRefsConvertible CFS rs rs')";
by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if,tys.split])
addsimps []) 1);
by (exhaust_tac "ts" 1);
by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if,tys.split])
addsimps []) 1);
by (asm_full_simp_tac (simpset() setloop (split_tac [expand_if,tys.split])
addsimps []) 1);
qed_spec_mp "wideRefinvoonvertible_disj";
goal thy
"wf_classfiles CFS --> wideRefConvertible CFS (CT Object) r --> (r=CT Object)";
by (fast_tac (claset() addDs [not_implements_Object,not_in_superclass_rel_Object]
addss (simpset() addsplits [Rt.split] addsimps [rtrancl_eq_or_trancl])) 1);
qed_spec_mp "wideRefConvertible_CT_Object";
goal thy
"wideRefsConvertible CFS rs rs' = (!r:set rs. ? r':set rs'. wideRefConvertible CFS r r')";
by (induct_tac "rs" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "wRC";
goal thy
"!!CFS. wf_classfiles CFS ==> \
\ (!r' r''. wideRefConvertible CFS r r' --> wideRefConvertible CFS r' r'' --> wideRefConvertible CFS r r'') & \
\ (!t' t''. invoConvertible CFS t t' --> invoConvertible CFS t' t'' --> invoConvertible CFS t t'') & \
\ (!rs' rs''. wideRefsConvertible CFS rs rs' --> wideRefsConvertible CFS rs' rs'' --> wideRefsConvertible CFS rs rs'')";
by (res_inst_tac [("Rt","r"),("tys","t"),("list","rs")] Rt_tys.induct 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
br conjI 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (fast_tac (claset() addEs [rtrancl_trans] addss (simpset())) 1);
by (Clarify_tac 1);
br conjI 1;
by (fast_tac (claset() addDs [not_implements_Object] addss (simpset())) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
by (fast_tac (claset() addDs [not_in_superclass_rel_Object] ) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
br conjI 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
be disjE 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
by (fast_tac (claset() addDs [implements_superinterface_trans] ) 1);
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
by (forward_tac [implements_impl_is_inter] 1);
ba 1;
by (fast_tac (claset() addDs [in_superclass_rel_Object] addss (simpset())) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
be disjE 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
be disjE 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (fast_tac (claset() addIs [implements_superclass_rel_trans,trancl_trans] addss (simpset())) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
by (fast_tac (claset() addDs [trancl_trans] addss (simpset())) 1);
(* increasing stack:
by (asm_full_simp_tac (simpset() addsimps []) 1);
*)
by (Clarify_tac 1);
bd wideRefConvertible_AT 1;
be disjE 1;
by (Clarify_tac 1);
bd wideRefConvertible_CT_Object 1;
ba 1;
by (simp_tac (simpset()) 1);
by (Clarify_tac 1);
by (Clarify_tac 1);
bd wideRefConvertible_AT 1;
be disjE 1;
by (Clarify_tac 1);
by (simp_tac (simpset()) 1);
by (Clarify_tac 1);
by (simp_tac (simpset() addsimps []) 1);
by (Fast_tac 1);
by (simp_tac (simpset() addsimps []) 1);
by (simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
bd wideRefinvoonvertible_disj 1;
be disjE 1;
by (Clarify_tac 1);
by (Clarify_tac 1);
by (simp_tac (simpset()) 1);
by (Fast_tac 1);
by (simp_tac (simpset()) 1);
by (simp_tac (simpset()) 1);
by (Clarify_tac 1);
br conjI 1;
by (Fast_tac 2);
by (thin_tac "!rs' rs''.\
\ wideRefsConvertible CFS list rs' -->\
\ wideRefsConvertible CFS rs' rs'' --> wideRefsConvertible CFS list rs''" 1);
by (thin_tac "wideRefsConvertible CFS list rs'" 1);
by (eres_inst_tac [("x","r'")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [wRC]) 1);
by (Fast_tac 1);
qed "Convertible_trans";
val wideRefConvertible_trans = Convertible_trans RS conjunct1 RS spec RS spec;
val invoConvertible_trans = Convertible_trans RS conjunct2 RS conjunct1 RS spec RS spec;
val wideRefsConvertible_trans = Convertible_trans RS conjunct2 RS conjunct2 RS spec RS spec;
goalw thy [wf_classfiles_def,wf_class_def]
"!!dummy.\
\[| wf_classfiles CFS; (sc,cn) : (d_superclass_rel CFS)^* |] \
\==> method_over_ok CFS cn sc";
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
be disjE 1;
by (fast_tac (claset() addss (simpset() addsimps [method_over_ok_def])) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","cn")] allE 1);
by (case_tac "no_super (CFS !! cn)" 1);
by (force_tac (claset() addEs [tranclE],simpset() addsimps [d_superclass_rel_def,is_class_def]) 1);
by (fast_tac (claset() addDs [in_superclass_rel_imp_is_class] addss (simpset()
addsimps [Let_def,is_class_def]) ) 1);
qed "wf_cs9";
(***
goal thy
"!!dummy.\
\[| wf_classfiles CFS; wideRefConvertible CFS (CT cn) (CT mc) |] \
\==> method_over_ok CFS cn mc";
by (asm_full_simp_tac (simpset()) 1);
by (fast_tac (claset() addIs [wf_cs9]) 1);
qed "wideRefConvertible_imp_method_over_ok";
***)
goal thy
"!!dummy. \
\[| wf_classfiles CFS; is_class CFS cn; get_methods (CFS !! cn) ml = None; \
\ cn ~= Object; get_superclass (CFS !! cn) = sc |] \
\==> dyn_class (CFS, ml, cn) = dyn_class (CFS, ml, sc)";
by (asm_full_simp_tac (simpset() addsimps [Let_def,dyn_class_rec]) 1);
qed "dyn_class_None";
goal thy
"!!dummy. \
\[| wf_classfiles CFS; is_class CFS cn; get_methods (CFS !! cn) ml ~= None |] \
\==> dyn_class (CFS, ml, cn) = cn";
by (asm_full_simp_tac (simpset() addsimps [Let_def,dyn_class_rec]) 1);
qed "dyn_class_not_None";
(**
goal thy
"wf_classfiles CFS --> wideRefConvertible CFS (CT Object) r --> r=CT Object";
by (asm_full_simp_tac (simpset() setloop (split_tac [Rt.split])
addsimps [not_in_superclass_rel_Object,not_implements_Object,rtrancl_eq_or_trancl]) 1);
qed_spec_mp "wideRefConvertible_Object";
goal thy
"is_class CFS mc --> wideRefConvertible CFS (CT cn) (CT mc) --> is_class CFS cn";
by (asm_full_simp_tac (simpset() addsimps [in_superclass_rel_imp_is_class,rtrancl_eq_or_trancl]) 1);
qed_spec_mp "wideRefConvertible_imp_is_class";
goal thy
"wideRefConvertible CFS (CT cn) (CT mc) --> cn~=mc \
\ --> wideRefConvertible CFS (CT (get_superclass CFS !! cn)) (CT mc)";
by (asm_full_simp_tac (simpset() addsimps [rtrancl_eq_or_trancl]) 1);
by (fast_tac (claset() addEs [tranclE] addss (simpset() addsimps [d_superclass_rel_def])) 1);
qed_spec_mp "wideRefConvertible_imp_wideRefConvertible_superclass";
goal thy
"wf_classfiles CFS --> is_class CFS cn --> cn ~= Object \
\ --> wideRefConvertible CFS (CT cn) (CT (get_superclass (CFS !! cn)))";
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def,rtrancl_eq_or_trancl]) 1);
by (fast_tac (claset() addIs [r_into_trancl] addDs [wf_cs4] addss (simpset())) 1);
qed_spec_mp "wideRefConvertible_superclass";
**)
goal thy
"get_methods (CFS !! cn) ml = None --> get_methods (CFS !! mc) ml = Some x --> cn~=mc";
by (case_tac "cn=mc" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "get_methods_None_Some_imp_neq";
goalw thy [method_over_ok_def]
"method_over_ok CFS cn si --> get_methods (CFS !! si) ml = Some (rd, ins) --> get_methods (CFS !! cn) ml ~= None\
\ --> (? ins'. get_methods (CFS !! cn) ml = Some (rd, ins'))";
by (fast_tac (claset() addss (simpset() delsimps [split_paired_All] addsimps [not_None_eq])) 1);
qed_spec_mp "method_over_ok_lemma";
(**************
goal thy
"!!dummy. \
\ wf_classfiles CFS \
\ --> wideRefConvertible CFS (CT oc) (CT mc) --> is_class CFS mc \
\ --> get_methods (CFS !! mc) (mn,pd) = Some (rd,ins) \
\ --> dc=dyn_class (CFS, (mn,pd), oc) \
\ --> is_class CFS dc & wideRefConvertible CFS (CT oc) (CT dc) & \
\ (? ins'. get_methods (CFS !! dc) (mn,pd) = Some (rd,ins'))";
by (res_inst_tac [("u","CFS"),("v","mn"),("w","pd"),("x","oc")] dyn_class.induct 1);
br wf_dyn_class_term_rel 1;
by (asm_full_simp_tac (simpset() addsimps [dyn_class_term_rel_def,d_superclass_rel_def]) 1);
by (Clarify_tac 1);
by (case_tac "get_methods (CFS !! cn) (a, b) = None" 1);
by (case_tac "cn=Object" 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [not_in_superclass_rel_Object,rtrancl_eq_or_trancl]) 1);
by (asm_full_simp_tac (simpset() addsimps [wf_d_superclass_rel]) 1);
by (forward_tac [in_d_superclass_rel_is_class] 1);
ba 1;
by (forward_tac [wf_cs4] 1);
ba 1;
br refl 1;
ba 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (Clarify_tac 1);
be rtranclE 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps [d_superclass_rel_def]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [dyn_class_None]) 1);
by (Clarify_tac 1);
be rtrancl_trans 1;
br r_into_rtrancl 1;
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (forward_tac [in_d_superclass_rel_is_class] 1);
ba 1;
by (asm_full_simp_tac (simpset() addsimps [dyn_class_not_None]) 1);
by (fast_tac (claset() addIs [wf_cs9,method_over_ok_lemma]) 1);
qed_spec_mp "get_methods_super_impl_get_methods3";
(* geht nicht ueber dyn_class.induct, aber es braucht ja gar keine Induktion *)
goal thy
"!!dummy. \
\ wf_classfiles CFS \
\ --> wideRefConvertible CFS (AT at) (CT mc) --> is_class CFS mc \
\ --> get_methods (CFS !! mc) (mn,pd) = Some (rd,ins) \
\ --> dc=dyn_class (CFS, (mn,pd), Object) \
\ --> is_class CFS dc & wideRefConvertible CFS (AT at) (CT dc) & \
\ (? ins'. get_methods (CFS !! dc) (mn,pd) = Some (rd,ins'))";
by (asm_full_simp_tac (simpset() addsimps [dyn_class_not_None]) 1);
qed_spec_mp "get_methods_super_impl_get_methods3_AT";
*************)
goal thy
"fd2tys CFS (get_obj_type obj) = RTS rs --> (!r:set rs. wideRefConvertible CFS r (AT t')) \
\ --> (? fd ad. obj = Arr fd ad & invoConvertible CFS (fd2tys CFS fd) t')";
by (exhaust_tac "obj" 1);
by (asm_simp_tac (simpset() ) 1);
br conjI 1;
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset()) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset()) 1);
br impI 1;
by (rotate_tac ~1 1);
bd sym 1;
by (asm_full_simp_tac (simpset() setloop (split_tac [Rt.split])) 1);
qed_spec_mp "fd2ty_RT_AT";